arrows pointing right and left

Ambidexter types


email Scott Turner
home
Ambidexter

reference

command line
syntax
built-ins
types
typekind
∀ 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.

typekindequivalence
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

termtype
'&' ( 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

patterntype
'&' ( pattern:T '&' )* (T∧)*
'&' ( placeholder '&' )* (T∧)*
'@' ( type:S ':>' )opt pattern:T(S) ∀A.T(A)
identifier:Z Z
( ) True
'[' copattern:T ']' ¬T

Coterms

cotermtype
'|' ( 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

copatterntype
'|' ( copattern:T  '|' )* (T∨)*
'|' ( placeholder '|' )* (T∨)*
'@' ( type:S '<:' )opt copattern:T(S) ∃A.T(A)
identifier:Z Z
( ) False
'(' pattern:T ')' ¬T

Support open standards!  
Valid XHTML 1.0!