fundeps for extended Monad definition

[oleg@pobox.com]

Ashley Yakeley wrote:

> If this were allowed, it would effectively allow type-lambda
> class C a b | a -> b
> instance C Int Bool
> instance C Bool Char

> newtype T a = MkT (forall b.(C a b) => b)
> helperIn :: (forall b.(C a b) => b) -> T a
> helperIn b = MkT b; -- currently won't work
> helperOut :: T a -> (forall b.(C a b) => b)
> helperOut (MkT b) = b

And it does work (based on the code shown here previously):

> class C a b | a -> b
> instance C Int Bool
> instance C Bool Char
> instance C Char Float
> instance C Float (Int->())
> instance (C a b) => C (a->()) (b->())



> newtype T a = T (forall b.(C a b) => b)
> data T1 a = T1 a (T a) 
> xx b = case (T1 b (T undefined)) of T1 _ (T x) -> x


Ok, modules loaded: Main.
*Main> :type xx$(1::Int)
Bool
*Main> :type xx$ xx$ (1::Int)
Char
*Main> :type xx$ xx$ xx$ (1::Int)
Float
*Main> :type xx$ xx$ xx$ xx$ (1::Int)
Int -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ (1::Int)
Bool -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
Char -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
Float -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Int -> ()) -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Bool -> ()) -> ()
*Main> :type xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ xx$ (1::Int)
(Char -> ()) -> ()

It seems it does compute....

The principle was to use constraints to force the "evaluation" of the
type "lambda". Obtaining the type "lambda" was the thrust behind the
exercise with existential and useless types. Perhaps I neglected to
mention that point.

We can use the Coerce type function (aka class) mentioned in the
thread on first-class types to convert from the types computed by 'xx'
to values. Incidentally, the class D was already a type function: the
function 'meet'.