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 <paratribulati...@free.fr> wrote:
> Thanks for pointing to "type level integers". With that I have found:
>
> http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Types
>
> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
