type.hs

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

data V (n::Nat) = V
  deriving Show

data M (n::Nat) (m::Nat) = M
  deriving Show


type family Add (x :: Nat) (y :: Nat) :: Nat where
  Add x y = x+y

type family Mul (x :: Nat) (y :: Nat) :: Nat where
  Mul x y = x*y

add :: (KnownNat n, KnownNat m) => V n -> V m -> V (Add n m)
add _ _ = V

mul :: (KnownNat m, KnownNat n, KnownNat o)
    => M m n
    -> M n o
    -> M m o
mul _ _ = M

reshape :: (KnownNat m, KnownNat n, KnownNat o, KnownNat p, (m * n) ~ (o * p))
        => M o p
        -> M m n
reshape _ = M

eq' :: (KnownNat n) => V n -> V n -> V n
eq' a _ = a


main = do
  let v1 = V :: V 1
      v2 = V :: V 2
      v3 = V :: V 3
      m1 = M :: M 4 2
      m2 = reshape m1 :: M 1 8
  print $ natVal $ m2
  print $ natVal $ eq' (add v1 v2) v3