### Re: partially applied data constructor and corresponding type

TP <paratribulations <at> free.fr>

2013-05-18 21:48:38 GMT

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