Version 6 (modified by benl, 8 years ago) (diff)

--

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
|  !0
|  \$0
```

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

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

• The components of a type sum must have effect or closure kind.
• The kind function constructor (~>) and implication constructor (=>) must be fully applied.
• With the function constructor (->), the first and last arguments are the parameter and return types. The second and third arguments are the effect and closure of the function.

Syntactic Sugar

The following type expressions are equivalent:

 [BIND1 BIND2 : TYPE1] . TYPE2 = [BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2 [BIND1 : TYPE1]. TYPE2 TYPE3 = [BIND1 : TYPE1]. (TYPE2 TYPE3) (TYPE) = TYPE TYPE1 TYPE2 TYPE3 = (TYPE1 TYPE2) TYPE3 TYPE1 + TYPE2 = TYPE2 + TYPE1 (TYPE1 + TYPE2) + TYPE3 = TYPE1 + (TYPE2 + TYPE3) TYPE + !0 = TYPE TYPE + \$0 = TYPE TYPE1 ~> TYPE2 = (~>) TYPE1 TYPE2 TYPE1 => TYPE2 = (=>) TYPE1 TYPE2 TYPE1 -(TYPE2 | TYPE3)> TYPE4 = (->) TYPE1 TYPE2 TYPE3 TYPE4 TYPE1 -> TYPE2 = (->) TYPE1 !0 \$0 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:%]. Int r

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

6)  [r:%]. [e:!]. [c:\$]. [a b:*].
(a -(e | c)> b) -> List r a -(Read r + e | c)> List r b

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

Binders

```BINDER
::= NAMEDVAR | HAT | UNDERSCORE
```

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

• 2011/12: Changed syntax of binders from (forall BIND : TYPE. TYPE) to ([BIND : 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.