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! Richard On Apr 29, 2013, at 2:55 AM, TP wrote:

Thanks for pointing to "type level integers". With that I have found:

http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Type...

For example:

------------------------------- data Zero = Zero data Succ a = Succ a

class Card c where c2num:: c -> Integer

cpred::(Succ c) -> c cpred = undefined

instance Card Zero where c2num _ = 0

instance (Card c) => Card (Succ c) where c2num x = 1 + c2num (cpred x)

main = do

putStrLn $ show $ c2num (Succ (Succ Zero)) -------------------------------

I will continue to examine the topic in the following days, according to my needs.

Thanks a lot,

TP

On Sunday, April 28, 2013 07:58:58 Stephen Tetley wrote:

...

What you probably want are type level integers (naturals)

Yury Sulsky used them in the message above - basically you can't use literal numbers 1,2,3,... etc as they are values of type Int (or Integer, etc...) instead you have to use type level numbers:

data One data Two

Work is ongoing for type level numbers in GHC and there are user libraries on Hackage so there is a lot of work to crib from.

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

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