## Ambidexter 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!