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