Skip to content

Commit 2010d41

Browse files
selloutsellout
authored
Add kind polymorphism. (#563)
Here’s an example: ./polyfunctor ```dhall λ(j : Kind) → λ(k : Kind) → λ(c : j → j → Type) → λ(d : k → k → Type) → λ(f : j → k) → { map : ∀(a : j) → ∀(b : j) → c a b → d (f a) (f b) } ``` then ```dhall ./polyfunctor Type Type (λ(a : Type) → λ(b : Type) → a → b) (λ(a : Type) → λ(b : Type) → a → b) Optional ``` normalizes to ```dhall { map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b } ``` and ```dhall ./polyfunctor (Type → Type) (Type → Type) (λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i) (λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i) ``` normalizes to ```dhall λ(f : (Type → Type) → Type → Type) → { map : ∀(a : Type → Type) → ∀(b : Type → Type) → (∀(i : Type) → a i → b i) → ∀(i : Type) → f a i → f b i } ```
1 parent 25a0d69 commit 2010d41

File tree

14 files changed

+249
-214
lines changed

14 files changed

+249
-214
lines changed

‎src/Dhall/Binary.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,8 @@ encode (Const Type) =
152152
TString "Type"
153153
encode (Const Kind) =
154154
TString "Kind"
155+
encode (Const Sort) =
156+
TString "Sort"
155157
encode e@(App _ _) =
156158
TList ([ TInt 0, f₁ ] ++ map encode arguments)
157159
where
@@ -478,6 +480,8 @@ decode (TString "Type") =
478480
return (Const Type)
479481
decode (TString "Kind") =
480482
return (Const Kind)
483+
decode (TString "Sort") =
484+
return (Const Sort)
481485
decode (TString x) =
482486
return (Var (V x 0))
483487
decode (TList [ TString x, TInt n ]) =

‎src/Dhall/Core.hs‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,22 +90,26 @@ import qualified Dhall.Map
9090

9191
{-| Constants for a pure type system
9292
93-
The only axiom is:
93+
The axioms are:
9494
9595
> ⊦ Type : Kind
96+
> ⊦ Kind : Sort
9697
9798
... and the valid rule pairs are:
9899
99100
> ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions)
100101
> ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions)
101102
> ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors)
103+
> ⊦ Sort ↝ Type : Type -- Functions from kinds to terms (kind-polymorphic functions)
104+
> ⊦ Sort ↝ Kind : Kind -- Functions from kinds to types (polymorphic type constructors)
105+
> ⊦ Sort ↝ Sort : Sort -- Functions from kinds to kinds (kind constructors)
102106
103107
These are the same rule pairs as System Fω
104108
105109
Note that Dhall does not support functions from terms to types and therefore
106110
Dhall is not a dependently typed language
107111
-}
108-
data Const = Type | Kind deriving (Show, Eq, Data, Bounded, Enum, Generic)
112+
data Const = Type | Kind | Sort deriving (Show, Eq, Data, Bounded, Enum, Generic)
109113

110114
instance Pretty Const where
111115
pretty = Pretty.unAnnotate . prettyConst
@@ -2117,6 +2121,7 @@ reservedIdentifiers =
21172121
, "in"
21182122
, "Type"
21192123
, "Kind"
2124+
, "Sort"
21202125
, "forall"
21212126
, "Bool"
21222127
, "True"

‎src/Dhall/Parser/Expression.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -266,6 +266,7 @@ completeExpression embedded = completeExpression_
266266
|| c == 'L'
267267
|| c == 'O'
268268
|| c == 'B'
269+
|| c == 'S'
269270
|| c == 'T'
270271
|| c == 'F'
271272
|| c == 'K'
@@ -316,6 +317,7 @@ completeExpression embedded = completeExpression_
316317
, Optional <$ _Optional
317318
]
318319
'B' -> Bool <$ _Bool
320+
'S' -> Const Sort <$ _Sort
319321
'T' ->
320322
choice
321323
[ Text <$ _Text

‎src/Dhall/Parser/Token.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ module Dhall.Parser.Token (
5757
_False,
5858
_Type,
5959
_Kind,
60+
_Sort,
6061
_equal,
6162
_or,
6263
_plus,
@@ -623,6 +624,9 @@ _Type = reserved "Type"
623624
_Kind :: Parser ()
624625
_Kind = reserved "Kind"
625626

627+
_Sort :: Parser ()
628+
_Sort = reserved "Sort"
629+
626630
_equal :: Parser ()
627631
_equal = reservedChar '='
628632

‎src/Dhall/Pretty/Internal.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -311,6 +311,7 @@ prettyScientific = literal . Pretty.pretty . show
311311
prettyConst :: Const -> Doc Ann
312312
prettyConst Type = builtin "Type"
313313
prettyConst Kind = builtin "Kind"
314+
prettyConst Sort = builtin "Sort"
314315

315316
prettyVar :: Var -> Doc Ann
316317
prettyVar (V x 0) = label (Pretty.unAnnotate (prettyLabel x))

‎src/Dhall/TypeCheck.hs‎

Lines changed: 105 additions & 94 deletions
Large diffs are not rendered by default.

‎tests/Parser.hs‎

Lines changed: 117 additions & 114 deletions
Original file line numberDiff line numberDiff line change
@@ -34,121 +34,124 @@ parserTests =
3434
, shouldParse
3535
"whitespace buffet"
3636
"./tests/parser/whitespaceBuffet.dhall"
37-
, shouldParse
38-
"label"
39-
"./tests/parser/label.dhall"
40-
, shouldParse
41-
"quoted label"
42-
"./tests/parser/quotedLabel.dhall"
43-
, shouldParse
44-
"double quoted string"
45-
"./tests/parser/doubleQuotedString.dhall"
46-
, shouldParse
47-
"Unicode double quoted string"
48-
"./tests/parser/unicodeDoubleQuotedString.dhall"
49-
, shouldParse
50-
"escaped double quoted string"
51-
"./tests/parser/escapedDoubleQuotedString.dhall"
52-
, shouldParse
53-
"interpolated double quoted string"
54-
"./tests/parser/interpolatedDoubleQuotedString.dhall"
55-
, shouldParse
56-
"single quoted string"
57-
"./tests/parser/singleQuotedString.dhall"
58-
, shouldParse
59-
"escaped single quoted string"
60-
"./tests/parser/escapedSingleQuotedString.dhall"
61-
, shouldParse
62-
"interpolated single quoted string"
63-
"./tests/parser/interpolatedSingleQuotedString.dhall"
64-
, shouldParse
65-
"double"
66-
"./tests/parser/double.dhall"
67-
, shouldParse
68-
"natural"
69-
"./tests/parser/natural.dhall"
70-
, shouldParse
71-
"identifier"
72-
"./tests/parser/identifier.dhall"
73-
, shouldParse
74-
"paths"
75-
"./tests/parser/paths.dhall"
76-
, shouldParse
77-
"path termination"
78-
"./tests/parser/pathTermination.dhall"
79-
, shouldParse
80-
"urls"
81-
"./tests/parser/urls.dhall"
82-
, shouldParse
83-
"environmentVariables"
84-
"./tests/parser/environmentVariables.dhall"
85-
, shouldParse
86-
"lambda"
87-
"./tests/parser/lambda.dhall"
88-
, shouldParse
89-
"if then else"
90-
"./tests/parser/ifThenElse.dhall"
91-
, shouldParse
92-
"let"
93-
"./tests/parser/let.dhall"
94-
, shouldParse
95-
"forall"
96-
"./tests/parser/forall.dhall"
97-
, shouldParse
98-
"function type"
99-
"./tests/parser/functionType.dhall"
100-
, shouldParse
101-
"operators"
102-
"./tests/parser/operators.dhall"
103-
, shouldParse
104-
"annotations"
105-
"./tests/parser/annotations.dhall"
106-
, shouldParse
107-
"merge"
108-
"./tests/parser/merge.dhall"
109-
, shouldParse
110-
"constructors"
111-
"./tests/parser/constructors.dhall"
112-
, shouldParse
113-
"fields"
114-
"./tests/parser/fields.dhall"
115-
, shouldParse
116-
"record"
117-
"./tests/parser/record.dhall"
118-
, shouldParse
119-
"union"
120-
"./tests/parser/union.dhall"
121-
, shouldParse
122-
"list"
123-
"./tests/parser/list.dhall"
124-
, shouldParse
125-
"builtins"
126-
"./tests/parser/builtins.dhall"
127-
, shouldParse
128-
"import alternatives"
129-
"./tests/parser/importAlt.dhall"
130-
, shouldParse
131-
"large expression"
132-
"./tests/parser/largeExpression.dhall"
133-
, shouldParse
134-
"names that begin with reserved identifiers"
135-
"./tests/parser/reservedPrefix.dhall"
136-
, shouldParse
137-
"interpolated expressions with leading whitespace"
138-
"./tests/parser/template.dhall"
139-
, shouldNotParse
140-
"records with duplicate fields"
141-
"./tests/parser/failure/duplicateFields.dhall"
142-
, shouldParse
143-
"collections with type annotations containing imports"
144-
"./tests/parser/collectionImportType.dhall"
145-
, shouldParse
146-
"a parenthesized custom header import"
147-
"./tests/parser/parenthesizeUsing.dhall"
148-
, shouldNotParse
149-
"accessing a field of an import without parentheses"
150-
"./tests/parser/failure/importAccess.dhall"
15137
]
38+
, shouldParse
39+
"label"
40+
"./tests/parser/label.dhall"
41+
, shouldParse
42+
"quoted label"
43+
"./tests/parser/quotedLabel.dhall"
44+
, shouldParse
45+
"double quoted string"
46+
"./tests/parser/doubleQuotedString.dhall"
47+
, shouldParse
48+
"Unicode double quoted string"
49+
"./tests/parser/unicodeDoubleQuotedString.dhall"
50+
, shouldParse
51+
"escaped double quoted string"
52+
"./tests/parser/escapedDoubleQuotedString.dhall"
53+
, shouldParse
54+
"interpolated double quoted string"
55+
"./tests/parser/interpolatedDoubleQuotedString.dhall"
56+
, shouldParse
57+
"single quoted string"
58+
"./tests/parser/singleQuotedString.dhall"
59+
, shouldParse
60+
"escaped single quoted string"
61+
"./tests/parser/escapedSingleQuotedString.dhall"
62+
, shouldParse
63+
"interpolated single quoted string"
64+
"./tests/parser/interpolatedSingleQuotedString.dhall"
65+
, shouldParse
66+
"double"
67+
"./tests/parser/double.dhall"
68+
, shouldParse
69+
"natural"
70+
"./tests/parser/natural.dhall"
71+
, shouldParse
72+
"identifier"
73+
"./tests/parser/identifier.dhall"
74+
, shouldParse
75+
"paths"
76+
"./tests/parser/paths.dhall"
77+
, shouldParse
78+
"path termination"
79+
"./tests/parser/pathTermination.dhall"
80+
, shouldParse
81+
"urls"
82+
"./tests/parser/urls.dhall"
83+
, shouldParse
84+
"environmentVariables"
85+
"./tests/parser/environmentVariables.dhall"
86+
, shouldParse
87+
"lambda"
88+
"./tests/parser/lambda.dhall"
89+
, shouldParse
90+
"if then else"
91+
"./tests/parser/ifThenElse.dhall"
92+
, shouldParse
93+
"let"
94+
"./tests/parser/let.dhall"
95+
, shouldParse
96+
"forall"
97+
"./tests/parser/forall.dhall"
98+
, shouldParse
99+
"function type"
100+
"./tests/parser/functionType.dhall"
101+
, shouldParse
102+
"operators"
103+
"./tests/parser/operators.dhall"
104+
, shouldParse
105+
"annotations"
106+
"./tests/parser/annotations.dhall"
107+
, shouldParse
108+
"merge"
109+
"./tests/parser/merge.dhall"
110+
, shouldParse
111+
"constructors"
112+
"./tests/parser/constructors.dhall"
113+
, shouldParse
114+
"fields"
115+
"./tests/parser/fields.dhall"
116+
, shouldParse
117+
"record"
118+
"./tests/parser/record.dhall"
119+
, shouldParse
120+
"union"
121+
"./tests/parser/union.dhall"
122+
, shouldParse
123+
"list"
124+
"./tests/parser/list.dhall"
125+
, shouldParse
126+
"builtins"
127+
"./tests/parser/builtins.dhall"
128+
, shouldParse
129+
"import alternatives"
130+
"./tests/parser/importAlt.dhall"
131+
, shouldParse
132+
"large expression"
133+
"./tests/parser/largeExpression.dhall"
134+
, shouldParse
135+
"names that begin with reserved identifiers"
136+
"./tests/parser/reservedPrefix.dhall"
137+
, shouldParse
138+
"interpolated expressions with leading whitespace"
139+
"./tests/parser/template.dhall"
140+
, shouldNotParse
141+
"records with duplicate fields"
142+
"./tests/parser/failure/duplicateFields.dhall"
143+
, shouldParse
144+
"collections with type annotations containing imports"
145+
"./tests/parser/collectionImportType.dhall"
146+
, shouldParse
147+
"a parenthesized custom header import"
148+
"./tests/parser/parenthesizeUsing.dhall"
149+
, shouldNotParse
150+
"accessing a field of an import without parentheses"
151+
"./tests/parser/failure/importAccess.dhall"
152+
, shouldParse
153+
"Sort"
154+
"./tests/parser/sort.dhall"
152155
]
153156

154157
shouldParse :: Text -> FilePath -> TestTree

‎tests/QuickCheck.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Chunks s a) where
129129
shrink = genericShrink
130130

131131
instance Arbitrary Const where
132-
arbitrary = Test.QuickCheck.oneof [ pure Type, pure Kind ]
132+
arbitrary = Test.QuickCheck.oneof [ pure Type, pure Kind, pure Sort ]
133133

134134
shrink = genericShrink
135135

‎tests/TypeCheck.hs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,9 @@ typecheckTests =
4646
, should
4747
"correctly handle α-equivalent merge alternatives"
4848
"mergeEquivalence"
49-
49+
, should
50+
"allow Kind variables"
51+
"kindParameter"
5052
, shouldNotTypeCheck
5153
"combining records of terms and types"
5254
"failure/combineMixedRecords"

‎tests/parser/sort.dhall‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Sort

0 commit comments

Comments
 (0)