Re: [Haskell-cafe] Fwd: Type families - how to resolve ambiguities?
On Sun, Sep 12, 2010 at 9:24 AM, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fwd: Type families - how to resolve ambiguities?
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]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Fwd: Type families - how to resolve ambiguities?
On Aug 25, 11:22 pm, Dan Doel dan.d...@gmail.com wrote:
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
