|
|
|
This presents the duality of values, covalues, and their types, as exhibited by the Ambidexter programming language.
Duality of Types
| self-dual | |
|---|
∀ T . type | | ∃ T . type |
| \ T . type | |
| type1 type2 | |
type1 → type2 | | type1 ↚ type2 |
| ¬ type | |
| T | |
| ( type ) | |
( ∧ type1 ∧ type2 ∧ ) | | ( ∨ type1 ∨ type2 ∨ ) |
Duality of Expressions
| terms | coterms |
|---|
& term & term & | | coterm | coterm | |
| |
[ coterm ] | ( term ) |
@ identifier :> term | @ identifier <: coterm |
copattern <+ term $ coterm | pattern -> term $ coterm |
\ pattern -> term | \ copattern <+ coterm |
term term | coterm coterm |
{ term =: pattern ; term } | { coterm =: copattern ; coterm } |
identifier | identifier |
( term ) | [ coterm ] |
| patterns | copatterns |
|---|
& pattern & pattern & | | copattern | copattern | |
| |
[ copattern ] | ( pattern ) |
@ type :> pattern | @ type <: copattern |
identifier | identifier |
( pattern ) | [ copattern ] |
|
