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

Julian Fondren jfondren at minimaltype.com
Sat Jul 20 10:02:34 AEST 2019


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.

I don't think this situation is that bad, though.

Compare Mercury's list.(++)

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

and the same function from Scala:

    def ++ [B >: A, That] (that: TraversableOnce[B])(implicit bf: 
CanBuildFrom[List[A], B, That]) : That

Scala's ++ is surely more flexible and perhaps the compiler can catch
some more classes of error with it, but, obviously there are also costs
that come with the benefits. I imagine chasing those benefits is like,
to sate your hunger, chasing a mouse through an entire supermarket.
You pass by a lot of really good food and then you die of the plague.

I just happened to read 
https://blog.joda.org/2011/11/scala-feels-like-ejb-2-and-other.html

Relatedly (to the supermarket analogy), how up to date are these pages?

https://mercurylang.org/development/developers/todo.html

https://mercurylang.org/development/developers/work_in_progress.html

And unrelatedly:

https://mercurylang.org/development/developers/release_checklist.html


More information about the users mailing list