Record constructors, similar to ML-style signatures/structures/functors etc.

[AshleyYakeley]

ML example:

signature STACK =
sig
    type 'a t

    val push : 'a t -> 'a -> 'a t
    val pop : 'a t -> 'a option * 'a t
    val size : 'a t -> int
    val empty : 'a t
end

Haskell equivalent as type:

type STACK :: (Type -> Type) -> Type
data STACK t = STACK {
    push :: forall a. t a -> a -> t a,
    pop :: forall a. t a -> (Maybe a, t a),
    size :: forall a. t a -> Int,
    empty :: forall a. t a
}

Haskell equivalent as class:

type STACK :: (Type -> Type) -> Constraint
class STACK t where
    push :: forall a. t a -> a -> t a
    pop :: forall a. t a -> (Maybe a, t a)
    size :: forall a. t a -> Int
    empty :: forall a. t a

Note there can be no Pinafore equivalent as type, because Pinafore disallows kind (* -> *) -> *.

[AshleyYakeley]

Related, but not quite the same:

let
    module M a b c = let
        p = a + b;
        q = c - a;
        in expose p, q;
in let
    using M 3 4 5; # must be fully applied
in p * q;

[AshleyYakeley]

signature STACK of
    type T +a;

    push: T a -> a -> T a;
    pop: T a -> Maybe a *: T a;
    size: T Any -> Integer;
    empty: T None;
end;

structure ListStack: STACK of
    type T = List;
    push = fns s a => a :: s;
    pop = match
        a :: s => (Just a,s)
        s => (Nothing,s)
        end;
    size = length;
    empty = [];
end;

[AshleyYakeley]

Some examples here.

signature ITERABLE of
    type Elem;
    type Collection;
    next: Collection -> Maybe (Elem *: Collection);
end;

signature FOLD of
    type Elem;
    type Collection;
    fold: (Elem *: a -> a) -> a -> Collection -> a
end;

module FoldFunctor(Iter: ITERABLE): FOLD of
    type Elem = Iter.Elem
    type Collection = Iter.Collection
    fold = fns f e xs => Iter.next xs >- match
        Nothing => e;
        Just (x,xs') => fold f (f (x, e)) xs';
        end;
end;

[AshleyYakeley]

Use records?

recordtype ITERABLE of
    type Elem;
    type Collection;
    next: Collection -> Maybe (Elem *: Collection);
end;

recordtype FOLD of
    type Elem;
    type Collection;
    fold: (Elem *: a -> a) -> a -> Collection -> a;
end;

subtype ITERABLE <: FOLD
= fn iter => record
    type Elem = iter.Elem;
    type Collection = iter.Collection;
    fold = fns f e xs => iter.next xs >- match
        Nothing => e;
        Just (x,xs') => fold f (f (x, e)) xs';
        end;
end;

or even

subtype ITERABLE <: FOLD
= fn iter => record
    using iter;
    fold = fns f e xs => next xs >- match
        Nothing => e;
        Just (x,xs') => fold f (f (x, e)) xs';
        end;
end;

[AshleyYakeley]

Haskell equivalent (as datatypes):

data ITERABLE elem collection = MkITERABLE {
    next :: collection -> Maybe (elem, collection);
}

data FOLD elem collection = MkFOLD {
    fold: forall a. ((Elem, a) -> a) -> a -> collection -> a;
}

foldFunctor: ITERABLE elem collection -> FOLD elem collection;
foldFunctor (MkITERABLE next) = MkFOLD {
    fold = \f e xs => case next xa of
        Nothing -> e
        Just (x,xs') -> fold f (f (x,e)) xs'
}

[AshleyYakeley]

...and back to Pinafore:

recordtype ITERABLE +elem {-collp,+collq} of
    next: collp -> Maybe (elem *: collq);
end;

recordtype FOLD +elem -collection of
    fold: (elem *: a -> a) -> a -> collection -> a;
end;

subtype ITERABLE elem collection <: FOLD elem collection
= fn iter => record
    fold = fns f e xs => iter.next xs >- match
        Nothing => e;
        Just (x,xs') => fold f (f (x, e)) xs';
        end;
end;

[AshleyYakeley]

This raises rank-2 questions.

recordtype R of
i: a -> a
end;

f = fn x => record R of
    i = x;
    end;

What is the type of f?

NOT similar to this, which is accepted with type (a -> a) -> a -> a:

f = fn x => let
    i: a -> a = x;
    in i

[AshleyYakeley]

Can we allow datatypes to have rank-2 types?

datatype D of
MkD (a -> a);
end;

No, because MkD cannot be given a type.

[AshleyYakeley]

Can we allow record types to have multiple constructors, like data types?

recordtype R of
    record MkR1 of
    i: a -> a
    end;
    record MkR2 of
    j: (a -> a) -> a -> a
    end;
end;

Possibly, but MkR1 and MkR2 would not be values. Instead construction would look like this:

r: R
= record MkR2 of
j = fns f x => f (f x);
end;

Destruction would look like this:

r >- match
MkR1 => i 3;
MkR2 => j (fn x => x + 1) 5;
end;

For single constructor, we can do:

let
MkR1 = r;
in expr;

(should do #169 first for this tbh.)

Dot syntax: r.i same as r >- fn MkR1 => i (possibly only if R has only one constructor) How does type inference work? What is the type of fn r => r.i?

[AshleyYakeley]

Can we use simpler syntax?

r: R
= let
j = fns f x => f (f x);
in MkR2;

Possibly, but note MkR2 can't be given a type even as an expression.

[AshleyYakeley]

What would this look like for UIStuff? UIStuff/Selection.pinafore:

recordtype UISContext of
    record MkUISContext of
    gtk: GTK.Context;
    store: Storage.Store;
    uh: Undo.UndoHandler;
    end;
end;

runUIStuff: (UISContext -> Action a) -> Action a
= fn call => do
...
end;

recordtype SelectionStuff of
    record MkSelectionStuff of
    stdWindow: WholeModel +Text -> WholeModel +(List MenuItem) -> Element -> Action Window;
    end;
end;

selectionStuff: UISContext -> SelectionStuff
= fn MkUISContext => record MkSelectionStuff of
    stdWindow = ... ;
end;

contacts, etc.:

let
import UIStuff.Selection;
in runUIStuff $
fn uisc@MkUISContext =>
selectionStuff uisc >- fn MkSelectionStuff => 
in do
    window <- stdWindow ...
end;

[AshleyYakeley]

Of course, we could also use subtype relations:

subtype UISContext <: SelectionStuff
= fn MkUISContext => record MkSelectionStuff of
    stdWindow = ... ;
end;

let
import UIStuff.Selection;
in runUIStuff $
fn MkUISContext@MkSelectionStuff =>
in do
    window <- stdWindow ...
end;

[AshleyYakeley]

What about class-type stuff (for types of kind * only, of course)?

recordtype Eq -a of
    record MkEq of
    equal: a -> a -> Boolean;
    end;
end;

recordtype Ord -a of
    record MkOrd of
    compare: a -> a -> Ordering;
    end;
end;

subtype Ord a <: Eq a
= fn MkOrd => record
    equal = fns p q => compare p q >- match
        EQ => True;
        _ => False;
        End;
    end;

[AshleyYakeley]

Possible idea: existential type variables.

recordtype Transformer -a +b of
    record MkTransformer of
    type State;
    initial: State;
    transform: a -> State -> (State,b);
    end;
end;

identityTransformer: Transformer a a
= record MkTransformer of
type State = Unit;
transform = fns a () => ((),a);
end;

composeTransfomer: Transformer b c -> Transformer a b -> Transformer a c
= fns bc ab => record MkTransformer of
type State = bc.State *: ab.State; # wrong, but not sure how to do this
end;

[AshleyYakeley]

The problem here is that ab.transform has type a -> ab.State -> (ab.State *: b). This is fine if ab is a symbol, but for a general expression, expr1.transform cannot be connected with the type expr2.State, without a way of proving expr1 = expr2.

[AshleyYakeley]

In general it's hard to do this:

recordtype R of
    record MkR of
    v: Integer
    end;
end;

addOne: R -> R
= fn r => record
v = r >- fn MkR => v + 1;
end;

[AshleyYakeley]

Possible solution: unpacking record-type constructors into namespaces:

MkR .> A = r

[AshleyYakeley]

Might as well merge record types and data types. Instead, data types now have a new kind of "record" constructor.

[AshleyYakeley]

Existential types lead to the problem of type escape.

let
recordtype R of
record MkR of
type T
v: T -> Action T
end;
end;

f = fn MkR => v;

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

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

in f r1 undefined >>= f1 r2

[AshleyYakeley]

Should do namespaces (#170) first.

[AshleyYakeley]

Should do datatype representation (#171) first.

[AshleyYakeley]

What type does this have?

datatype R of
    MkR of
    f: a -> a
    end
end;

v1 = fn x => MkR of f=x end;

Similarly:

v2 = fn x => let f: a -> a = x in f

[AshleyYakeley]

v3 = fn x => let y: a -> a = x in (y 3, y "text");
v4 = fn x => let y = x in (y 3,y "text");

gives

v3: ((Integer | Text | a) -> a) -> (a | Integer) *: (a | Text);
v4: ((Integer | Text) -> a) -> a *: a;

[AshleyYakeley]

v1 should give a type error. a -> a is a positive type with rigid a, and cannot be inverted.

More specifically, given some positive type T, there is some set of positive types S that can be subsumed to T. The task is to find a negative type T' such that the set of positive types that unify with T' is the same as S. This is "type inversion with rigid type variables", and will fail for types with type variables.

But this must be accepted:

datatype R1 of
    MkR1 of
    f: a -> a;
    end;
end;

v5 = let x = fn a => a in
    MkR1 of f=x end;

Also this:

datatype R2 of
    MkR2 of
    f: Integer -> Text;
    end;
end;

v6 = fn x => MkR2 of f=x end;

[AshleyYakeley]

Done.