[m-dev.] subtypes proposal

[Peter Wang]

On Tue, 19 Jan 2021 23:39:55 +1100 Mark Brown <mark at mercurylang.org> wrote:
> >
> > 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.
> 
> That proposal allowed you to say, for example, that reversing a
> non-empty list results in a non-empty list whereas reversing a list
> just gives you a list, without just writing two separate reverse
> functions. Any chance of allowing something like that?

For that example, you could share a helper predicate in one of two ways:

1. the helper predicate is defined on the supertype, so you need to
convert terms of the subtype to the supertype, then back again.
You'd need to declare an inst corresponding to the subtype.
For larger pieces of code, it may be hard to avoid losing the inst
information (which is partly what subtypes are supposed to help with, hmm).

2. the helper predicate is defined on the subtype, so you need to
convert from the supertype to the subtype to call the helper predicate,
then convert back again.

I imagine (2) would usually be the way to go. To help with (1) perhaps
we could have a briefer way to declare a ground inst that corresponds to
a subtype, or even have it declared automatically by the subtype
declaration, assuming it's useful enough.

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

:- type list(T)
    --->    []
    ;       [T | list(T)].

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

:- inst nonempty_list for list/1
    --->    [ground | ground].

:- pred reverse(list(T), list(T)).
:- mode reverse(in, out) is det.

:- pred reverse_ne(nonempty_list(T), nonempty_list(T)).
:- mode reverse_ne(in, out) is det.

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

:- implementation.

reverse(L, R) :-
    reverse_prepend(L, [], R).

reverse_ne(L0, R) :-
    L = coerce_to_list(L0),
    reverse_prepend(L, [], R0),
    R = coerce_to_ne(R0).

:- pred reverse_prepend(list(T), list(T), list(T)).
:- mode reverse_prepend(in(nonempty_list), in, out(nonempty_list)) is det.
:- mode reverse_prepend(in, in(nonempty_list), out(nonempty_list)) is det.
:- mode reverse_prepend(in, in, out) is det.

reverse_prepend([], R, R).
reverse_prepend([H | T], R0, R) :-
    reverse_prepend(T, [H | R0], R).

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

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

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

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

coerce_to_ne([H | T]) = [H | T].
-------------- next part --------------
:- module reverse2.
:- interface.

:- type list(T)
    --->    []
    ;       [T | list(T)].

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

:- pred reverse(list(T), list(T)).
:- mode reverse(in, out) is det.

:- pred reverse_ne(nonempty_list(T), nonempty_list(T)).
:- mode reverse_ne(in, out) is det.

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

:- implementation.

reverse(L0, R) :-
    (
        L0 = [],
        R = []
    ;
        L0 = [_ | _],
        L1 = coerce_to_ne(L0),
        reverse_ne(L1, R1),
        R = coerce_to_list(R1)
    ).

reverse_ne([H | T], R) :-
    reverse_prepend(T, [H], R).

:- pred reverse_prepend(list(T), nonempty_list(T), nonempty_list(T)).
:- mode reverse_prepend(in, in, out) is det.

reverse_prepend([], R, R).
reverse_prepend([H | T], R0, R) :-
    R1 = [H | coerce_to_list(R0)],
    reverse_prepend(T, R1, R).

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

:- inst nonempty_list for list/1
    --->    [ground | ground].

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

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

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

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