fundeps for extended Monad definition

Hal Daume III hdaume@ISI.EDU
Mon, 3 Mar 2003 10:38:24 -0800 (PST)


> | entirely so, since the result of it is not of type 'forall b. b', but
> | rather of 'forall b. C Int b => b'.  Thus, if the C class has a
> function
> | which takes a 'b' as an argument, then this value does have use.
> 
> I disagree.   Can you give an example of its use?   

I believe something along the lines of the following would work:

> class C a b | a -> b where { foo :: b -> String }
> instance C Int Int   where { foo x = show (x+1) }
> x :: forall b. C Int b => b
> x = 5

(Supposing that the above definition were valid; i.e., we didn't get the
type signature error, this reads that x has type "b" for all types
"b" such that C Int b -- the fact that there is only one such type (due to
the fun dep) is for us to know.)

Then, we should be able to say:

> foo x

and get "6".

>From a "translation to untyped core" perpective (*grin*), we essentially
replace class constraints with dictionaries.  The definition of C
introduces a dictionary like the following (I'm not 100% familiar with
MPTC dictionaries, but I assume they're just like normal dictionaries):

> data CDict a b = CDict (b -> String)

Then the instance will give us:

> cIntIntDict :: CDict Int Int
> cIntIntDict = CDict (\x -> show (x+1))

foo will become:

> foo (CDict foo_f) x = foo_f x

and if we apply this properly, we get:

|      foo cIntIntDict x
| ==>  (\ (CDict foo_f) x -> foo_f x) cIntIntDict x
| ==>  (\ (CDict foo_f) -> foo_f x) cIntIntDict
| ==>  (\x -> show (x+1)) x
| ==>  show (5+1)
| ==>  "6"

or something like that?

In fact, except for the type definition on x, this is actually a valid
translation into typed core, I believe.  The weird type on x is the only
stumbling block, afaics.

...it is well known that I could be wrong though...

 - Hal