[Haskell-cafe] Type families vs. functional dependencies -- how to
express something
Tomáš Janoušek
tomi at nomi.cz
Tue May 18 19:13:09 EDT 2010
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/
More information about the Haskell-Cafe
mailing list