Existential types in record constructors

[AshleyYakeley]

Extend record constructors (#150) to have existential types and subtype relations.

• type T - +
• type storable T + +
• subtype P <: Q

Examples:

datatype Machine -a +b of
    MkMachine of
    type S;
    initial: S;
    step: a -> S -> S *: b;
    end;
end

runMachine: Machine a b -> List a -> List b =
    fn MkMachine => let
        run = fn olds => match
            [] => [];
            a :: aa => let
                (news,b) = step a olds;
                bb = run news;
                in b :: bb;
            end;
        in run initial

runningSum: Machine Integer Integer =
    MkMachine of
    type S = Integer;
    initial = 0;
    step = fns a s => let b = a+s in (b,b);
    end;

Note types can have any kind:

datatype R of
    MkR of
    type S - + {-,+};
    ...
    end;
end

[AshleyYakeley]

Type escape issue:

let

datatype R of
    MkR of
        type T
        v: T -> Action T
    end;
end;

f = fn MkR => v;

r1: R
= MkR of
    type T = Integer;
    v = fn _ => return 0;
end;

r2: R
= MkR of
    type T = Text;
    v = fn t => writeLn stdout (t <> "!") >> return t
end;

in f r1 undefined >>= f r2

f cannot be given a type. Solution: when matching a record pattern over an expression, examine the type of the expression to ensure it does not contain existential types defined in the record.

[AshleyYakeley]

• requires Type Synonyms #47.

[AshleyYakeley]

Idea: distinguish upper case and lower case:

type T

• Can be any kind, e.g. type T +a -b {-c,+d}
• No inference, must be specified by user

type t (#312)

• kind * only
• Doesn't need to be specified, can be inferred

record functions

rf: t of type t; f: a -> (t *: Maybe a) end

Type of rf is effectively forall t. (forall a. a -> (t *: Maybe a)) -> t

record constructors

datatype R +t of Mk of type t; f: a -> (t *: Maybe a) end end