[m-users.] Using insts to simulate dependent-type features.

[Julien Fischer]

Hi Mark,

On Fri, 19 Jul 2019, Mark Brown wrote:

> On Thu, Jul 18, 2019 at 8:01 PM Julien Fischer <jfischer at opturion.com> wrote:
>> The major issue with using insts like the above is that the standard
>> library doesn't use polymorphic modes (for the most part), so the
>> subtype information tends to get lost quite easily.
>
> There's that, and also that it doesn't tend to provide specific modes
> that constrain the subtype. For example, list.append could have these
> additional modes:
>
> :- mode append(in(non_empty_list), in, out(non_empty_list)) is det.
> :- mode append(in, in(non_empty_list), out(non_empty_list)) is det.
>
> Similarly for list.reverse, list.reverse_prepend, list.map*, etc.
> Also, some existing modes could be tightened, such as the (in, in,
> out) mode of list.insert.

You'd probably want to combine the two things, e.g. define

     :- inst non_empty_list(I) for list/1
         --->    [I | list(I)].

    :- mode append(in(non_empty_list(I)), in, out(non_empty_list(I))) is det.

Julien.