[m-dev.] subtypes proposal

[Julien Fischer]

On Wed, 20 Jan 2021, Peter Wang wrote:

> On Tue, 19 Jan 2021 17:24:22 +1100 Julien Fischer <jfischer at opturion.com> wrote:
>>
>> What's the motivation for bringing this up again?
>>
>
> I've wanted some sort of subtyping feature before, this idea seems
> relatively easy to implement, and I probably have time to implement it.

Just curious; I was wondering whether yeslogic or yourself had
encountered a definite need for them.  (If you are going to proceed, I
suggest you begin by drafting a change to the reference manaual.)

>> On Thu, 14 Jan 2021, Peter Wang wrote:
>>
>>> 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.
>>
>> I would be inclined to retain the ':- subtype' declaration of
>> the original subtypes proposal.
>>
>
> ':- subtype' in the original proposal makes sense as it introduces a
> sort of type synonym, and the body of the declaration was an inst,
> not constructors.
>
> I preferred ':- type' in this proposal as it really does introduce a new
> d.u. type. The only difference from the programmer's point of view is
> that it enables coercions between types that share a base type.
>
> If an type is abstractly exported, the fact that it is a subtype of some
> other type should not be visible to the user. The user of a module
> should see
>
>    :- type foo.
>
> instead of
>
>    :- subtype foo.
>
> in the module interface.
> (Assuming we won't mix ':- type' and ':- subtype'.)

I wouldn't mix them.  I'm happy enough with just ':- type'.

...

>>> 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).
>>
>> Do any existential class constraints have to be repeated in the subtype
>> declaration?
>>
>
> Yes. I don't see why we should allow them to be omitted.

One reason would be: they are known from the supertype and having to
replicate them is a possible source of errors.

Julien.