[mercury-users] Scott Types in Mercury

[Jonathan Morgan]

In Functional Programming we were looking at Scott types, and Bernie
mentioned that they were not typable in Haskell (Scott types are
largely trying to represent ADTs as functions).

I tried to type this in Mercury using existential typing, so that the
type of the output was completely separate from the type of the list
(since we want to be able to write functions that take a list and
return any arbitrary type).  You would like to be able to write
functions like length below, which allow you to act on the list.

:- type list(A) --->
	some[B]
	list(
		func(B, func(A, list(A)) = B) = B
	).

:- func nil = list(A).
nil = list((func(Nil, _Cons) = Nil)).

:- func cons(A, list(A)) = list(A).
cons(X, Xs) = list(L) :-
	L = (func(_Nil, Cons) = Cons(X, Xs)).

:- func length(list(A)) = int.
length(list(L)) = L(0, func(_, Rest) = 1 + length(Rest)).

When I try doing this, I get the following errors, referring to the
typeinfos being free in nil and cons (presumably because I haven't
given any context from which the type of B can be decided).  Is it
possible to type these types in Mercury?  If so, what am I doing
wrong?

scott.m:023: In clause for `nil = out':
scott.m:023:   mode error in conjunction. The next 2 error messages indicate
scott.m:023:   possible causes of this error.
scott.m:023:   In clause for `nil = out':
scott.m:023:   in function result term of clause head:
scott.m:023:   in argument 1 of functor `list/1':
scott.m:023:   mode error: variable `TypeInfo_12' has instantiatedness `free',
scott.m:023:   expected instantiatedness for non-local variables of lambda
scott.m:023:   goals is `ground'.
scott.m:023:   In clause for `nil = out':
scott.m:023:   in function result term of clause head:
scott.m:023:   mode error in unification of `HeadVar__1' and
scott.m:023:   `scott.list(TypeInfo_12, V_4)'.
scott.m:023:   Variable `HeadVar__1' has instantiatedness `free',
scott.m:023:   term `scott.list(TypeInfo_12, V_4)' has instantiatedness
scott.m:023:   `scott.list(
scott.m:023:     free,
scott.m:023:     free
scott.m:023:   )'.
scott.m:027: In clause for `cons(in, in) = out':
scott.m:027:   mode error in conjunction. The next 2 error messages indicate
scott.m:027:   possible causes of this error.
scott.m:027:   In clause for `cons(in, in) = out':
scott.m:027:   mode error: variable `TypeInfo_16' has instantiatedness `free',
scott.m:027:   expected instantiatedness for non-local variables of lambda
scott.m:027:   goals is `ground'.
scott.m:026:   In clause for `cons(in, in) = out':
scott.m:026:   in function result term of clause head:
scott.m:026:   mode error in unification of `HeadVar__3' and
scott.m:026:   `scott.list(TypeInfo_16, L)'.
scott.m:026:   Variable `HeadVar__3' has instantiatedness `free',
scott.m:026:   term `scott.list(TypeInfo_16, L)' has instantiatedness
scott.m:026:   `scott.list(
scott.m:026:     free,
scott.m:026:     free
scott.m:026:   )'.

Jon
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------