Type families - how to resolve ambiguities?
Hi, The code below defines a type synonym family: {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-} data Vect k b = V [(b,k)] deriving (Eq,Show) data TensorBasis a b = T a b deriving (Eq, Ord, Show) type family Tensor k u v :: * type instance Tensor k (Vect k a) (Vect k b) = Vect k (TensorBasis a b) class Algebra k v where -- "v is a k-algebra" unit :: k -> v mult :: Tensor k v v -> v instance Algebra Integer (Vect Integer [Int]) where unit 0 = V [] unit x = V [([],x)] mult (V ts) = V [(g++h,x) | (T g h, x) <- ts] Naively I think of the type instance declaration as saying that the two types are synonyms, so I should be able to use one in a context where the other is expected. However, when I try to use the code, I don't seem to be able to get the type inferencer to recognise an object as being of both "types" at the same time. For example: *> mult $ (V [(T [1] [2],3)] :: Vect Integer (TensorBasis [Int] [Int])) <interactive>:1:8: Couldn't match expected type `Tensor k v v' against inferred type `Vect Integer (TensorBasis [Int] [Int])' NB: `Tensor' is a type function, and may not be injective In the second argument of `($)', namely `(V [(T [1] [2], 3)] :: Vect Integer (TensorBasis [Int] [Int]))' In the expression: mult $ (V [(T [1] [2], 3)] :: Vect Integer (TensorBasis [Int] [Int])) In the definition of `it': it = mult $ (V [(T [1] [2], 3)] :: Vect Integer (TensorBasis [Int] [Int])) *> mult $ (V [(T [1] [2],3)] :: Tensor Integer (Vect Integer [Int]) (Vect Integer [Int])) <interactive>:1:8: Couldn't match expected type `Tensor k v v' against inferred type `Vect Integer (TensorBasis [Int] [Int])' NB: `Tensor' is a type function, and may not be injective In the second argument of `($)', namely `(V [(T [1] [2], 3)] :: Tensor Integer (Vect Integer [Int]) (Vect Integer [Int]))' In the expression: mult $ (V [(T [1] [2], 3)] :: Tensor Integer (Vect Integer [Int]) (Vect Integer [Int])) In the definition of `it': it = mult $ (V [(T [1] [2], 3)] :: Tensor Integer (Vect Integer [Int]) (Vect Integer [Int])) Are type families the right mechanism to express what I'm trying to express? If so, what am I doing wrong, and how do I fix it?
On Wednesday 25 August 2010 5:05:11 pm DavidA wrote:
Hi,
The code below defines a type synonym family:
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
data Vect k b = V [(b,k)] deriving (Eq,Show)
data TensorBasis a b = T a b deriving (Eq, Ord, Show)
type family Tensor k u v :: *
type instance Tensor k (Vect k a) (Vect k b) = Vect k (TensorBasis a b)
class Algebra k v where -- "v is a k-algebra" unit :: k -> v mult :: Tensor k v v -> v
instance Algebra Integer (Vect Integer [Int]) where unit 0 = V [] unit x = V [([],x)] mult (V ts) = V [(g++h,x) | (T g h, x) <- ts]
Naively I think of the type instance declaration as saying that the two types are synonyms, so I should be able to use one in a context where the other is expected. However, when I try to use the code, I don't seem to be able to get the type inferencer to recognise an object as being of both "types" at the same time. For example:
Are type families the right mechanism to express what I'm trying to express? If so, what am I doing wrong, and how do I fix it?
The problem with mult is that k is not specified unambiguously. You either need v to determine k (which is probably not what you want, at a guess), mult to take a dummy argument that determines what k is: mult :: k -> Tensor k v v -> v or mult :: D k -> Tensor k v v -> v -- D k being some datatype or, to make Tensor a data family instead of a type family. If you used functional dependencies, for instance, this would be something like: class Algebra k v t | k v -> t where unit :: k -> v mult :: t -> v and mult is obviously problematic in not mentioning all the necessary parameters. -- Dan
participants (2)
-
Dan Doel -
DavidA