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