[mercury-users] Scott Types in Mercury

[Jonathan Morgan]

On Fri, Apr 25, 2008 at 6:59 PM, Julien Fischer
<juliensf at csse.unimelb.edu.au> wrote:
>  On Fri, 25 Apr 2008, Jonathan Morgan wrote:
> > 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?
> >
>
>  For the problem with the type_infos see section 11.3 of the
>  reference manual,  When "construct(ing) a value using an existentially
>  quantified functor, you must prepend `new ' onto the functor name".
>
>  So, in the above:
>
>         nil = 'new list'((func(Nil, _Cons) = Nil)).
>
>  Likewise, for cons/2. (Of course, you'll still get warnings about
> unresolved polymorphism
>  in the above code.)

I'd forgotten about that (I haven't used Mercury seriously for a while).

That makes nil and cons work, but it still won't make length work,
because it ends up having to unify some[B] with int, which it can't do
because the callee should determine the type.  I can see why this
doesn't work with existential types, but is there any better way to
represent something like this? (where we want the output of the ADT
functions to be of any arbitrary type, but determined by the caller,
not the callee).  You could make it work with univ or something
similar, but that wouldn't really be very useful to do.  It seems
sensible, but I'm not sure that it's easily typeable

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