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

[Julian Fondren]

Hello,

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
the language enforces that you only pass lists into this code that
your code has definitely checked does abide by this requirement.

The closest I've gotten to that in Mercury is this code:

   :- module nonempty.
   :- interface.
   :- import_module io.
   :- pred main(io::di, io::uo) is det.
   :- implementation.
   :- import_module list.

   :- pred check(list(T), list(T)).
   :- mode check(in, out(non_empty_list)) is semidet.
   :- pragma promise_pure(check/2).
   check(L0 @ [_|_], L) :-
       impure magic(L0, L).

   :- impure pred magic(list(T), list(T)).
   :- mode magic(in, out(non_empty_list)) is det.
   :- pragma foreign_proc("C",
       magic(List0::in, List::out(non_empty_list)),
       [will_not_call_mercury],
   "
       List = List0;
   ").

   :- pred print_nonempty(list(T)::in(non_empty_list), io::di, io::uo) is 
det.
   print_nonempty(L, !IO) :-
       foldl((pred(X::in, !.IO::di, !:IO::uo) is det :-
           io.print(X, !IO),
           io.nl(!IO)), L, !IO).

   main(!IO) :-
       io.command_line_arguments(Args0, !IO),
       (
           check(Args0, Args)
       ->
           print_nonempty(Args, !IO)
       ;
           true
       ).

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", 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?

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.

Thanks,