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

[Julien Fischer]

Hi,

On Thu, 18 Jul 2019, Julian Fondren wrote:

> In dependent-typed languages (the only one I'm really familiar with is
> ATS, but I believe Idris is fairly well known), you can associate some
> compile-time values with statically known variables, checked by a
> constraint solver, so that you can f.e. write a bunch of code that
> operates on lists that must be of even and positive length, and then

Here's an inst definition for even length lists:

     :- inst even_list ---> [] ; [ground | odd_list].
     :- inst odd_list ---> [ground | even_list].

(I have no idea what a list of non-positive length would be.)

> the language enforces that you only pass lists into this code that
> your code has definitely checked does abide by this requirement.

In general, you're not going to get as far with insts as you can
in a dependently-typed language.

...

> It seems to me that this is also about the limits of what can be done.
> If I go further with an arbitrary requirement like "the list must have
> exactly 13 members",

You can build up insts describing lists with exactly N members, although
it's a bit cumbersome.

    :- inst exactly0 ---> [];
    :- inst exactly1 ---> [ground | exactly0].
    :- inst exactly2 ---> [ground | exactly1].
    :- inst exactly3 ---> [ground | exactly2].

etc etc.

> then I'd have to do something more like OOP with
> getter/setters that check some property, and the code could easily
> fail to check that requirement.
>
> Do I have that right? How advanced can you get with insts?

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.

> Maybe related question: is there any example code that puts this
> example from the manual to use?
>
>   :- type operation
>        --->   lookup(key, data)
>        ;      set(key, data).
>   :- inst request
>       --->    lookup(ground, free)
>       ;       set(ground, ground).
>   :- mode create_request == free >> request.
>   :- mode satisfy_request == request >> ground.

No, as is noted a couple of paragraphs above that example, support
for partial instantiation in the current mode checker is quite limited.

Julien.