Trying to sort out multiparameter type classes and their instances
I'm playing around with some types to represent a game board (like Go, Chess, Scrabble, etc). I'm using a type class to represent the basic Board interface, so I can change the implementation freely: class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece -- Query pos to get piece (Nothing if off board) at :: b pos piece -> pos -> Maybe piece -- Empty board empty :: b pos piece and a Position on the board is represented thus: class Position p where up :: p -> p down :: p -> p left :: p -> p right :: p -> p With a concrete implementation using a tuple: instance (Enum c,Enum r) => Position (c,r) where up = second pred down = second succ left = first pred right = first succ My initial Board is a function: position -> Maybe piece, but I'm having a hard time writing the instance for it. My first attempt is: instance Board (pos -> Maybe piece) pos piece where empty = \_ -> Nothing at = ($) play b pos piece = move where move pos' | pos' == pos = Just piece | otherwise = b pos' but ghci complains: board.hs:34:15: Kind mis-match Expected kind `* -> * -> *', but `pos -> Maybe piece' has kind `*' In the instance declaration for `Board (pos -> Maybe piece) pos piece' Playing around with parentheses on the instance line got various similar messages, but I couldn't get anything to work. What am I missing here? One thing that strikes me is that "Board (pos -> Maybe piece) pos piece" has a lot of redundancy, and I'm wondering if I'm defining the Board type class wrong in the first place. Given that the "b" type parameter necessarily defines the position and pieces, I tried using dependent types: class Board b | b -> pos, b -> piece where ... but this complains "Not in scope: type variable `pos'/`piece'", so I tried sprinkling some existential types around as well: class (forall pos piece. b pos piece) => Board b | b -> pos, b -> piece where ... (with and without the dependent types) but this just complains "malformed class assertion". As you can probably tell, I'm just thrashing around trying things without really understanding what's going on here, so I'm hoping someone can give me some useful pointers. J
Am Dienstag 01 Dezember 2009 23:34:46 schrieb Jeremy Fitzhardinge:
I'm playing around with some types to represent a game board (like Go, Chess, Scrabble, etc).
I'm using a type class to represent the basic Board interface, so I can change the implementation freely:
class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece
So the parameter b of the class is a type constructor taking two types and constructing a type from those. IOW, it's a type constructor of kind (* -> * -> *), like (->) or Either. (* is the kind of types [Int, Char, Either Bool (), Double -> Rational -> Int, ...]
-- Query pos to get piece (Nothing if off board) at :: b pos piece -> pos -> Maybe piece -- Empty board empty :: b pos piece
and a Position on the board is represented thus:
class Position p where up :: p -> p down :: p -> p left :: p -> p right :: p -> p
With a concrete implementation using a tuple:
instance (Enum c,Enum r) => Position (c,r) where up = second pred down = second succ left = first pred right = first succ
My initial Board is a function: position -> Maybe piece, but I'm having a hard time writing the instance for it. My first attempt is:
instance Board (pos -> Maybe piece) pos piece where empty = \_ -> Nothing at = ($) play b pos piece = move where move pos' | pos' == pos = Just piece
| otherwise = b pos'
but ghci complains: board.hs:34:15: Kind mis-match Expected kind `* -> * -> *', but `pos -> Maybe piece' has kind `*' In the instance declaration for `Board (pos -> Maybe piece) pos piece'
Yes, as said above. (pos -> Maybe piece) is a *type*, but the type class expects a type constructor of kind (* -> * ->*) here.
Playing around with parentheses on the instance line got various similar messages, but I couldn't get anything to work.
What am I missing here?
One thing that strikes me is that "Board (pos -> Maybe piece) pos piece" has a lot of redundancy, and I'm wondering if I'm defining the Board type class wrong in the first place.
Given that the "b" type parameter necessarily defines the position and pieces, I tried using dependent types:
class Board b | b -> pos, b -> piece where ...
Method 1: The class above, with a modified instance. newtype Brd pos piec = Brd { mpiece :: pos -> Maybe piece } instance (Eq pos) => Board Brd pos piece where play b pos piece = Brd $ \p -> if p == pos then Just piece else mpiece b pos ... Perhaps not truly satisfying. Method 2: Multiparameter type class with functional dependencies and suitable kinds class Board b pos piece | b -> pos, b -> piece where play :: b -> pos -> piece -> b at :: b -> pos -> Maybe piece empty :: b instance (Eq pos) => Board (pos -> Maybe piece) pos piece where play b pos piece = \p -> if p == pos then Just piece else b p at = id empty = const Nothing requires {-# LANGUAGE FlexibleInstances #-} Not necessarily ideal either. Method 3: Associated type families {-# LANGUAGE TypeFamilies, FlexibleInstances #-} module Board where class Board b where type Pos b :: * type Piece b :: * play :: b -> Pos b -> Piece b -> b at :: b -> Pos b -> Maybe (Piece b) empty :: b instance (Eq pos) => Board (pos -> Maybe piece) where type Pos (pos -> Maybe piece) = pos type Piece (pos -> Maybe piece) = piece play b pos piece = \p -> if p == pos then Just piece else b p at b p = b p empty _ = Nothing I would try that first. Choose your pick.
On 12/01/09 15:12, Daniel Fischer wrote:
Am Dienstag 01 Dezember 2009 23:34:46 schrieb Jeremy Fitzhardinge:
I'm playing around with some types to represent a game board (like Go, Chess, Scrabble, etc).
I'm using a type class to represent the basic Board interface, so I can change the implementation freely:
class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece
So the parameter b of the class is a type constructor taking two types and constructing a type from those.
Yep.
IOW, it's a type constructor of kind (* -> * -> *), like (->) or Either. (* is the kind of types [Int, Char, Either Bool (), Double -> Rational -> Int, ...]
[...]
but ghci complains: board.hs:34:15: Kind mis-match Expected kind `* -> * -> *', but `pos -> Maybe piece' has kind `*' In the instance declaration for `Board (pos -> Maybe piece) pos piece'
Yes, as said above. (pos -> Maybe piece) is a *type*, but the type class expects a type constructor of kind (* -> * ->*) here.
I thought "(pos -> Maybe piece) pos piece" would provide the 3 type arguments to Board. Oh, I see my mistake. I was seeing "b pos piece" as type parameters for Board, but actually Board is just taking a single parameter of kind * -> * -> *.
Method 2: Multiparameter type class with functional dependencies and suitable kinds
class Board b pos piece | b -> pos, b -> piece where play :: b -> pos -> piece -> b at :: b -> pos -> Maybe piece empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) pos piece where play b pos piece = \p -> if p == pos then Just piece else b p at = id empty = const Nothing
requires {-# LANGUAGE FlexibleInstances #-}
Not necessarily ideal either.
OK, but that's pretty much precisely what I was aiming for. I'm not sure I understand what the difference between play :: b pos piece -> pos -> piece -> b pos piece and play :: b -> pos -> piece -> b is. Does adding type params to b here change its kind?
Method 3: Associated type families
{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module Board where
class Board b where type Pos b :: * type Piece b :: * play :: b -> Pos b -> Piece b -> b at :: b -> Pos b -> Maybe (Piece b) empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) where type Pos (pos -> Maybe piece) = pos type Piece (pos -> Maybe piece) = piece play b pos piece = \p -> if p == pos then Just piece else b p at b p = b p empty _ = Nothing
I would try that first.
OK, there's some new stuff there I'm going to have to digest... Thanks very much, J
Am Mittwoch 02 Dezember 2009 01:43:04 schrieb Jeremy Fitzhardinge:
On 12/01/09 15:12, Daniel Fischer wrote:
Am Dienstag 01 Dezember 2009 23:34:46 schrieb Jeremy Fitzhardinge:
I'm playing around with some types to represent a game board (like Go, Chess, Scrabble, etc).
I'm using a type class to represent the basic Board interface, so I can change the implementation freely:
class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece
So the parameter b of the class is a type constructor taking two types and constructing a type from those.
Yep.
IOW, it's a type constructor of kind (* -> * -> *), like (->) or Either. (* is the kind of types [Int, Char, Either Bool (), Double -> Rational -> Int, ...]
[...]
but ghci complains: board.hs:34:15: Kind mis-match Expected kind `* -> * -> *', but `pos -> Maybe piece' has kind `*' In the instance declaration for `Board (pos -> Maybe piece) pos piece'
Yes, as said above. (pos -> Maybe piece) is a *type*, but the type class expects a type constructor of kind (* -> * ->*) here.
I thought "(pos -> Maybe piece) pos piece" would provide the 3 type arguments to Board.
Oh, I see my mistake. I was seeing "b pos piece" as type parameters for Board, but actually Board is just taking a single parameter of kind * -> * -> *.
No. class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece the class Board takes three parameters: b, pos and piece. The (first) argument of play is the type (kind *) b pos piece Thus b is a type constructor taking two arguments. Since the arguments it takes, pos and piece, appear as the types of the second and third argument of play, these two must be plain types (kind *). Thus b :: * -> * -> * But in your instance declaration, in the position of b, you pass (pos -> Maybe piece), which is a type (kind *) and not a binary type constructor as required by the class declaration. If Haskell had type-level lambdas, what you would have needed to pass there is (/\ t1 t2. (t1 -> Maybe t2)) (or, if Haskell had type-constructor composition: ((. Maybe) . (->)) ) However, Haskell has neither type-level lambdas nor type-constructor composition, so you can't. You can only emulate that by using newtypes, hence Method 1 in my reply.
Method 2: Multiparameter type class with functional dependencies and suitable kinds
class Board b pos piece | b -> pos, b -> piece where play :: b -> pos -> piece -> b at :: b -> pos -> Maybe piece empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) pos piece where play b pos piece = \p -> if p == pos then Just piece else b p at = id empty = const Nothing
requires {-# LANGUAGE FlexibleInstances #-}
Not necessarily ideal either.
OK, but that's pretty much precisely what I was aiming for. I'm not sure I understand what the difference between
play :: b pos piece -> pos -> piece -> b pos piece
and
play :: b -> pos -> piece -> b
is. Does adding type params to b here change its kind?
That's not quite correctly expressed, but basically, yes, that's it. Any type expression that may legally appear to the left or right of '->' in a type signature has kind *. A type expression that takes parameters has a different kind, if it takes one plain type to produce a plain type, it has kind (* -> *), examples: [], Maybe. If it takes two plain types to produce a plain type, it has kind (* -> * -> *), examples: Either, (->). A type expression may also take type expressions which are not plain types to produce a plain type, for example StateT. That takes 1) the state type s (kind *) 2) the transforming (or transformed, I'm not sure about the terminology) Monad m (kind * -> *) 3) the result type a (kind *) to produce the plain type StateT s m a (kind *), hence StateT :: * -> (* -> *) -> * -> *. So with the signature play :: b -> pos -> piece -> b, b must be a plain type (elementary, like Int, Bool; or a fully applied type constructor of arity > 0, like [()], Maybe Char, Either Int Bool, ((Int,Int) -> Maybe String) or StateT [Int] Maybe Bool), that is, a type expression of kind *. With the signature play :: b pos piece -> pos -> piece -> b pos piece, b must be a type expression of arity 2, taking two plain types as arguments, that is, a type constructor of kind (* -> * -> *), like Either, State, (->) or a partially applied type constructor of higher arity like ((,,,) Int (Char ->Bool)) [the quadruple constructor (,,,) of kind (* -> * -> * -> * -> *) applied to two types, leaving two slots open].
Method 3: Associated type families
{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module Board where
class Board b where type Pos b :: * type Piece b :: * play :: b -> Pos b -> Piece b -> b at :: b -> Pos b -> Maybe (Piece b) empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) where type Pos (pos -> Maybe piece) = pos type Piece (pos -> Maybe piece) = piece play b pos piece = \p -> if p == pos then Just piece else b p at b p = b p empty _ = Nothing
I would try that first.
OK, there's some new stuff there I'm going to have to digest...
It's very becoming. Type families have several advantages over functional dependencies.
Thanks very much, J
On 12/01/09 17:38, Daniel Fischer wrote:
Am Mittwoch 02 Dezember 2009 01:43:04 schrieb Jeremy Fitzhardinge:
On 12/01/09 15:12, Daniel Fischer wrote:
Am Dienstag 01 Dezember 2009 23:34:46 schrieb Jeremy Fitzhardinge:
I'm playing around with some types to represent a game board (like Go, Chess, Scrabble, etc).
I'm using a type class to represent the basic Board interface, so I can change the implementation freely:
class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece
So the parameter b of the class is a type constructor taking two types and constructing a type from those.
Yep.
IOW, it's a type constructor of kind (* -> * -> *), like (->) or Either. (* is the kind of types [Int, Char, Either Bool (), Double -> Rational -> Int, ...]
[...]
but ghci complains: board.hs:34:15: Kind mis-match Expected kind `* -> * -> *', but `pos -> Maybe piece' has kind `*' In the instance declaration for `Board (pos -> Maybe piece) pos piece'
Yes, as said above. (pos -> Maybe piece) is a *type*, but the type class expects a type constructor of kind (* -> * ->*) here.
I thought "(pos -> Maybe piece) pos piece" would provide the 3 type arguments to Board.
Oh, I see my mistake. I was seeing "b pos piece" as type parameters for Board, but actually Board is just taking a single parameter of kind * -> * -> *.
No.
class Board b pos piece where -- Update board with piece played at pos play :: b pos piece -> pos -> piece -> b pos piece
the class Board takes three parameters: b, pos and piece.
The (first) argument of play is the type (kind *)
b pos piece
Thus b is a type constructor taking two arguments. Since the arguments it takes, pos and piece, appear as the types of the second and third argument of play, these two must be plain types (kind *).
Thus
b :: * -> * -> *
But in your instance declaration, in the position of b, you pass
(pos -> Maybe piece), which is a type (kind *) and not a binary type constructor as required by the class declaration. If Haskell had type-level lambdas, what you would have needed to pass there is
(/\ t1 t2. (t1 -> Maybe t2))
(or, if Haskell had type-constructor composition: ((. Maybe) . (->)) )
However, Haskell has neither type-level lambdas nor type-constructor composition, so you can't. You can only emulate that by using newtypes, hence Method 1 in my reply.
Method 2: Multiparameter type class with functional dependencies and suitable kinds
class Board b pos piece | b -> pos, b -> piece where play :: b -> pos -> piece -> b at :: b -> pos -> Maybe piece empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) pos piece where play b pos piece = \p -> if p == pos then Just piece else b p at = id empty = const Nothing
requires {-# LANGUAGE FlexibleInstances #-}
Not necessarily ideal either.
OK, but that's pretty much precisely what I was aiming for. I'm not sure I understand what the difference between
play :: b pos piece -> pos -> piece -> b pos piece
and
play :: b -> pos -> piece -> b
is. Does adding type params to b here change its kind?
That's not quite correctly expressed, but basically, yes, that's it.
What would be the correct way to express it?
With the signature
play :: b pos piece -> pos -> piece -> b pos piece,
b must be a type expression of arity 2, taking two plain types as arguments, that is, a type constructor of kind (* -> * -> *), like Either, State, (->) or a partially applied type constructor of higher arity like ((,,,) Int (Char ->Bool)) [the quadruple constructor (,,,) of kind (* -> * -> * -> * -> *) applied to two types, leaving two slots open].
OK, I think I understand now. It helps explain my questions about the types of "first" and "second", which I always use on tuples, but their types are much more general.
Method 3: Associated type families
{-# LANGUAGE TypeFamilies, FlexibleInstances #-} module Board where
class Board b where type Pos b :: * type Piece b :: * play :: b -> Pos b -> Piece b -> b at :: b -> Pos b -> Maybe (Piece b) empty :: b
instance (Eq pos) => Board (pos -> Maybe piece) where type Pos (pos -> Maybe piece) = pos type Piece (pos -> Maybe piece) = piece play b pos piece = \p -> if p == pos then Just piece else b p at b p = b p empty _ = Nothing
I would try that first.
OK, there's some new stuff there I'm going to have to digest...
It's very becoming. Type families have several advantages over functional dependencies.
Could you go into more detail about the advantages? Thanks, J
participants (2)
-
Daniel Fischer -
Jeremy Fitzhardinge