fundeps help
Simon Peyton-Jones
simonpj at microsoft.com
Mon Dec 3 09:21:12 EST 2007
| Is it really a good idea to permit a type signature to include
| equality constraints among unifiable types? Does the above type
| signature mean something different from a ->a? Does the type signature:
| foo :: (a~Bar b) => a -> Bar b
| mean something different from:
| foo :: Bar b -> Bar b
| ? I know that System FC is designed to let us write stuff like:
| foo :: (Bar a ~ Baz b) => Bar a -> Baz b
| Which is of course what we need for relating type functions. But I'm
| wondering if there's a subtlety of using an equality constraint vs
| just substitution that I've missed
No, you didn't miss anything. I wouldn't expect anyone to write these types directly. But it can happen:
class C a b | a->b
instance C Int Bool
class D x where
op :: forall y. C x y => x -> y
instance D Int where
op = ...
In the (D Int) instance, what's the type of op? Well, it must be
op :: forall y. C Int y => Int -> y
And here we know that y=Bool; yet since we don't write the type sig directly we can't say it. So GHC's implementation of fundeps rejects this program; again it can't be translated into System F.
Simon
More information about the Glasgow-haskell-users
mailing list