Replace Datatypes with Sum Types and Product Types

[AshleyYakeley]

This is almost certainly a bad idea, but I want to record it here anyway.

The basic issue is that datatypes are "sums of products". That is, a datatype is a sum of intermediate types, and an intermediate type is a product of types. This is fine, except that the intermediate product types are not represented as types in Pinafore.

The solution to this problem (likely at great cost to other parts of the language) is to separate out sum types and product types.

Example

sumtype S {
    C1: X;
    C2: Y;
};

# constructors:
C1: X -> S;
C2: Y -> S;

# destructor:
match S {
    C1 => fn x => ...;
    C2 => fn y => ...;
}

producttype P {
    m1: X;
    m2: Y;
};

# destructors:
m1: P -> X;
m2: P -> Y;

# constructor:
P {
    m1 = x;
    m2 = y;
};

Basic Types

producttype Unit {};

sumtype Void {};

sumtype Maybe +a {
    Just: a;
    None: Unit;
};

let rec {
    producttype List1 +a {
        head: a;
        tail: List a;
    };

    sumtype List +a {
        Cons: List1 a;
        Nil: Unit
    };

    subtype List1 a <: List a = Cons;
};

Patterns

C1 x
m1 => x
Cons (head => 1;tail => Cons (head => 2))

Benefits

• C1 and C2 are prisms, m1 and m2 are lenses.
• Easy type extension.

producttype P1 {
    m1: X;
};

producttype P2 <: P1 {
    m2: Y;
};

sumtype S1 {
    C1: X;
};

sumtype S2 :> S1 {
    C2: Y;
};

Costs

• The syntax is awkward.
• For some types, the intermediate types should not be exposed.