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

[Julian Fondren]

On 2019-07-18 05:01, Julien Fischer wrote:
> 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.)

Non-zero length, then. I'm used to Positive (1..) as a subtype of
Natural (0..).

>> 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.

Ah, I see. Thanks for your reply.