Richard Eisenberg wrote: > There's a lot of recent work on GHC that might be helpful to you. Is it > possible for your application to use GHC 7.6.x? If so, you could so > something like this: > > {-# LANGUAGE DataKinds, GADTs, KindSignatures #-} > > data Nat = Zero | Succ Nat > > type One = Succ Zero > type Two = Succ One > type Three = Succ Two > > -- connects the type-level Nat with a term-level construct > data SNat :: Nat -> * where > SZero :: SNat Zero > SSucc :: SNat n -> SNat (Succ n) > > zero = SZero > one = SSucc zero > two = SSucc one > three = SSucc two > > data Tensor (n :: Nat) a = MkTensor { dims :: SNat n, items :: [a] } > > type Vector = Tensor One > type Matrix = Tensor Two > > mkVector :: [a] -> Vector a > mkVector v = MkTensor { dims = one, items = v } > > vector_prod :: Num a => Vector a -> Vector a > vector_prod (MkTensor { items = v }) = ... > > specializable :: Tensor n a -> Tensor n a > specializable (MkTensor { dims = SSucc SZero, items = vec }) = ... > specializable (MkTensor { dims = SSucc (SSucc SZero), items = mat }) = ... > > > This is similar to other possible approaches with type-level numbers, but > it makes more use of the newer features of GHC that assist with type-level > computation. Unfortunately, there are no "constructor synonyms" or > "pattern synonyms" in GHC, so you can't pattern match on "MkVector" or > something similar in specializable. But, the pattern matches in > specializable are GADT pattern-matches, and so GHC knows what the value of > n, the type variable, is on the right-hand sides. This will allow you to > write and use instances of Tensor defined only at certain numbers of > dimensions. > > I hope this is helpful. Please write back if this technique is unclear!
Thanks a lot! Those days I have read about "DataKinds" extension (with help of Haskell-Cafe guys), and now I am able to understand your code. The technique to connect the type-level and term-level integers allows to duplicate information (duplicate information needed because of my more or less clear requirements in my previous posts), but in a safe way (i.e. with no copy/paste error): if I change "one" in "two" in the definition of the smart constructor mkVector, I obtain an error, as expected because of the use of type variable n on both sides of the equality in Tensor type definition (and then we understand why the type constructor SNat has been introduced). This is a working example (this is not exactly what I will do at the end, but it is very instructive! One more time, thanks!): -------------------------------------- {-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving #-} data Nat = Zero | Succ Nat type One = Succ Zero type Two = Succ One type Three = Succ Two -- connects the type-level Nat with a term-level construct data SNat :: Nat -> * where SZero :: SNat Zero SSucc :: SNat n -> SNat (Succ n) deriving instance Show (SNat a) zero = SZero one = SSucc zero two = SSucc one three = SSucc two data Tensor (n :: Nat) a = MkTensor { order :: SNat n, items :: [a] } deriving Show type Vector = Tensor One type Matrix = Tensor Two mkVector :: [a] -> Vector a mkVector v = MkTensor { order = one, items = v } -- some dummy operation defined between two Vectors (and not other order -- tensors), which results in a Vector. some_operation :: Num a => Vector a -> Vector a -> Vector a some_operation (MkTensor { items = v1 }) (MkTensor { items = v2 }) = mkVector (v1 ++ v2) main = do let va = mkVector ([1,2,3] :: [Integer]) let vb = mkVector ([4,5,6] :: [Integer]) print $ some_operation va vb print $ order va print $ order vb --------------------------------- _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe