Length Indexed Matrix and Indexed Functor

IndexedMatrixAndIFunctor.hs

-- Run on GHC 7.6.1

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.List (find)


-- Nat

data Nat = Zero | Succ Nat
type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

type family (m :: Nat) + (n :: Nat) :: Nat
type instance Zero + n = n
type instance (Succ m) + n = Succ (m + n)


-- Length Indexed Vector

data Vec :: Nat -> * -> * where
  VNil  :: Vec Zero a
  VCons :: a -> Vec n a -> Vec (Succ n) a

instance Show a => Show (Vec n a) where
  showsPrec d VNil         = showString "VNil"
  showsPrec d (VCons x xs) = showParen (d > prec) $ 
                               showString "VCons "
                               . showsPrec (prec+1) x
                               . showChar ' '
                               . showParen (case xs of { VNil -> False; _ -> True }) (shows xs)
    where prec = 5

instance Functor (Vec n) where
  fmap f VNil = VNil
  fmap f (VCons x xs) = VCons (f x) (fmap f xs)


-- Length Indexed Matrix

data Matrix :: Nat -> (k -> *) -> k -> * where
  Matrix :: Vec n (f a) -> Matrix n f a

instance Show (f a) => Show (Matrix n f a) where
  showsPrec d (Matrix v) = showParen (d > prec) $
                             showString "Matrix " . showsPrec (prec+1) v
    where prec = 5

instance Functor f => Functor (Matrix n f) where
  fmap g (Matrix v) = Matrix (fmap (fmap g) v)


-- Indexed Functor

type f :~> g = forall a. f a -> g a

class IFunctor (f :: (k -> *) -> k -> *) where
  imap :: forall a b. (a :~> b) -> f a :~> f b


instance IFunctor (Matrix n) where
  imap g (Matrix v) = Matrix (fmap g v)


-- Vec transform function examples

vDupFirst :: Vec (One + n) :~> Vec (Two + n)
vDupFirst v@(VCons x _) = VCons x v

vecToList :: Vec n :~> []
vecToList VNil = []
vecToList (VCons x xs) = x : vecToList xs

usage-ghci.hs

ghci> let m = VCons 2 (VCons 3 VNil) :: Vec Two Int
ghci> let n = VCons 4 (VCons 5 VNil) :: Vec Two Int
ghci> let x = Matrix $ VCons m (VCons n VNil) :: Matrix Two (Vec Two) Int

ghci> :t x
x :: Matrix * Two (Vec Two) Int

-- Functor
ghci> fmap (*2) x
Matrix (VCons (VCons 4 (VCons 6 VNil)) (VCons (VCons 8 (VCons 10 VNil)) VNil))
ghci> :t fmap show x
fmap show x :: Matrix * Two (Vec Two) String

-- Indexed Functor
ghci> :t imap vDupFirst x
imap vDupFirst x :: Matrix * Two (Vec ('Succ ('Succ One))) Int
ghci> imap vDupFirst x
Matrix (VCons (VCons 2 (VCons 2 (VCons 3 VNil))) (VCons (VCons 4 (VCons 4 (VCons 5 VNil))) VNil))

ghci> :t imap vecToList x
imap vecToList x :: Matrix * Two [] Int
ghci> imap vecToList x
Matrix (VCons [2,3] (VCons [4,5] VNil))