[mercury-users] Existential types and list.map

[Mark Brown]

On 29-Jul-2005, Peter Hawkins <peter at hawkins.emu.id.au> wrote:
> Hi...
> 
> Why doesn't this work?
> 
> :- module test3.
> :- interface.
> :- import_module io.
> 
> :- pred main(io.state::di, io.state::uo) is det.
> 
> :- implementation.
> 
> :- import_module list.
> 
> :- some [T] func get_thing(int) = T.
> get_thing(X) = X.
> 
> main(!IO) :-
>    X = [1,2],
>    Y = map(get_thing, X),
>    io.print(Y, !IO),
>    io.nl(!IO),
>    true.

This is not type safe because there is nothing in the signature of get_thing
that guarantees that all of the elements in list Y have the same type.  To
build such a list you would need to have get_thing return a structure that
contains an existentially typed value.  For example, the signature for
get_thing could be:

	:- func get_thing(int) = univ.

Then Y would have type list(univ), which would be okay.

> I get the misleading error message:
> $ mmc --make test3
> Making Mercury/int3s/test3.int3
> Making Mercury/cs/test3.c
> test3.m:016: In clause for predicate `test3.main/2':
> test3.m:016:   in argument 1 of functor `map/2':
> test3.m:016:   error: undefined symbol `get_thing/0'.

Well, you should bear in mind that get_thing/0 and get_thing/1 are in fact
different names.  Mercury's type checker does allow this distinction to be
blurred to some extent by automatically considering names with equal or
greater arity than what literally appears in the program, whenever the
name matches that of a known predicate or function.  However, it then rules
out any cases which could not be type-correct, which in this case includes
get_thing/1.

Generally you can get better error messages if an explicit lambda expression
is used.  Unfortunately that doesn't work in this case, which really is a
(known) bug in the compiler that existentially typed lambda expressions are
not properly supported.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------