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

[Julien Fischer]

On Fri, 19 Jul 2019, Julian Fondren wrote:

> On 2019-07-19 02:28, Julien Fischer wrote:
>> 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.
>
> It's interesting that Mercury's libraries are not as clever as Mercury
> allows. I noticed that first with typeclasses, which are omnipresent in
> some other languages but which only even appear in nine of Mercury's
> library modules.

Something to bear in mind here is that much of Mercury's standard
library was written *before* type classes were added to the language.
(If we were starting the standard library again from scratch, we'd
probably make more use of them.)

The lack of various advanced mode system feature in the standard
library is down to a similar reason and also due to stability and
preformance concerns.

Julien.