arrows pointing right and left

Duality


email Scott Turner
home
Ambidexter

rationale

product/sum types
duality
pitfalls avoided

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 → type2type1 ↚ type2
¬ type
T
( type )
( ∧ type1 ∧ type2 ∧ )( ∨ type1 ∨ type2 ∨ )

Duality of Expressions

termscoterms
& term & term &| coterm | coterm |
  
[ coterm ]( term )
@ identifier :> term@ identifier <: coterm
copattern <+ term $ cotermpattern -> term $ coterm
\ pattern -> term\ copattern <+ coterm
term termcoterm coterm
{ term =: pattern ; term }{ coterm =: copattern ; coterm }
identifieridentifier
( term )[ coterm ]

patternscopatterns
& pattern & pattern &| copattern | copattern |
  
[ copattern ]( pattern )
@ type :> pattern@ type <: copattern
identifieridentifier
( pattern )[ copattern ]

Support open standards!  
Valid XHTML 1.0!