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

[Ryan Ingram]

I'm pretty sure this is a bug.  My code works if I put a type
signature on your second example.

*TFInjectivity> :t testX'
testX' :: (P a ~ B (L a), X' a) => a -> B (L a)

*TFInjectivity> :t testX' (\(A _) -> B __) :: B (HCons a HNil)
testX' (\(A _) -> B __) :: B (HCons a HNil) :: B (HCons a HNil)

*TFInjectivity> :t testX' (\(A _) -> B __)

Top level:
    Couldn't match expected type `t TFInjectivity.:R1L B a'
           against inferred type `a'
      Expected type: B (L (A t -> B a))
      Inferred type: P (A t -> B a)

Here's my back-of-the-envelope thoughts on how typechecking should go:

*TFInjectivity> :t (\(A _) -> B __)
(\(A _) -> B __) :: A t -> B a

*TFInjectivity> :t testX'
testX' :: (P a ~ B (L a), X' a) => a -> B (L a)

testX' (\(A _) -> B__)

introduce variables for (\(A _) -> B__)
(\(A _) -> B __) :: A t1 -> B t2

introduce variables and desired context for testX'
testX' :: t3 -> B (L t3)

needed:
1)  P t3 ~ B (L t3),
2)   X' t3
have:
3)  t3 ~ (A t1 -> B t2)

apply (3) to (1) and (2)

needed:
4) P (A t1 -> B t2) ~ B (L (A t1 -> B t2))
5) X' (A t1 -> B t2)
apply X' instances to discharge (5)

apply P from X' instance (A t -> x) to (4)
6) P (B t2) ~ B (L (A t1 -> B t2))

apply P from X' instance (B t) to (6)
7) B t2 ~ B (L (A t1 -> B t2))

injectivity of data constructor
8) t2 ~ L (A t1 -> B t2)

(this is a very interesting unification to have to make, and might be
the heart of the problem?  it looks like an infinite type, but it's
not!)

apply L from X' instance (A t -> x) to (8)
9) t2 ~ HCons t1 (L (B t2))

apply L from X' instance (B t2) to (9)
10) t2 ~ HCons t1 HNil

unify t2 and HCons t1 HNil, discharge

testX' (\(A _) -> B __) :: B (L (A t1 -> B t2))
or, simplifying,
testX' (\(A _) -> B __) :: B (HCons t1 HNil)

(Code follows)

  -- ryan

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module TFInjectivity where

__ = undefined

data HNil = HNil
data HCons a b = HCons a b

data A a = A a
data B a = B a

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)))

testX' :: (L a ~ l, P a ~ B l, X' a) => a -> B l
testX' x = pp' x




2010/5/18 Tomáš Janoušek <tomi at nomi.cz>:
> 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,
> --
> Tomáš Janoušek, a.k.a. Liskni_si, http://work.lisk.in/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>