Type families vs. functional dependencies -- how to express something

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Type families vs. functional dependencies -- how to express something

Tomáš Janoušek
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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@.../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,

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type families vs. functional dependencies -- how to express something

Tomáš Janoušek
Hello,

On Tue, May 18, 2010 at 04:47:50PM -0700, Dan Weston wrote:

> > 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@.../msg63359.html

That's probably it, thanks. I think I'll just stay with functional
dependencies this time, a data type with wrapping and unwrapping can't
possibly make the code more readable :-).

Regards,
--
Tomáš Janoušek, a.k.a. Liskni_si, http://work.lisk.in/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type families vs. functional dependencies -- how to express something

Ryan Ingram
In reply to this post by Tomáš Janoušek
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 <[hidden email]>:

> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe