|
|
|
| type | kind |
|---|
∀ identifier . type |
* |
∃ identifier . type |
* |
\ identifier . type |
* |
¬ type |
* |
type type |
* |
∧ ( type ∧)* |
* |
∨ ( type ∨)* |
* |
True |
* |
False |
* |
String |
* |
Integer |
* |
Boolean |
* |
List |
*→* |
Colist |
*→* |
IO |
*→* |
Type Synonyms
The following types normally are synonyms for basic types described above. The --no-lower-types command line option retains these as distinct types.
| type | kind | equivalence |
|---|
type → type |
* |
S→T ≡ ¬(∧S∧¬T∧) |
type ↚ type |
* |
S↚T ≡ ∧¬S∧T∧ |
IOV |
*→* |
IOV T ≡ IO T |
ION |
*→* |
ION T ≡ ¬IO ¬T |
abstract syntax with type rules
Terms
| term | type |
|---|
'&' ( term:T '&' )* |
∧(T∧)* |
',' ( term:T ',' )* |
List T |
'[' coterm:T ']' |
¬T |
copattern:T '<+' term:S '$' coterm:S |
T |
'\' pattern:S '->' term:T |
S→T |
'@' identifier:Z ':>' term:T(Z) |
∀A.T(A) |
term:S term:S→T |
T |
identifier:Z |
Z |
( ) |
True |
integer |
Integer |
string |
String |
'{' ( term:M S ( '=:' pattern:S )opt ';' )* term:M T '}' |
M T |
Patterns
| pattern | type |
|---|
'&' ( pattern:T '&' )* |
∧(T∧)* |
'&' ( placeholder '&' )* |
∧(T∧)* |
'@' ( type:S ':>' )opt pattern:T(S) |
∀A.T(A) |
identifier:Z |
Z |
( ) |
True |
'[' copattern:T ']' |
¬T |
Coterms
| coterm | type |
|---|
'|' ( coterm:T '|' )* |
∨(T∨)* |
',' ( coterm:T ',' )* |
Colist T |
'(' term:T ')' |
¬T |
pattern:T '->' term:S '$' coterm:S |
T |
'\' copattern:S '<+' coterm:T |
S↚T |
'@' identifier:Z '<:' coterm:T(Z) |
∃A.T(A) |
coterm:S coterm:S↚T |
T |
identifier:Z |
Z |
( ) |
False |
integer |
¬Integer |
string |
¬String |
'{' ( coterm:M S ( '=:' copattern:S )opt ';' )* coterm:M T '}' |
M T |
Note: the type constraints on monadic coterms (i.e. having the {...=:...;...} form)
vary, depending on the --strict-monad and --no-lower-types command
line options.
Copatterns
| copattern | type |
|---|
'|' ( copattern:T '|' )* |
∨(T∨)* |
'|' ( placeholder '|' )* |
∨(T∨)* |
'@' ( type:S '<:' )opt copattern:T(S) |
∃A.T(A) |
identifier:Z |
Z |
( ) |
False |
'(' pattern:T ')' |
¬T |
|
