Open Types

[AshleyYakeley]

Type

opentype T;
namespace T of
constructor Int: Integer -> T;
constructor Other: Bool -> Unit -> T;
end;

Storability

Probably shouldn't allow storable, because:

let
opentype storable S;
c = cell @S !"s" ?store;
(m,checkM) = let
        constructor M: S !"M";
        m: S = M;
        checkM: S -> Bool = match M => True; _ => False; end;
    in (m,checkM);
in do
    c := m;
    found <- get c;
    pure $ checkM found
    end;

Parameters

opentype T +a;
namespace T of
constructor This: Maybe a -> T a;
constructor That: a -> T a;
end;

GADTs

Allowed?

opentype T +a;
namespace T of
constructor IsInt: T Integer;  # allowed?
end;

Int.T: T Integer;
fn Int.T => (): T Integer -> Unit;  # wrong as GADT

GADTs might be possible, save for another issue.

Prereq

• do Rename "open types" to "entity types" #302 first
• do instead of More general dynamic types #300
• use this for Extensible exceptions #299