Type inference is a judgment of the form:
Ξ β’ t : T
... where:
Ξ(an input context) is the type inference context which relates identifiers to their typest(an input expression) is the term to infer the type ofT(the output expression) is the inferred type
Type inference also type-checks the input expression, too, to ensure that it is well-typed.
To infer the type of a closed expression, supply an empty context:
Ξ΅ β’ t : T
This judgment guarantees the invariant that the inferred type is safe to normalize.
- Normalization
- Constants
- Variables
BoolNaturalTextDate/Time/TimeZoneListOptional- Records
- Unions
withexpressionsIntegerDouble- Functions
letexpressions- Type annotations
- Assertions
- Nested record updates
- Imports
Types inferred according to the following rules will be in Ξ²-normal form, provided that
all types in the input context Ξ are in Ξ²-normal form.
The advantage of Ξ²-normalizing all inferred types is that repeated normalization of the
same types can largely be avoided.
However implementations MAY choose to infer types that are not Ξ²-normalized as long as they are equivalent to the types specified here.
The first rules are that the inferred type of Type is Kind and the inferred
type of Kind is Sort:
βββββββββββββββ
Ξ β’ Type : Kind
βββββββββββββββ
Ξ β’ Kind : Sort
In other words, Kind is the "type of types" and Sort serves as the
foundation of the type system.
Note that you cannot infer the type of Sort as there is nothing above Sort
in the type system's hierarchy. Inferring the type of Sort is a type error.
Infer the type of a variable by looking up the variable's type in the context:
Ξ β’ T : k
ββββββββββββββββββ
Ξ, x : T β’ x@0 : T
Since x is a synonym for x@0, you can shorten this rule to:
Ξ β’ T : k
ββββββββββββββββ
Ξ, x : T β’ x : T
The order of types in the context matters because there can be multiple type annotations in the context for the same variable. The DeBruijn index associated with each variable disambiguates which type annotation in the context to use:
Ξ β’ x@n : T
ββββββββββββββββββββββββ ; 0 < n
Ξ, x : A β’ x@(1 + n) : T
Ξ β’ x@n : T
ββββββββββββββββββ ; x β y
Ξ, y : A β’ x@n : T
If the natural number associated with the variable is greater than or equal to the number of type annotations in the context matching the variable then that is a type error.
Bool is a Type:
βββββββββββββββ
Ξ β’ Bool : Type
True and False have type Bool:
βββββββββββββββ
Ξ β’ True : Bool
ββββββββββββββββ
Ξ β’ False : Bool
An if expression takes a predicate of type Bool and returns either the
then or else branch of the expression, both of which must be the same type:
Ξ β’ t : Bool
Ξ β’ l : L
Ξ β’ r : R
Ξ β’ L : cβ
Ξ β’ R : cβ
L β‘ R
ββββββββββββββββββββββββββ
Ξ β’ if t then l else r : L
If either branch of the if expression is not a term, type, or kind, then that is a type error.
If the predicate is not a Bool then that is a type error.
If the two branches of the if expression do not have the same type then that
is a type error.
All of the logical operators take arguments of type Bool and return a result
of type Bool:
Ξ β’ l : Bool Ξ β’ r : Bool
βββββββββββββββββββββββββββ
Ξ β’ l || r : Bool
Ξ β’ l : Bool Ξ β’ r : Bool
βββββββββββββββββββββββββββ
Ξ β’ l && r : Bool
Ξ β’ l : Bool Ξ β’ r : Bool
βββββββββββββββββββββββββββ
Ξ β’ l == r : Bool
Ξ β’ l : Bool Ξ β’ r : Bool
βββββββββββββββββββββββββββ
Ξ β’ l != r : Bool
If the operator arguments do not have type Bool then that is a type error.
Natural is a type:
ββββββββββββββββββ
Ξ β’ Natural : Type
Natural number literals have type Natural:
βββββββββββββββ
Ξ β’ n : Natural
The arithmetic operators take arguments of type Natural and return a result of
type Natural:
Ξ β’ x : Natural Ξ β’ y : Natural
βββββββββββββββββββββββββββββββββ
Ξ β’ x + y : Natural
Ξ β’ x : Natural Ξ β’ y : Natural
βββββββββββββββββββββββββββββββββ
Ξ β’ x * y : Natural
If the operator arguments do not have type Natural then that is a type error.
The built-in functions on Natural numbers have the following types:
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ Natural/build : (β(natural : Type) β β(succ : natural β natural) β β(zero : natural) β natural) β Natural
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ Natural/fold : Natural β β(natural : Type) β β(succ : natural β natural) β β(zero : natural) β natural
βββββββββββββββββββββββββββββββββββ
Ξ β’ Natural/isZero : Natural β Bool
βββββββββββββββββββββββββββββββββ
Ξ β’ Natural/even : Natural β Bool
ββββββββββββββββββββββββββββββββ
Ξ β’ Natural/odd : Natural β Bool
βββββββββββββββββββββββββββββββββββββββββ
Ξ β’ Natural/toInteger : Natural β Integer
βββββββββββββββββββββββββββββββββ
Ξ β’ Natural/show : Natural β Text
ββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ Natural/subtract : Natural β Natural β Natural
Text is a type:
βββββββββββββββ
Ξ β’ Text : Type
Text literals have type Text:
ββββββββββββββ
Ξ β’ "s" : Text
Ξ β’ t : Text Ξ β’ "ssβ¦" : Text
βββββββββββββββββββββββββββββββ
Ξ β’ "s${t}ssβ¦" : Text
The Text show function has the following type:
βββββββββββββββββββββββββββ
Ξ β’ Text/show : Text β Text
The Text/replace function has the following type:
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ Text/replace : β(needle : Text) β β(replacement : Text) β β(haystack : Text) β Text
The Text concatenation operator takes arguments of type Text and returns a
result of type Text:
Ξ β’ x : Text Ξ β’ y : Text
βββββββββββββββββββββββββββ
Ξ β’ x ++ y : Text
If the operator arguments do not have type Text, then that is a type error.
Date, Time, and TimeZone are all Types:
βββββββββββββββ
Ξ β’ Date : Type
βββββββββββββββ
Ξ β’ Time : Type
βββββββββββββββββββ
Ξ β’ TimeZone : Type
Date literals have type Date:
βββββββββββββββββββββ
Ξ β’ YYYY-MM-DD : Date
Time literals have type Time:
βββββββββββββββββββ
Ξ β’ hh:mm:ss : Time
β¦ and TimeZone literals have type TimeZone:
βββββββββββββββββββββ
Ξ β’ Β±HH:MM : TimeZone
List is a function from a Type to another Type:
ββββββββββββββββββββββ
Ξ β’ List : Type β Type
A List literal's type is inferred either from the type of the elements (if
non-empty) or from the type annotation (if empty):
Ξ β’ Tβ : c Tβ β₯ List Tβ Ξ β’ Tβ : Type
βββββββββββββββββββββββββββββββββββββββββ
Ξ β’ ([] : Tβ) : List Tβ
Ξ β’ t : Tβ Ξ β’ Tβ : Type Ξ β’ [ tsβ¦ ] : List Tβ Tβ β‘ Tβ
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ [ t, tsβ¦ ] : List Tβ
Note that the above rules forbid List elements that are Types. More
generally, if the element type is not a Type then that is a type error.
If the list elements do not all have the same type then that is a type error.
If an empty list does not have a type annotation then that is a type error.
The List concatenation operator takes arguments that are both Lists of the
same type and returns a List of the same type:
Ξ β’ x : List Aβ
Ξ β’ y : List Aβ
Aβ β‘ Aβ
βββββββββββββββββββ
Ξ β’ x # y : List Aβ
If the operator arguments are not Lists, then that is a type error.
If the arguments have different element types, then that is a type error.
The built-in functions on Lists have the following types:
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/build : β(a : Type) β (β(list : Type) β β(cons : a β list β list) β β(nil : list) β list) β List a
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/fold : β(a : Type) β List a β β(list : Type) β β(cons : a β list β list) β β(nil : list) β list
ββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/length : β(a : Type) β List a β Natural
βββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/head : β(a : Type) β List a β Optional a
βββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/last : β(a : Type) β List a β Optional a
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/indexed : β(a : Type) β List a β List { index : Natural, value : a }
ββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ List/reverse : β(a : Type) β List a β List a
Optional is a function from a Type to another Type:
ββββββββββββββββββββββββββ
Ξ β’ Optional : Type β Type
The Some constructor infers the type from the provided argument:
Ξ β’ a : A Ξ β’ A : Type
ββββββββββββββββββββββββ
Ξ β’ Some a : Optional A
... and the None constructor is an ordinary function that is typeable in
isolation:
βββββββββββββββββββββββββββββββββββ
Ξ β’ None : β(A : Type) β Optional A
Note that the above rules forbid an Optional element that is a Type. More
generally, if the element type is not a Type then that is a type error.
Record types are "anonymous", meaning that they are uniquely defined by the names and types of their fields.
An empty record is a Type:
βββββββββββββ
Ξ β’ {} : Type
A non-empty record can store terms, types and kinds:
Ξ β’ T : tβ Ξ β’ { xsβ¦ } : tβ tβ β tβ = tβ
ββββββββββββββββββββββββββββββββββββββββββββ ; x β { xsβ¦ }
Ξ β’ { x : T, xsβ¦ } : tβ
If the type of a field is not Type, Kind, or Sort then that is a type
error.
Carefully note that there should be no need to handle duplicate fields by this point because the desugaring rules for record literals merge duplicate fields into unique fields.
Record values are also anonymous. The inferred record type has sorted fields and normalized field types.
ββββββββββββ
Ξ β’ {=} : {}
Π⒠t : T Π⒠{ xs⦠} : { ts⦠} Π⒠{ x : T, ts⦠} : i
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ ; x β { xsβ¦ }
Π⒠{ x = t, xs⦠} : { x : T, ts⦠}
You can only select field(s) from the record if they are present:
Π⒠e : { x : T, xs⦠}
ββββββββββββββββββββββ
Ξ β’ e.x : T
Π⒠e : { ts⦠}
βββββββββββββββ
Ξ β’ e.{} : {}
Ξ β’ e : { x : T, tsββ¦ } Ξ β’ e.{ xsβ¦ } : { tsββ¦ }
ββββββββββββββββββββββββββββββββββββββββββββββββββ ; x β { xsβ¦ }
Ξ β’ e.{ x, xsβ¦ } : { x : T, tsββ¦ }
Record projection can also be done by specifying the target record type.
For instance, provided that s is a record type and e is the source record,
e.(s) produces another record of type s whose values are taken from the
respective fields from e.
Π⒠e : { ts⦠}
Ξ β’ s : c
s β₯ {}
βββββββββββββββ
Ξ β’ e.(s) : {}
Ξ β’ e : { x : Tβ, tsβ¦ }
Ξ β’ s : c
s β₯ { x : Tβ, ssβ¦ }
Tβ β‘ Tβ
Π⒠e.({ ss⦠}) : U
βββββββββββββββββββββββββββ
Ξ β’ e.(s) : { x : Tβ, ssβ¦ }
If you select a field from a value that is not a record, then that is a type error.
If the field is absent from the record then that is a type error.
Non-recursive right-biased merge also requires that both arguments are records:
Π⒠l : { ls⦠}
Ξ β’ r : {}
βββββββββββββββββββ
Π⒠l ⫽ r : { ls⦠}
Π⒠l : { ls⦠}
Π⒠r : { a : A, rs⦠}
Π⒠{ ls⦠} ⫽ { rs⦠} : { ts⦠}
βββββββββββββββββββββββββββββββ ; a β ls
Π⒠l ⫽ r : { a : A, ts⦠}
Ξ β’ l : { a : Aβ, lsβ¦ }
Ξ β’ r : { a : Aβ, rsβ¦ }
Π⒠{ ls⦠} ⫽ { rs⦠} : { ts⦠}
βββββββββββββββββββββββββββββββ
Ξ β’ l β«½ r : { a : Aβ, tsβ¦ }
If the operator arguments are not records then that is a type error.
Recursive record type merge requires that both arguments are record type literals. Any conflicting fields must be safe to recursively merge:
Ξ β’ l : t
Ξ β’ r : Type
l β₯ { lsβ¦ }
r β₯ {}
βββββββββββββ
Ξ β’ l β© r : t
Ξ β’ l : tβ
Ξ β’ r : tβ
l β₯ { lsβ¦ }
r β₯ { a : A, rsβ¦ }
Π⒠{ ls⦠} ⩠{ rs⦠} : t
tβ β tβ = tβ
βββββββββββββββββββββββββ ; a β ls
Ξ β’ l β© r : tβ
Ξ β’ l : tβ
Ξ β’ r : tβ
l β₯ { a : Aβ, lsβ¦ }
r β₯ { a : Aβ, rsβ¦ }
Ξ β’ Aβ β© Aβ : Tβ
Ξ β’ { lsβ¦ } β© { rsβ¦ } : Tβ
tβ β tβ = tβ
ββββββββββββββββββββββββββ
Ξ β’ l β© r : tβ
If the operator arguments are not record types then that is a type error.
If they share a field in common that is not a record type then that is a type error.
Recursive record merge requires that the types of both arguments can be combined with recursive record merge:
Ξ β’ l : Tβ
Ξ β’ r : Tβ
Ξ β’ Tβ β© Tβ : i
Tβ β© Tβ β₯ Tβ
βββββββββββββββ
Ξ β’ l β§ r : Tβ
The toMap operator can be applied only to a record value, and every field
of the record must have the same type, which in turn must be a Type.
Π⒠e : { x : T, xs⦠}
Π⒠( toMap { xs⦠} : List { mapKey : Text, mapValue : T } ) : List { mapKey : Text, mapValue : T }
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ toMap e : List { mapKey : Text, mapValue : T }
Ξ β’ e : {} Ξ β’ Tβ : Type Tβ β₯ List { mapKey : Text, mapValue : Tβ }
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ ( toMap e : Tβ ) : List { mapKey : Text, mapValue : Tβ }
Ξ β’ toMap e : Tβ Tβ β‘ Tβ
ββββββββββββββββββββββββββ
Ξ β’ ( toMap e : Tβ ) : Tβ
You can complete a record literal using the record completion operator (T::r),
which is syntactic sugar for (T.default β«½ r) : T.Type. The motivation for
this operator is to easily create records without having to explicitly specify
default-valued fields.
In other words, given a a record T containing the following fields:
- A
Typefield with a record type - A
defaultfield with default fields for the record type
... then T::r creates a record of type T.Type by extending the default
fields from T.default with the fields provided by r, overriding if
necessary.
To type-check a record completion, desugar the operator and type-check the desugared form:
Ξ β’ ((T.default β«½ r) : T.Type) : U
ββββββββββββββββββββββββββββββββββ
Ξ β’ T::r : U
Union types are "anonymous", meaning that they are uniquely defined by the names and types of their alternatives.
An empty union is a Type:
βββββββββββββ
Ξ β’ <> : Type
A non-empty union can have alternatives of terms, types and kinds:
Ξ β’ T : tβ Ξ β’ < xsβ¦ > : tβ tβ β tβ = tβ
βββββββββββββββββββββββββββββββββββββββββββ ; x β { xsβ¦ }
Ξ β’ < x : T | xsβ¦ > : tβ
A union type may contain alternatives without an explicit type label:
Π⒠< ts⦠> : c
βββββββββββββββββββ ; x β < tsβ¦ >
Π⒠< x | ts⦠> : c
Note that the above rule allows storing values, types, and kinds in
unions. However, if the type of the alternative is not Type,
Kind, or Sort then that is a type error.
If two alternatives share the same name then that is a type error.
If a union alternative is non-empty, then the corresponding constructor is a function that wraps a value of the appropriate type:
Ξ β’ u : c u β₯ < x : T | tsβ¦ > β(1, x, 0, < x : T | tsβ¦ >) = U
βββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ u.x : β(x : T) β U
If a union alternative is empty, then the corresponding constructor's type is the same as the original union type:
Ξ β’ u : c u β₯ < x | tsβ¦ >
βββββββββββββββββββββββββββ
Π⒠u.x : < x | ts⦠>
A merge expression is well-typed if there is a one-to-one correspondence
between the fields of the handler record and the alternatives of the union:
Ξ β’ t : {} Ξ β’ u : <> Ξ β’ T : Type
ββββββββββββββββββββββββββββββββββββββ
Ξ β’ (merge t u : T) : T
Ξ β’ merge t u : Tβ Tβ β‘ Tβ
ββββββββββββββββββββββββββββ
Ξ β’ (merge t u : Tβ) : Tβ
We use a trick to recursively check that all handlers have the same output type:
Based on the types of the remaining fields and alternatives, we "invent" values
(tβ and uβ) from which we can create the smaller merge expression.
An implementation could simply loop over the inferred record type.
Ξ β’ tβ : { y : β(x : Aβ) β Tβ, tsβ¦ }
Ξ β’ uβ : < y : Aβ | usβ¦ >
Aβ β‘ Aβ
Ξ β’ tβ : { tsβ¦ }
Ξ β’ uβ : < usβ¦ >
β(-1, x, 0, Tβ) = Tβ
Ξ β’ (merge tβ uβ : Tβ) : Tβ
ββββββββββββββββββββββββββββββββββββ ; `x` not free in `Tβ`
Ξ β’ merge tβ uβ : Tβ
Ξ β’ tβ : { y : Tβ, tsβ¦ }
Ξ β’ uβ : < y | usβ¦ >
Ξ β’ tβ : { tsβ¦ }
Ξ β’ uβ : < usβ¦ >
Ξ β’ (merge tβ uβ : Tβ) : Tβ
βββββββββββββββββββββββββββββββββββββ
Ξ β’ merge tβ uβ : Tβ
Optionals can also be merged as if they had type < None | Some : A >:
Ξβ β’ o : Optional A
β(1, x, 0, (Ξβ, x : < None | Some : A >)) = Ξβ
Ξβ β’ merge t x : T
ββββββββββββββββββββββββββββββββββ
Ξ β’ merge t o : T
If the first argument of a merge expression is not a record then that is a
type error.
If the second argument of a merge expression is not a union or an Optional
then that is a type error.
If you merge an empty union without a type annotation then that is a type
error.
If the merge expression has a type annotation that is not a Type then that
is a type error.
If there is a handler without a matching alternative then that is a type error.
If there is an alternative without a matching handler then that is a type error.
If a handler is not a function and the corresponding union alternative is non-empty, then that is a type error.
If the handler's input type does not match the corresponding alternative's type then that is a type error.
If there are two handlers with different output types then that is a type error.
If a merge expression has a type annotation that doesn't match every handler's
output type then that is a type error.
A showConstructor expression with a union or an Optional as its first
argument has type Text.
Π⒠e : < ts⦠>
ββββββββββββββββββββββββββββββ
Ξ β’ showConstructor e : Text
Ξ β’ o : Optional A
ββββββββββββββββββββββββββββ
Ξ β’ showConstructor o : Text
If the first argument of a showConstructor expression is not a union or an
Optional then that is a type error.
A record update using the with keyword replaces a field:
Ξ β’ e : { k : Tβ, tsβ¦ }
Ξ β’ v : Tβ
ββββββββββββββββββββββββββββββββββ
Ξ β’ e with k = v : { k : Tβ, tsβ¦ }
Π⒠e : { ts⦠}
Ξ β’ v : T
βββββββββββββββββββββββββββββββββ ; k β ts
Π⒠e with k = v : { k : T, ts⦠}
... and record updates can be nested, creating intermediate records if necessary:
Ξ β’ e : { kβ : Tβ, tsβ¦ }
Ξ β’ e.kβ with kβ.ksβ¦ = v : Tβ
βββββββββββββββββββββββββββββββββββββββββββ
Ξ β’ e with kβ.kβ.ksβ¦ = v : { kβ : Tβ, tsβ¦ }
Π⒠e : { ts⦠}
Ξ β’ {=} with kβ.ksβ¦ = v : Tβ
βββββββββββββββββββββββββββββββββββββββββββ ; kβ β ts
Ξ β’ e with kβ.kβ.ksβ¦ = v : { kβ : Tβ, tsβ¦ }
An Optional update using the with keyword must preserve the type of the "inner" value.
Ξ β’ e : Optional T
Ξ β’ v : T
ββββββββββββββββββββββββββββββββββ
Π⒠e with ?.ks⦠= v : Optional T
If the expression being updated (i.e. the e in e with ks⦠= v) is not a
record or an Optional then that is a type error.
Integer is a type:
ββββββββββββββββββ
Ξ β’ Integer : Type
Integer literals have type Integer:
ββββββββββββββββ
Ξ β’ Β±n : Integer
The built-in functions on Integer have the following types:
βββββββββββββββββββββββββββββββββ
Ξ β’ Integer/show : Integer β Text
βββββββββββββββββββββββββββββββββββββββ
Ξ β’ Integer/toDouble : Integer β Double
ββββββββββββββββββββββββββββββββββββββ
Ξ β’ Integer/negate : Integer β Integer
βββββββββββββββββββββββββββββββββββββ
Ξ β’ Integer/clamp : Integer β Natural
Double is a type:
ββββββββββββββββββ
Ξ β’ Double : Type
Double literals have type Double:
ββββββββββββββββ
Ξ β’ n.n : Double
The built-in Double/show function has the following type:
βββββββββββββββββββββββββββββββ
Ξ β’ Double/show : Double β Text
A function type is only well-typed if the input and output type are well-typed and if the inferred input and output type are allowed by the function check:
Ξβ β’ A : i β(1, x, 0, (Ξβ, x : A)) = Ξβ Ξβ β’ B : o i β o : c
ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
Ξβ β’ β(x : A) β B : c
If the input or output type is neither a Type, a Kind, nor a Sort then
that is a type error.
An unquantified function type A β B is a short-hand for β(_ : A) β B. Note
that the _ does not denote some unused type variable but rather denotes the
specific variable named _ (which is a valid variable name and this variable
named _ may in fact be present within B). For example, this is a well-typed
judgment:
Ξ΅ β’ Type β β(x : _) β _ : Type
... because it is equivalent to:
Ξ΅ β’ β(_ : Type) β β(x : _) β _ : Type
The type of a Ξ»-expression is a function type whose input type (A) is the same
as the type of the bound variable and whose output type (B) is the same as the
inferred type of the body of the Ξ»-expression (b).
Ξβ β’ Aβ : cβ
Aβ β₯ Aβ
β(1, x, 0, (Ξβ, x : Aβ)) = Ξβ
Ξβ β’ b : B
Ξβ β’ β(x : Aβ) β B : cβ
ββββββββββββββββββββββββββββββββββ
Ξβ β’ Ξ»(x : Aβ) β b : β(x : Aβ) β B
Note that the above rule requires that the inferred function type must be well-typed.
The type system ensures that function application is well-typed, meaning that the input type that a function expects matches the inferred type of the function's argument:
Ξ β’ f : β(x : Aβ) β Bβ
Ξ β’ aβ : Aβ
Aβ β‘ Aβ
β(1, x, 0, aβ) = aβ
Bβ[x β aβ] = Bβ
β(-1, x, 0, Bβ) = Bβ
Bβ β₯ Bβ
ββββββββββββββββββββββ
Ξ β’ f aβ : Bβ
If the function does not have a function type, then that is a type error.
If the inferred input type of the function does not match the inferred type of the function argument then that is a type error.
For the purposes of type-checking, an expression of the form:
let x : A = aβ in bβ
... is not semantically identical to:
(Ξ»(x : A) β bβ) aβ
let differs in behavior in order to support "type synonyms", such as:
let t : Type = Natural in 1 : t
If you were to desugar that to:
(Ξ»(t : Type) β 1 : t) Natural
... then that would not be a well-typed expression, even though the let
expression would be well-typed.
Ξ β’ aβ : Aβ
Ξ β’ Aβ : i
Aβ β‘ Aβ
aβ β₯ aβ
β(1, x, 0, aβ) = aβ
bβ[x β aβ] = bβ
β(-1, x, 0, bβ) = bβ
Ξ β’ bβ : B
βββββββββββββββββββββββββββββ
Ξ β’ let x : Aβ = aβ in bβ : B
Ξ β’ aβ : A
aβ β₯ aβ
β(1, x, 0, aβ) = aβ
bβ[x β aβ] = bβ
β(-1, x, 0, bβ) = bβ
Ξ β’ bβ : B
ββββββββββββββββββββββββ
Ξ β’ let x = aβ in bβ : B
If the let expression has a type annotation that doesn't match the type of
the right-hand side of the assignment then that is a type error.
Type-checking an annotated expression verifies that the annotation matches the inferred type of the annotated expression, and returns the inferred type as the type of the whole expression:
Ξ β’ Tβ : i Ξ β’ t : Tβ Tβ β‘ Tβ
βββββββββββββββββββββββββββββββββ
Ξ β’ (t : Tβ) : Tβ
Note that the above rule permits kind annotations, such as List : Type β Type.
If the inferred type of the annotated expression does not match the type annotation then that is a type error.
Even though Sort is not a type-valid expression by itself, it is valid
as a type annotation:
Ξ β’ t : Sort
βββββββββββββββββββββ
Ξ β’ (t : Sort) : Sort
An assertion is equivalent to built-in language support for checking two expressions for judgmental equality, commonly invoked like this:
let example = assert : (2 + 2) === 4
in β¦
An assertion checks that:
- The type annotation is an equivalence
- The two sides of the equivalence are in fact equivalent
... or in other words:
Ξ β’ T : Type
T β₯ x === y
x β‘ y
ββββββββββββββββββββββββββ
Ξ β’ (assert : T) : x === y
The inferred type of an assertion is the same as the provided annotation.
If the annotation is not an equivalence then that is a type error.
If the two sides of the equivalence are not equivalent then that is a type error.
To type-check an equivalence, verify that the two sides are terms:
Ξ β’ x : Aβ
Ξ β’ y : Aβ
Ξ β’ Aβ : Type
Ξ β’ Aβ : Type
Aβ β‘ Aβ
ββββββββββββββββββ
Ξ β’ x === y : Type
If either side of the equivalence is not a term, then that is a type error.
If the inferred types do not match, then that is also a type error.
An expression with unresolved imports cannot be type-checked