[Haskell-cafe] partially applied data constructor and corresponding type

[TP]

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