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

[TP]

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