[mercury-users] Typeclass constraint on HO (function) discriminator

[Ralph Becket]

doug.auclair at logicaltypes.com, Wednesday, 19 April 2006:
> Dear all,
> 
> I'm running into type errors when I attempt to
> constrain a higher-order function discriminator
> of a type.  It may be due to an existential issue,
> (it complains that I need a function of arity X,
> but I am passing it a(n existentially quantified)
> function of arity X (with a typeclass constraint 
> on an argument), so I'm quite stuck, as my 
> attempts to create an existential function lead 
> to (many) more errors.  How do I get the 
> following program to compile and to run?
> 
> The refman shows straightforward examples of
> calling existential functions, but not HO ones.
> Must HO functions be universal?  If so, is there
> a workaround to impose a typeclass constraint on
> an argument in an HO function?
> 
> Thanks for your help!
> 
> Sincerely,
> Doug Auclair
> 
> ----- program -----
> 
> :- module proba.
> 
> :- interface.
> 
> :- import_module io.
> 
> :- pred main(io::di, io::uo) is det.
> 
> :- implementation.
> :- import_module int.
> 
> :- typeclass generator(X) where [
>       func generate(int, X) = int
> ].
> 
> :- type foo
>         ---> some [Gen]
>              { int, func(int, Gen) = int } => generator(Gen).

Using braces in discriminated unions is a Bad Idea.  See `type tricky'
in the "Discriminated unions" part of the Reference Manual.  Use a
different data constructor name, such as `foo', to avoid trouble.

> :- type bar ---> bar.
> 
> :- instance generator(bar) where [generate(Int, _) = Int + 3].
> 
> main -->
> 	print("Hello world!\n"),
> 	foo_me_baby({ 5,
> 	              (func(X, Gen) = Baz :- Baz = generate(X, Gen)) },
> 	            bar).

[After changing {} to foo()] you could have just written that as

main -->
	print("Hello world!\n"),
	foo_me_baby(foo(5, generate), bar).

[Please don't use DCGs for IO; use state variables instead.]

> :- pred foo_me_baby(foo::in, Gen::in, io::di, io::uo) is det.
> foo_me_baby({ X, Func }, Gen) -->
> 	print(Func(X, Gen)).

The problem here is that you're applying an polymorphic, unconstrained,
value Gen to Func which is expecting *some particular, unknown* type
that is an instance of generator.  Even adding the constraint
`<= generator(Gen)' to the pred declaration won't work because the
compiler still can't show that whatever particular Gen is passed on a
given call is the actual type expected by Func.

The thing is that it's only meaningful to existentially quantify output
arguments, not input arguments.

What I think you're trying to do is require that the second argument of
any function in a foo value be an instance of generator.  Unfortunately
that leads to a bunch of problems, so we don't support it (I can't
recall the reasons off the top of my head, but you can search the list
archives if you're interested).

The current solution would be to have an auxiliary mk_foo function which
does have the right constraints on its signature:

:- type foo(T) ---> foo(int, func(int, T) = int).

:- func mk_foo(int, func(int, T) = int) = foo(T) <= generator(T).

mk_foo(N, F) = foo(N, F).

Then you can write

main(!IO) :-
	print("Hello, World!\n", !IO),
	foo_me_baby(mk_foo(5, generate), bar).

:- pred foo_me_baby(foo::in, T::in, io::di, io::uo) is det <= generator(T).

foo_me_baby(foo(X, Func), Gen, !IO) :-
	print(Func(X, Gen), !IO).

This works fine for me!

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