Epilogue

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# OPTIONS #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE KindSignatures #-}

> module Vec where

> import Control.Applicative

> data Nat = Z | S Nat

> data Vec :: {Nat} -> * -> * where
>   VNil :: Vec {Z} x
>   (:>) :: x -> Vec {n} x -> Vec {S n} x

> vtail :: Vec {S n} x -> Vec {n} x
> vtail (x :> xs) = xs

> vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t
> vapp VNil VNil = VNil
> vapp (f :> fs) (s :> ss) = f s :> vapp fs ss

Yes, in a manner of speaking. But you need a bit of

darcs get http://personal.cis.strath.ac.uk/~conor/pub/she

Update: she’s on hackage!

Update: I had to…

> type family (m :: {Nat}) :+ (n :: {Nat}) :: {Nat}
> type instance {Z} :+ n = n
> type instance {S m} :+ n = {S} (m :+ n)

> vappend :: Vec m x -> Vec n x -> Vec (m :+ n) x
> vappend VNil ys = ys
> vappend (x :> xs) ys = x :> vappend xs ys

This entry was posted on Tuesday, June 30th, 2009 at 7:37 pm and is filed under General. You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.