5 | | |
6 | | |
7 | | [[br]] |
8 | | == Binders == |
9 | | |
10 | | {{{ |
11 | | BINDER |
12 | | ::= NAMEDVAR | HAT | UNDERSCORE |
13 | | }}} |
14 | | |
15 | | 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. |
16 | | |
17 | | * During type checking, evaluation and optimisation, named variables can be rewritten to debruijn indices to avoid name capture. |
18 | | |
19 | | [[br]] |
20 | | == Types == |
21 | | We use the same syntax of "types" for terms of the Spec, Kind and Sort universes. |
22 | | |
23 | | {{{ |
24 | | TYPE |
25 | | ::= VAR |
26 | | | CON |
27 | | | TYPE TYPE |
28 | | | [ BINDER+ : TYPE ] . TYPE |
29 | | | ( TYPE ) |
30 | | |
31 | | (type sums) |
32 | | | TYPE + TYPE |
33 | | | !0 |
34 | | | $0 |
35 | | |
36 | | (arrow types) |
37 | | | TYPE ~> TYPE |
38 | | | TYPE => TYPE |
39 | | | TYPE -> TYPE |
40 | | | TYPE -(TYPE | TYPE)> TYPE |
41 | | }}} |
42 | | |
43 | | A type can be a variable, constructor, universally quantified type, type application, parenthesised type, type sum or arrow type. |
44 | | |
45 | | A type sum can be the least-upper-bound of two types, the least effect, or the least closure. |
46 | | |
47 | | An arrow type can be the kind arrow, implication, the pure and empty function, or the effectful and closureful function. |
48 | | |
49 | | * The components of a type sum must have effect or closure kind. |
50 | | * The kind arrow and implication arrows must be fully applied. |
51 | | * With the function arrow, the first and last arguments are the parameter and return types. The second and third arguments are the effect and closure of the function. |
52 | | |
53 | | The following type expressions are equivalent: |
54 | | || {{{[BIND1 BIND2 : TYPE1] . TYPE2}}} || = || {{{[BIND1 : TYPE1] . [BIND2 : TYPE1] . TYPE2}}} || |
55 | | || {{{[BIND1 : TYPE1]. TYPE2 TYPE3}}} || = || {{{[BIND1 : TYPE1]. (TYPE2 TYPE3)}}} || |
56 | | || {{{(TYPE)}}} || = || {{{TYPE}}} || |
57 | | || {{{TYPE1 TYPE2 TYPE3}}} || = || {{{(TYPE1 TYPE2) TYPE3}}} || |
58 | | || {{{TYPE1 + TYPE2}}} || = ||{{{TYPE2 + TYPE1}}} || |
59 | | || {{{(TYPE1 + TYPE2) + TYPE3 }}} || = || {{{TYPE1 + (TYPE2 + TYPE3)}}} || |
60 | | || {{{TYPE + !0}}} || = || {{{TYPE}}} || |
61 | | || {{{TYPE + $0}}} || = || {{{TYPE}}} || |
62 | | || {{{TYPE1 ~> TYPE2}}} || = || {{{(~>) TYPE1 TYPE2}}} || |
63 | | || {{{TYPE1 => TYPE2}}} || = || {{{(=>) TYPE1 TYPE2}}} || |
64 | | || {{{TYPE1 -(TYPE2 | TYPE3)> TYPE4}}} || = || {{{(->) TYPE1 TYPE2 TYPE3 TYPE4}}} || |
65 | | || {{{TYPE1 -> TYPE2}}} || = || {{{(->) TYPE1 !0 $0 TYPE2}}} || |
66 | | || {{{TYPE1 ~> TYPE2 ~> TYPE3}}} || = || {{{TYPE1 ~> (TYPE2 ~> TYPE3)}}} || |
67 | | || {{{TYPE1 => TYPE2 => TYPE3}}} || = || {{{TYPE1 => (TYPE2 => TYPE3)}}} || |
68 | | || {{{TYPE1 -> TYPE2 -> TYPE3}}} || = || {{{TYPE1 -> (TYPE2 -> TYPE3)}}} || |
69 | | || {{{TYPE1 -> TYPE2 + TYPE3}}} || = || {{{(TYPE1 -> TYPE2) + TYPE3}}} || |
70 | | |
71 | | |
72 | | |
73 | | Example types: |
74 | | {{{ |
75 | | 1) Int r1 |
76 | | |
77 | | 2) e + Read r1 + Write r2 |
78 | | |
79 | | 3) [r:%]. Int r |
80 | | |
81 | | 4) [a: *]. a -> a |
82 | | |
83 | | 5) [r:%]. [e:!]. [c:$]. [a b:*]. |
84 | | (a -(e | c)> b) -> List r a -(Read r + e | c)> List r b |
85 | | |
86 | | 6) [^^^:%].Int ^2 -> Int ^1 -(Read ^2 + Read ^1 + Alloc ^0 | Use ^2)> Int ^0 |
87 | | }}} |
88 | | |
| 5 | * [wiki:Language/Core/Types Types] |