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

[Dominique Devriese]

Paolo,

>> 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:
> [...]
>> or, to make Tensor a data family instead of a type family.
> What is the difference making it work?
The problem is that in your definition of mult
  mult :: Tensor k v v -> v
you seem to expect the type v to be determined by the type of Tensor
you apply it to. However, since Tensor is not an injective type
functor, it does not uniquely determine the type v. It is possible
that there is a completely unrelated type instance for Tensor, for
different types k and v that is also equal to the type you apply mult
to.

If you make Tensor a data family, then the types k and v are uniquely
determined, because then it is an injective type functor.

> However, it would make more sense to have it be a type family, without
> the overhead of data (both in space and in typing).

You can make Tensor a data family and use "newtype instances". As I
understand these, there should not be a space overhead. The only
overhead I would expect this to introduce is the extra newtype
constructor.

> Is there a non-
> hacky approach, without dummies and without making Tensor a data
> family without a semantic need?

Without thinking about your problem domain, I have the impression that
you do have a semantic need, because you seem to expect your Tensor
type to uniquely determine at least the type v. If this is not the
case, you need a different solution.

Anyway, the below compiles fine with the following result:
*Main> mult $ Tensor $ (V [(T [1] [2],3)] :: Vect Integer (TensorBasis
[Int] [Int]))
V [([1,2],3)]

{-# 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)

data family Tensor k u v :: *

newtype instance Tensor k (Vect k a) (Vect k b) = Tensor (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 (Tensor (V ts)) = V [(g++h,x) | (T g h, x) <- ts]