A rather non-traditional, non-Hask functor in Haskell

NonHask.hs

{-# LANGUAGE DataKinds
           , TypeFamilies
           , TypeOperators
           , GADTs
           , KindSignatures #-}

data Nat = Z | S Nat

type family Plus n m :: Nat where
  Plus Z m = m
  Plus (S n) m = S (Plus n m)

data Vector :: * -> Nat -> * where
  Nil :: Vector a Z
  Cons :: a -> Vector a n -> Vector a (S n)

append :: Vector a n -> Vector a m -> Vector a (Plus n m)
append l r = case l of
  Nil -> r
  Cons a as -> Cons a (append as r)

data n ~> m where
  NilA  :: n ~> Z
  ConsA :: n ~> m -> n ~> Plus n m

-- Witness to the fact that `Vector a` is an object map from Nat to a subcategory
-- of Hask, Hask[Vector].
nmap :: (n ~> m) -> (Vector a n -> Vector a m)
nmap x v = case x of
  NilA    -> Nil
  ConsA q -> append v (nmap q v)

*Main> nmap (ConsA $ ConsA $ ConsA $ NilA) (Cons 2 $ Cons 1 $ Nil)

Cons 2 (Cons 1 (Cons 2 (Cons 1 (Cons 2 (Cons 1 Nil)))))