[Haskell-cafe] Type families and kind signatures
The following module does not compile, and I can't figure out why:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
module Foo where
import Control.Monad
import Data.Maybe
class Key k where
type Map k :: * - *
empty :: Map k v
look :: k - Map k v - Maybe v
update :: k - (Maybe v - Maybe v) - Map k v - Map k v
instance (Key k1, Key k2) = Key (k1, k2) where
type Map (k1, k2) v = Map k1 (Map k2 v)
empty = empty
update (k1, k2) f = update k1 (update k2 f . fromMaybe empty)
look (k1, k2) = look k1 = look k2
The compile fails with
Foo.hs:16:1:
Number of parameters must match family declaration; expected 1
In the type synonym instance declaration for `Map'
In the instance declaration for `Key (k1, k2)'
Is this a bug with type synonym families? Is there something silly I'm
missing?
Louis Wasserman
wasserman.lo...@gmail.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
2009/4/2 Louis Wasserman wasserman.lo...@gmail.com
The following module does not compile, and I can't figure out why:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
module Foo where
import Control.Monad
import Data.Maybe
class Key k where
type Map k :: * - *
empty :: Map k v
look :: k - Map k v - Maybe v
update :: k - (Maybe v - Maybe v) - Map k v - Map k v
instance (Key k1, Key k2) = Key (k1, k2) where
type Map (k1, k2) v = Map k1 (Map k2 v)
The arity of the instance has to be *exactly* the same as is declared. So
the v is one too many parameters. That does make your life a little more
difficult (but points to an abstraction you may not have seen :-).
I would resolve this as:
type Map (k1,k2) = Map k1 `O` Map k2
Where O is functor composition from TypeCompose on hackage.
empty = empty
update (k1, k2) f = update k1 (update k2 f . fromMaybe empty)
look (k1, k2) = look k1 = look k2
The compile fails with
Foo.hs:16:1:
Number of parameters must match family declaration; expected 1
In the type synonym instance declaration for `Map'
In the instance declaration for `Key (k1, k2)'
Is this a bug with type synonym families? Is there something silly I'm
missing?
Louis Wasserman
wasserman.lo...@gmail.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
Mkay. One more quick thing -- the wiki demonstrates a place where the
original attempt worked, with a data family instead. (That is, replacing
'type' with 'data' and adjusting the instance makes this program compile
immediately.)
a) Is there a type-hackery reason this is different from data families?
b) Is there a reason this isn't made a lot clearer in the documentation?
GHC's docs say that higher-order type families can be declared with kind
signatures, but never gives any examples -- which would make it a lot
clearer that the below program doesn't work.
Louis Wasserman
wasserman.lo...@gmail.com
On Thu, Apr 2, 2009 at 12:05 PM, Luke Palmer lrpal...@gmail.com wrote:
2009/4/2 Louis Wasserman wasserman.lo...@gmail.com
The following module does not compile, and I can't figure out why:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
module Foo where
import Control.Monad
import Data.Maybe
class Key k where
type Map k :: * - *
empty :: Map k v
look :: k - Map k v - Maybe v
update :: k - (Maybe v - Maybe v) - Map k v - Map k v
instance (Key k1, Key k2) = Key (k1, k2) where
type Map (k1, k2) v = Map k1 (Map k2 v)
The arity of the instance has to be *exactly* the same as is declared. So
the v is one too many parameters. That does make your life a little more
difficult (but points to an abstraction you may not have seen :-).
I would resolve this as:
type Map (k1,k2) = Map k1 `O` Map k2
Where O is functor composition from TypeCompose on hackage.
empty = empty
update (k1, k2) f = update k1 (update k2 f . fromMaybe empty)
look (k1, k2) = look k1 = look k2
The compile fails with
Foo.hs:16:1:
Number of parameters must match family declaration; expected 1
In the type synonym instance declaration for `Map'
In the instance declaration for `Key (k1, k2)'
Is this a bug with type synonym families? Is there something silly I'm
missing?
Louis Wasserman
wasserman.lo...@gmail.com
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
2009/4/2 Louis Wasserman wasserman.lo...@gmail.com: Mkay. One more quick thing -- the wiki demonstrates a place where the original attempt worked, with a data family instead. (That is, replacing 'type' with 'data' and adjusting the instance makes this program compile immediately.) a) Is there a type-hackery reason this is different from data families? It's not type hackery. Data families are different from type families, and the syntax for declaring instances of higher-kinded families is a consequence of those differences. An instance of a data family is a new type constructor, so you have to provide the additional arguments in order to declare the data constructors. data family Foo a :: * - * data instance Foo Bool a = FB a a -- Foo Bool has kind * - *, like [], so I could make it a Functor Instance of type families are always pre-existing type constructors. type family Bar a :: * - * -- Bar a must equal something of kind * - * type instance Bar () = Maybe b) Is there a reason this isn't made a lot clearer in the documentation? GHC's docs say that higher-order type families can be declared with kind signatures, but never gives any examples -- which would make it a lot clearer that the below program doesn't work. Here's a higher-kinded type family I've used. type family Sig t :: * - * class (Traversable (Sig t)) = Recursive t where roll :: Sig t t - t unroll :: t - Sig t t The Traversable context wouldn't be valid if I had declared Sig t a :: *, because type families must always be fully applied. The difference is analogous to the difference between type M0 a = StateT Int IO a type M1 = StateT Int IO Since type synonyms (like type and data families) must always be fully applied, you can use M1 in places where you can't use M0, even though they're effectively the same thing. foo :: ErrorT String M1 a -- valid bar :: ErrorT String M0 a -- not valid -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
Mkay. I get it now. I was under the impression that, essentially, a data family was precisely equivalent to a type family aliasing to a separately declared datatype. One more question: is there any way to get the low overhead of newtypes for particular instances of a data family? Is this impossible? That is, is there any way to do something like data family Foo a data instance Foo Int = Bar Int -- Bar is actually a newtype Louis Wasserman wasserman.lo...@gmail.com On Thu, Apr 2, 2009 at 12:47 PM, David Menendez d...@zednenem.com wrote: 2009/4/2 Louis Wasserman wasserman.lo...@gmail.com: Mkay. One more quick thing -- the wiki demonstrates a place where the original attempt worked, with a data family instead. (That is, replacing 'type' with 'data' and adjusting the instance makes this program compile immediately.) a) Is there a type-hackery reason this is different from data families? It's not type hackery. Data families are different from type families, and the syntax for declaring instances of higher-kinded families is a consequence of those differences. An instance of a data family is a new type constructor, so you have to provide the additional arguments in order to declare the data constructors. data family Foo a :: * - * data instance Foo Bool a = FB a a -- Foo Bool has kind * - *, like [], so I could make it a Functor Instance of type families are always pre-existing type constructors. type family Bar a :: * - * -- Bar a must equal something of kind * - * type instance Bar () = Maybe b) Is there a reason this isn't made a lot clearer in the documentation? GHC's docs say that higher-order type families can be declared with kind signatures, but never gives any examples -- which would make it a lot clearer that the below program doesn't work. Here's a higher-kinded type family I've used. type family Sig t :: * - * class (Traversable (Sig t)) = Recursive t where roll :: Sig t t - t unroll :: t - Sig t t The Traversable context wouldn't be valid if I had declared Sig t a :: *, because type families must always be fully applied. The difference is analogous to the difference between type M0 a = StateT Int IO a type M1 = StateT Int IO Since type synonyms (like type and data families) must always be fully applied, you can use M1 in places where you can't use M0, even though they're effectively the same thing. foo :: ErrorT String M1 a -- valid bar :: ErrorT String M0 a -- not valid -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families and kind signatures
Louis Wasserman: Mkay. I get it now. I was under the impression that, essentially, a data family was precisely equivalent to a type family aliasing to a separately declared datatype. No, they are not equivalent. You can see that as follows. Assume, data family T a type family S a Now, given `T a ~ T b', we know that `a ~ b'. (We call this implication decomposition.) In contrast, given `S a ~ S b' we do *not* know whether `a ~ b'. Why not? Consider the instances type instance S Int = Bool type instance S Float = Bool Clearly, `S Int ~ S Float', but surely not `Int ~ Float'. So, decomposition does not hold for type synonym families, but it does hold for data families. This is actually, not really a property of type *families* alone. It already distinguishes vanilla data types from vanilla type synonyms. We know, say, that if `Maybe a ~ Maybe b', then `a ~ b'. However, given type Const a = Int we have `Const Int ~ Const Float' (and still not `Int ~ Float'). Definitions, such as that of `Const', are rarely used, which is why this issue doesn't come up much until you use type families. One more question: is there any way to get the low overhead of newtypes for particular instances of a data family? Is this impossible? That is, is there any way to do something like data family Foo a data instance Foo Int = Bar Int -- Bar is actually a newtype You can use newtype instance Foo Int = MkFoo Int So, the instances of a data family can be data or newtype instances., and you can freely mix them. Manuel On Thu, Apr 2, 2009 at 12:47 PM, David Menendez d...@zednenem.com wrote: 2009/4/2 Louis Wasserman wasserman.lo...@gmail.com: Mkay. One more quick thing -- the wiki demonstrates a place where the original attempt worked, with a data family instead. (That is, replacing 'type' with 'data' and adjusting the instance makes this program compile immediately.) a) Is there a type-hackery reason this is different from data families? It's not type hackery. Data families are different from type families, and the syntax for declaring instances of higher-kinded families is a consequence of those differences. An instance of a data family is a new type constructor, so you have to provide the additional arguments in order to declare the data constructors. data family Foo a :: * - * data instance Foo Bool a = FB a a -- Foo Bool has kind * - *, like [], so I could make it a Functor Instance of type families are always pre-existing type constructors. type family Bar a :: * - * -- Bar a must equal something of kind * - * type instance Bar () = Maybe b) Is there a reason this isn't made a lot clearer in the documentation? GHC's docs say that higher-order type families can be declared with kind signatures, but never gives any examples -- which would make it a lot clearer that the below program doesn't work. Here's a higher-kinded type family I've used. type family Sig t :: * - * class (Traversable (Sig t)) = Recursive t where roll :: Sig t t - t unroll :: t - Sig t t The Traversable context wouldn't be valid if I had declared Sig t a :: *, because type families must always be fully applied. The difference is analogous to the difference between type M0 a = StateT Int IO a type M1 = StateT Int IO Since type synonyms (like type and data families) must always be fully applied, you can use M1 in places where you can't use M0, even though they're effectively the same thing. foo :: ErrorT String M1 a -- valid bar :: ErrorT String M0 a -- not valid -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
