wiki:Language/Core/Types

Types

We use the same syntax of "types" for terms of the Spec, Kind and Sort universes.

Type ::= Var
      |  Con
      |  Type Type
      |  [ Binder : Type ] . Type

 (type sums)
      |  Type + Type
      |  'Pure'
      |  'Empty'

A type can be a variable, constructor, universally quantified type, type application or type sum.

A type sum can be the least-upper-bound of two types, the least effect Pure, or the least closure Empty

Sugar and Equivalences

The following type expressions are equivalent:

(Type) = Type
Type1 Type2 Type3 = (Type1 Type2) Type3
[Binder1 Binder2 : Type1] . Type2 = [Binder1 : Type1] . [Binder2 : Type1] . Type2
[Binder1 : Type1]. Type2 Type3 = [Binder1 : Type1]. (Type2 Type3)
[Binder1 : Type1]. Type2 + Type3 = ([Binder1 : Type1]. Type2) + Type3
Type1 + Type2 = Type2 + Type1
(Type1 + Type2) + Type3 = Type1 + (Type2 + Type3)
Type + 'Pure' = Type
Type + 'Empty' = Type
Type1 ~> Type2 = (~>) Type1 Type2
Type1 => Type2 = (=>) Type1 Type2
Type1 -(Type2 | Type3)> Type4 = (->) Type1 Type2 Type3 Type4
Type1 -> Type2 = (->) Type1 'Pure' 'Empty' Type2
Type1 ~> Type2 ~> Type3 = Type1 ~> (Type2 ~> Type3)
Type1 => Type2 => Type3 = Type1 => (Type2 => Type3)
Type1 -> Type2 -> Type3 = Type1 -> (Type2 -> Type3)
Type1 -> Type2 + Type3 = (Type1 -> Type2) + Type3

Examples

1)  Int r1

2)  (->) (Int r2)

3)  e + Read r1 + Write r2

4)  [r : Region]. Int r

5)  [a b : Data]. a -> b

6)  [r : Region]. [e : Effect]. [c : Closure]. [a b : Data]. 
      (a -(e | c)> b) -> List r a -(Read r + e | c)> List r b

7)  [^^^:Region].Int ^2 -> Int ^1 -(Read ^2 + Read ^1 + Alloc ^0 | Use ^2)> Int ^0


Binders

Binder ::= NamedVar | '^' | '_'

These are used at binding positions in both types and expressions. The hat ^ binder adds a debruijn index to the stack. The underscore _ is a non-binding binder, or alternatively, is sugar for a named variable that is not free in the body of the binding construct.

  • During type checking, evaluation and optimisation, named variables can be rewritten to debruijn indices to avoid name capture.


History

  • 2013/06: Changed !0 and $0 syntax to Pure and Empty. This was done for consistency after the change of kind constructor syntax from ! and $ to Effect and Closure.
  • 2011/12: Changed syntax of binders from (forall Binder : Type. Type) to ([Binder : Type]. Type). Followed TweLF with this. The square parens don't conflict with anything else in the core language, and the syntax is more compact. Core programs are type heavy, so this matters more in the core language than the source language.
  • 2010/06: Changed syntax of type sums from {Type; Type ... } to Type + Type. Writing effects as sets has an annoying normalisation problem: what to do about nested sets like: { Type; { Type; ...}; Type } . These can be created when substituting effect variables, but the result looks a bit "mis-kinded". Almost changed the syntax of sums to Type \/ Type, but figured Type + Type was cleaner. It then made sense to use !0 and $0 for the least effect and closure terms, which looks ok.
Last modified 3 years ago Last modified on Mar 8, 2014, 5:45:14 AM