Thanks a lot for your message. I can use a recent version of GHC 7.6.x (I will install the last version of Kubuntu for that purpose). However, it will take me some time to understand correctly this code (e.g. I do not know "data kinds"), I will go back to you if I encounter difficulties. Thanks, TP On Monday, April 29, 2013 08:19:43 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!
Richard