[Haskell-cafe] Type families - how to resolve ambiguities?

[DavidA]

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]))

: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]))

: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?


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Type families - how to resolve ambiguities?

[Dan Doel]

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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe