[mercury-users] dependent types with mercury

[Vladimir Gubarkov]

Hi,

I've read this blogpost

http://adventuresinmercury.blogspot.com/2011/04/dependent-typing-reversing-non-empty.html

And thought, I could try to implement smth like even- (odd-) sized list
using appropriate modes.
I tried next:

:- module lists1.

:- interface.

:- import_module io.

:- pred main(io::di, io::uo) is det.

:- implementation.

:- import_module list.

%:- inst even_list ---> [] ; [ground|even_list]. % XXX
:- inst even_list ---> [] ; [ground,ground|even_list]. % YYY

%:- type even_list(T) ---> []; [T,T|even_list(T)].

%:- pred t(even_list(int)).
:- pred t(list(int)).
:- mode t(in(even_list)) is semidet.
t([1,2,3,4]).

main(!IO) :-
L=[1,2,3,4,5,6],
%L=[1,2,3,4,5,6,7],
( t(L) ->
print("1",!IO)
;
print("2",!IO)
).

But this resulted in

D:\stuff\test\mercury\deptypes>mmc.bat --make lists1
Making Mercury\int3s\lists1.int3
Making Mercury\ints\lists1.int
Making Mercury\cs\lists1.c
lists1.m:014: In definition of inst `lists1.even_list'/0:
lists1.m:014:   error: undefined inst `[|]'/2.
Error: system command received signal 1.
** Error making `Mercury\cs\lists1.c'.

Note, that if I comment YYY line and uncomment XXX - code compiles well.
My will is that I could compile code with L=[1,2,3,4,5,6] (even sized list)
but not with L=[1,2,3,4,5,6,7] (odd).

Is this possible with mercury?

Sincerely yours,
Vladimir.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20110407/2cbc1901/attachment.html>