Contexts in Existential Types

[Fergus Henderson]

On 13-Mar-2001, Ashley Yakeley <ashley@semantic.org> wrote:
> Would it be appropriate for Haskell to be able to remember contexts in 
> existential types?

I'm not sure exactly what you mean by that.
But your example requires existentially typed functions.
It would certainly be appropriate for Haskell to support
existentially typed functions.

> For instance, currently this does not work in Hugs:
> 
> --
> class Charable a where
> 	obtainChar :: a -> Char
> 
> instance Charable Char where
> 	obtainChar c = c
> 
> data AnyCharable = forall c. (Charable c) => MkAnyCharable c
> 
> anyA = MkAnyCharable 'a'
> recoverA = obtainChar ((\(MkAnyCharable c) -> c) anyA)
> --

You can write that kind of thing in Mercury.  However, you need to use
a separate function rather than a lambda expression, since for this
to work the lambda expression has to have an existentially quantified
polymorphic type, and in Mercury (as in Haskell 98), lambda expressions
are always monomorphic.

fjh$ cat test.m
	:- import_module char.
	:- typeclass charable(A) where [
		func obtainChar(A) = char
	].
	:- instance charable(char) where [
		obtainChar(C) = C
	].
	% Note for Haskell readers:
	% in Mercury the constructor name goes on the left of the `=>'
	% and the type class constraints go on the right of it
	:- type anyCharable ---> some [C] mkAnyCharable(C) => charable(C).

	anyA = 'new mkAnyCharable'('a').
	recoverA = obtainChar(x(anyA)).
	x(mkAnyCharable(C)) = C.

fjh$ mmc -C --infer-all test.m
test.m:001: Warning: module should start with a `:- module' declaration.
test.m:  1: Warning: interface for module `test' does not export anything.
test.m:012: Inferred :- func anyA = (test:anyCharable).
test.m:013: Inferred :- func recoverA = character.
test.m:014: Inferred :- some [C] (func x((test:anyCharable)) = C => (test:charab
le(C))).

Note that the type inferred for `x' is an existentially quantified function
type.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.