The following examples, from Codatatypes in ML, clearly show the duality between inductive and coinductive datatypes. It should be noted that constructor disjunction (i.e., |) becomes destructor conjunction (i.e., &) and of becomes is. This is the same as saying that the arrows point in the other direction. In other words, of indicates an arrow type from the type of argument of the constructor (A) to the datatype we are defining (e.g., A -> T) and is indicates an arrow type from the datatype we are defining to the destructor argument type (T -> A).

Inductive and coinductive types:

datatype T = c1 of A1 | ... | cn of An

c1 : A1 -> T
...
cn : An -> T

codatatype S = d1 is B1 & ... & dn is Bn

d1 : T -> B1
...
dn : T -> Bn

Examples:

datatype 'a + 'b = inl of 'a | inr of 'b

inl : 'a -> 'a + 'b
inr : 'b -> 'a + 'b

codatatype 'a * 'b = fst is 'a & snd is 'b

fst : 'a * 'b -> 'a
snd : 'a * 'b -> 'b

Merge control structure:

The merge construct is the dual of case ... of. Whereas case... of is a destructor for inductive types, merge is a constructor for coinductive types.

          e1:B1 ... en:Bn
-------------------------------------
(merge d1 <= e1 & ... & dn <= en) : S

(merge fst <= 1 & snd <= 2) : int * int

Without the merge construct, it is not possible to construct coinductive types unless a constructor is provided as a primitive in the language.

Tags: type theory