Fwd: Type families - how to resolve ambiguities?
On Aug 25, 11:22 pm, Dan Doel
On Wednesday 25 August 2010 5:05:11 pm DavidA wrote:
The code below defines a type synonym family:
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-} {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
[snip]
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?
However, it would make more sense to have it be a type family, without the overhead of data (both in space and in typing). Is there a non- hacky approach, without dummies and without making Tensor a data family without a semantic need? I am having a similar problem with the vector package, with the Data.Vector.Generic.Mutable module, because of the PrimState type family. How am I expected to best solve this? This function is easy to write: fillVector n elems = do arr <- VectorGM.new n VectorG.copy arr $ VectorG.fromList elems return arr However, what I have below is not easy to write for me - some specific type annotations are needed. Interestingly, I needed to annotate a statement rather than the return value, because unifying PrimState IO and PrimState m fails, rather than producing m = IO. While I managed to make them work, it looks like type inference is not helping much - the code seems more complicated to properly type-annotate than it would be in a language with just typechecking. V1, not generic - it works for arrays of integers: fillSortVector n elems = do arr <- VectorGM.new n :: IO (VectorU.MVector (PrimState IO) Int) -- I can't annotate just arr, I need to annotate the IO action! -- arr :: (VectorU.MVector (PrimState IO) Int) <- VectorGM.new n -- doesn't compile! let arrI :: VectorU.Vector Int = VectorG.fromList elems VectorG.copy arr arrI (timing, _) <- timed $ VectorI.sort arr return timing V2, almost fully generic - but not in the array types (that was even more complicated IIRC): fillSortVector :: forall a. (Ord a, VectorG.Vector VectorU.Vector a, VectorGM.MVector VectorU.MVector a) => Int -> [a] -> IO Double fillSortVector n elems = do arr <- VectorGM.new n :: IO (VectorU.MVector (PrimState IO) a) -- I can't annotate just arr, I need to annotate the IO action! -- arr :: (VectorU.MVector (PrimState IO) a) <- VectorGM.new n -- doesn't compile! let arrI :: VectorU.Vector a = VectorG.fromList elems VectorG.copy arr arrI (timing, _) <- timed $ VectorI.sort arr return timing Best regards Paolo G. Giarrusso -- PhD student
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
Paolo, 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]
On Sun, Sep 12, 2010 at 9:24 AM, Dominique Devriese
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.
Which is only at programming time; newtype constructors do not exist at runtime. They get erased after typechecking. This also means that pattern matching against newtype constructors cannot fail. For example:
data family F a data instance F Bool = B () newtype instance F Int = I ()
fBool :: F Bool -> Int f1 (B _) = 3
fInt :: F Int -> Int f2 (I _) = 4
main = do print (fInt undefined) print (fBool undefined)
This program should print 4 and then exit with an error. -- ryan
participants (3)
-
Dominique Devriese -
Paolo Giarrusso -
Ryan Ingram