[Haskell-cafe] Type families vs. functional dependencies -- how to express something

[Dan Weston]

 > Unifying those two types by hand, I get:
 >
 >     P (A t -> B a)
 > ~>  P (B a)

Maybe the problem is that type families (and associated types, their 
class cousins) are not injective: P x ~ P y does not imply that x ~ y. 
Maybe you need a data type (with appropriate wrapping and unwrapping) to 
ensure injectivity. Cf:

http://www.haskell.org/haskellwiki/GHC/Type_families#Injectivity.2C_type_inference.2C_and_ambiguity
http://www.mail-archive.com/haskell-cafe@haskell.org/msg63359.html

Dan

Tomáš Janoušek wrote:
> Hello all,
> 
> for the past few hours I've been struggling to express a certain idea using
> type families and I really can't get it to typecheck. It all works fine using
> functional dependencies, but it could be more readable with TFs. From those
> papers about TFs I got this feeling that they should be as expressive as FDs,
> and we should use them (some people even occasionally mentioning that FDs may
> be deprecated in favor of them). Can someone help me make the following work,
> please?
> 
> The working code with functional dependencies:
> 
>> {-# LANGUAGE FlexibleInstances #-}
>> {-# LANGUAGE MultiParamTypeClasses #-}
>> {-# LANGUAGE FunctionalDependencies #-}
>> {-# LANGUAGE TypeFamilies #-}
>> {-# LANGUAGE UndecidableInstances #-}
>> {-# LANGUAGE ScopedTypeVariables #-}
>>
>> __ = undefined
>>
>> data HNil = HNil
>> data HCons a b = HCons a b
>>
>> data A a = A a
>> data B a = B a
>>
>> class X a l p | a -> l p where
>>     ll :: a -> l
>>     pp :: a -> p
>>
>> instance X (B l) HNil (B l) where
>>     ll _ = HNil
>>     pp p = p
>>
>> instance (X x l p) => X (A t -> x) (HCons t l) p where
>>     ll _ = HCons __ (ll (__ :: x))
>>     pp p = pp (p (A (__ :: t)))
>>
>> -- (inferred)
>> -- testX :: (X a l (B l)) => a -> B l
>> testX x = pp x `asTypeOf` B (ll x)
> 
> The motivation here is that A a represents a variable of type a, B b
> represents a computation with state b, and functions of type A a -> B b
> represent a computations with state b that use the first parameter as an
> accessor for a variable (or, more precisely, state component) of type a. Now,
> I want testX to take such function (with n parameters) and provide it with
> those accessors, fixing the type b to contain components of the corresponding
> accessors only.
> (The example uses dummy types and undefineds for simplicity.)
> 
> This pretty much works:
> 
> testX (B __)                       :: B HNil
> testX (\(A _) -> B __)             :: B (HCons t HNil)
> testX (\(A True) -> B __)          :: B (HCons Bool HNil)
> testX (\(A _) (A _) -> B __)       :: B (HCons t (HCons t1 HNil))
> testX (\(A _) (A _) (A _) -> B __) :: B (HCons t (HCons t1 (HCons t2 HNil)))
> testX (\(A _) -> B HNil)           :: error
> 
> 
> This is my attempt to rephrase it using type families:
> 
>> class X' a where
>>     type L a
>>     type P a
>>     ll' :: a -> L a
>>     pp' :: a -> P a
>>
>> instance X' (B l) where
>>     type L (B l) = HNil
>>     type P (B l) = B l
>>     ll' _ = HNil
>>     pp' p = p
>>
>> instance (X' x) => X' (A t -> x) where
>>     type L (A t -> x) = HCons t (L x)
>>     type P (A t -> x) = P x
>>     ll' _ = HCons __ (ll' (__ :: x))
>>     pp' p = pp' (p (A (__ :: t)))
>>
>> -- (inferred)
>> -- testX' :: (B (L a) ~ P a, X' a) => a -> P a
>> testX' x = pp' x `asTypeOf` B (ll' x)
> 
> Only the X' (B l) instance works, the other produces a strange error:
> 
> testX' (B __)           :: P (B HNil) :: B HNil
> testX' (\(A _) -> B __) :: error
> 
>     Couldn't match expected type `a'
>            against inferred type `Main.R:L(->) t (B a)'
>       Expected type: P (A t -> B a)
>       Inferred type: B (L (A t -> B a))
> 
> Unifying those two types by hand, I get:
> 
>     P (A t -> B a)
> ~>  P (B a)
> ~>  B a
> 
>     B (L (A t -> B a))
> ~>  B (HCons t (L (B a)))
> ~>  B (HCons t HNil)
> 
> Hence, a = HCons t HNil. But GHC doesn't get that.
> 
> I'm using GHC 6.12.1.
> 
> Thanks for any hints. Best regards,