[Haskell-cafe] Strange type error with associated type synonyms
ryani.spam at gmail.com
Mon Apr 6 20:07:04 EDT 2009
On Mon, Apr 6, 2009 at 2:36 PM, Peter Berry <pwberry at gmail.com> wrote:
> As I understand it, the type checker's thought process should be along
> these lines:
> 1) the type signature dictates that x has type Memo d a.
> 2) appl has type Memo d1 a -> d1 -> a for some d1.
> 3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1
This isn't true, though, and for similar reasons why you can't declare
a generic "instance Fun d => Functor (Memo d)". Type synonyms are not
injective; you can have two instances that point at the same type:
data Unit1 = Unit1
data Unit2 = Unit2
newtype Identity x = Id x
unit_abst x f = Id (f x)
unit_appl (Id v) _ = v
instance Fun Unit1 where
type Memo Unit1 = Identity
abst = unit_abst Unit1
appl = unit_appl
instance Fun Unit2 where
type Memo Unit2 = Identity
abst = unit_abst Unit2
appl = unit_appl
Now, Memo Unit1 a = Identity a = Memo Unit2 a, but that does not give
us that Unit1 = Unit2.
In fact, memo_fmap' is ambiguous; what should this application do?
memo_fmap' id (Id ())
Should it look at the instance for Unit1, or Unit2, or some other
instance we haven't given yet?
You can use a data family instead, and then you get the property you
want; if you make Memo a data family, then Memo d1 = Memo d2 does
indeed give you d1 = d2.
You can still use other types in your instances, just use "newtype
instance Memo Unit1 a = MemoUnit1 (Identity a)" and add the
appropriate newtype wrappers and unwrappers.
> But for some reason, step 3 fails. If we annotate appl with the
> correct type (using scoped type variables), it type checks:
>> -- thanks to mmorrow on #haskell for this
>> memo_fmap'' :: forall a b d. Fun d => (a -> b) -> Memo d a -> Memo d b
>> memo_fmap'' f x = abst (f . (appl :: Memo d a -> d -> a) x)
Right, because now you have constrained appl ahead of time, passing in
the correct type, instead of hoping the compiler can guess how you
meant to use "appl".
I don't know if this function is callable, though; at the very least
you need to annotate its call site to get the proper instance passed
This is somewhat solvable with a proxy element to fix the instance of Fun:
data Proxy d = Proxy
memo_fmap_nonamb :: Fun d => Proxy d -> (a -> b) -> Memo d a -> Memo d b
memo_fmap_nonamb _ f x = abst (f . appl x)
I don't know if this version compiles without the type annotation; my
guess is that it might! But even if it doesn't, once you add the
proper annotation it is at least callable:
test = memo_fmap_nonamb (Proxy :: Proxy Unit1) id (Id ())
I think, for this problem, data families are a better solution. They
also let you write the generic Functor instance.
More information about the Haskell-Cafe