[m-dev.] subtypes proposal

[Peter Wang]

Hi,

In this proposal, subtypes are distinct d.u. types that share a data
representation with a base type, which is a normal d.u. type.
Subtypes of subtypes are allowed.
Every term of a given subtype must also be valid term in the supertype
(recursively, up to the base type), with the same data representation.

A subtype can be introduced like this:

    :- type SUBTYPE =< SUPERTYPE
        --->    BODY.

The constructor definitions in BODY must be a (non-strict) subset of the
constructors of the supertype. If the supertype t has constructor
f(T1, ..., Tn) then a subtype s =< t may have a constructor
f(S1, ..., Sn) such that Si =< Ti.

TODO: requires further thought

  - higher order types can have inst constraints now
  - existential class constraints must match exactly?

Any type variable that occurs in SUBTYPE must also occur in SUPERTYPE.
Any universally quantified type variable that occurs in BODY
must also occur in SUBTYPE.

Examples:

    :- type empty_list =< list(T)
        --->    [].

    :- type non_empty_list(T) =< list(T)
        --->    [T | list(T)].

    :- type non_empty_list_of_foo =< list(foo)
        --->    [foo | list(foo)].

    :- type maybe_univ
        --->    none
        ;       some [T] univ(T).

    :- type yes_univ =< maybe_univ
        --->    some [T] univ(T).


Type conversions
----------------

I propose to not introduce any implicit conversion between subtypes and
supertypes, for a few reasons:

  - there are no implicit type conversions anywhere else in the language
  - explicit conversions may be easier to understand
  - I do not want to set myself up to potentially rewrite the type
    checker ;)

Rather, terms can be coerced between subtype and supertype with an
explicit operation, say, written like a function call:

    Y = coerce(X)

A coercion from FromType to ToType is type correct if FromType and ToType
are equivalent after replacing any subtypes with their base types.

For example, if s =< t and non_empty_list(T) =< list(T) then coercions
between these pairs of types should be accepted by the type checker:

    s <-> t
    list(s) <-> list(t)
    non_empty_list(s) <-> non_empty_list(t)
    list(s) <-> non_empty_list(s)
    list(s) <-> non_empty_list(t)

Coercions must be mode correct.
Assume we have a coercion of X:s to Y:t.
If Xi, Xf, Yi, Yf are the initial and final insts of X and Y
then the coercion is mode correct iff:

  - Xi is a ground inst (no partial instantiation, no uniqueness)

  - Xf = Xi

  - Yi is free

  - Yf is the glb of Xi and the instantiatedness tree derived from t
    where all nodes are bound.
    The glb must exist,
    Yf must be be ground,
    and Yf must be a valid inst of t.

Coercing a ground term from subtype to supertype is always allowed.
We use the mode system to ensure that a coercion from supertype to
subtype is safe at compile time.

It would probably be useful to also provide a semidet coercion operation
that can fail at runtime if the term is not valid for the result type.


Interaction with modules
------------------------

The compiler needs to know the definition of the base type in order to
construct, deconstruct and coerce terms of a subtype.

If a subtype is defined in the interface section of a module M
then its supertype must either

 - be defined in the interface section of M, or
 - be defined in a module imported in the interface section of M.

If a subtype is defined in the implementation section of a module M,
then its supertype must either

  - be defined in M, or
  - be defined in the interface section of a module imported by M.

A subtype may be abstractly exported, like other d.u. types.
Coercions to/from the subtype cannot be checked in modules without
visibility of the subtype definition (and its supertype),
and will be rejected at compile time.


Comparison to previous proposal
-------------------------------

Compared to Fergus's 1998 proposal
(http://lists.mercurylang.org/pipermail/developers/1998-February/002274.html)
the "subtypes" in this proposal works with polymorphically typed
(but non polymorphically moded) predicates and containers in a
straightforward way, without constrained polymorphic modes.

I think the declarations of the form

    :- subtype SubType < Type :: Inst.

would have been most useful to provide an inst for a higher order Type,
but we have a different feature to handle that now.


I have attached a copy of a module that demonstrates what code using the
proposed feature might look like. (Not suggesting that it would be
better than the cord representation used in the standard library.)

Peter
-------------- next part --------------
:- module cord_subtypes.
:- interface.

:- import_module list.

:- type cord(T).

:- func init = cord(T).

:- pred is_empty(cord(T)::in) is semidet.

:- func singleton(T) = cord(T).

:- func from_list(list(T)) = cord(T).

:- func to_list(cord(T)) = list(T).

:- func cons(T, cord(T)) = cord(T).

:- func cord(T) ++ cord(T) = cord(T).

:- pred head_tail(cord(T)::in, T::out, cord(T)::out) is semidet.

:- pred member(T::out, cord(T)::in) is nondet.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- implementation.

:- type cord(T)
    --->    empty_cord
    ;       unit_node(T)
    ;       list_node(nonempty_list(T))
    ;       branch_node(nonempty_cord(T), nonempty_cord(T)).

:- type nonempty_list(T) % =< list(T)
    --->    [T | list(T)].

:- type nonempty_cord(T) % =< cord(T)
    --->    unit_node(T)
    ;       list_node(nonempty_list(T))
    ;       branch_node(nonempty_cord(T), nonempty_cord(T)).

init = empty_cord.

is_empty(empty_cord).

singleton(X) = unit_node(X).

from_list(Xs) = C :-
    (
        Xs = [],
        C = empty_cord
    ;
        Xs = [_ | _],
        C = list_node(coerce_to_nonempty_list(Xs))
    ).

to_list(C) = Xs :-
    (
        C = empty_cord,
        Xs = []
    ;
        C = unit_node(X),
        Xs = [X]
    ;
        C = list_node(Xs0),
        Xs = coerce_to_list(Xs0)
    ;
        C = branch_node(A, B),
        Xs = to_list(coerce_to_cord(A)) ++ to_list(coerce_to_cord(B))
    ).

cons(X, C0) = C :-
    (
        C0 = empty_cord,
        C = unit_node(X)
    ;
        ( C0 = unit_node(_)
        ; C0 = list_node(_)
        ; C0 = branch_node(_, _)
        ),
        C = coerce_to_cord(cons_ne(X, coerce_to_nonempty_cord(C0)))
    ).

:- func cons_ne(T, nonempty_cord(T)) = nonempty_cord(T).

cons_ne(X, unit_node(Y)) = list_node([X, Y]).
cons_ne(X, list_node(Xs)) = list_node([X | coerce_to_list(Xs)]).
cons_ne(X, branch_node(A, B)) = branch_node(cons_ne(X, A), B).

A ++ B = C :-
    (
        A = empty_cord,
        C = B
    ;
        ( A = unit_node(_)
        ; A = list_node(_)
        ; A = branch_node(_, _)
        ),
        (
            B = empty_cord,
            C = A
        ;
            ( B = unit_node(_)
            ; B = list_node(_)
            ; B = branch_node(_, _)
            ),
            C = branch_node(
                    coerce_to_nonempty_cord(A),
                    coerce_to_nonempty_cord(B))
        )
    ).

head_tail(C, Head, Tail) :-
    ( C = unit_node(_)
    ; C = list_node(_)
    ; C = branch_node(_, _)
    ),
    head_tail_ne(coerce_to_nonempty_cord(C), Head, Tail).

:- pred head_tail_ne(nonempty_cord(T)::in, T::out, cord(T)::out) is det.

head_tail_ne(Node, Head, Tail) :-
    (
        Node = unit_node(Head),
        Tail = empty_cord
    ;
        Node = list_node([Head | T]),
        (
            T = [],
            Tail = empty_cord
        ;
            T = [_ | _],
            Tail = list_node(coerce_to_nonempty_list(T))
        )
    ;
        Node = branch_node(A0, B),
        head_tail_ne(A0, Head, A),
        (
            A = empty_cord,
            Tail = coerce_to_cord(B)
        ;
            ( A = unit_node(_)
            ; A = list_node(_)
            ; A = branch_node(_, _)
            ),
            Tail = branch_node(coerce_to_nonempty_cord(A), B)
        )
    ).

member(X, Node) :-
    (
        Node = unit_node(X)
    ;
        Node = list_node(Xs),
        member(X, coerce_to_list(Xs))
    ;
        Node = branch_node(A, B),
        (
            member(X, coerce_to_cord(A))
        ;
            member(X, coerce_to_cord(B))
        )
    ).

%---------------------------------------------------------------------------%

% Emulate coerce

:- inst nonempty_cord for cord/1
    --->    unit_node(ground)
    ;       list_node(ground)
    ;       branch_node(ground, ground).

:- func coerce_to_cord(nonempty_cord(T)) = cord(T).
:- mode coerce_to_cord(in) = out(nonempty_cord) is det.

coerce_to_cord(unit_node(X)) = unit_node(X).
coerce_to_cord(list_node(Xs)) = list_node(Xs).
coerce_to_cord(branch_node(A, B)) = branch_node(A, B).

:- func coerce_to_nonempty_cord(cord(T)) = nonempty_cord(T).
:- mode coerce_to_nonempty_cord(in(nonempty_cord)) = out is det.

coerce_to_nonempty_cord(unit_node(X)) = unit_node(X).
coerce_to_nonempty_cord(list_node(Xs)) = list_node(Xs).
coerce_to_nonempty_cord(branch_node(A, B)) = branch_node(A, B).

:- func coerce_to_nonempty_list(list(T)) = nonempty_list(T).
:- mode coerce_to_nonempty_list(in(non_empty_list)) = out is det.

coerce_to_nonempty_list([H | T]) = [H | T].

:- func coerce_to_list(nonempty_list(T)) = list(T).

coerce_to_list([H | T]) = [H | T].

:- pred semidet_coerce_to_nonempty_cord(cord(T), nonempty_cord(T)).
:- mode semidet_coerce_to_nonempty_cord(ground >> nonempty_cord, out)
    is semidet.

semidet_coerce_to_nonempty_cord(C0, C) :-
    is_nonempty_cord(C0),
    C = coerce_to_nonempty_cord(C0).

:- pred is_nonempty_cord(cord(T)).
:- mode is_nonempty_cord(ground >> nonempty_cord) is semidet.

is_nonempty_cord(unit_node(_)).
is_nonempty_cord(list_node([_ | _])).
is_nonempty_cord(branch_node(_, _)).