[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