taba.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators  #-}

import Data.Kind
import Data.Coerce

data Nat = Z | S Nat

data Vec (a :: Type) (n :: Nat) where
  Nil :: Vec a Z
  (:-) :: a -> Vec a n -> Vec a (S n)

newtype (:.:) (f :: b -> Type) (g :: a -> b) (x :: a) = Comp { unComp :: f (g x) }

foldlVec :: forall a b n. (forall m. a -> b m -> b (S m)) -> b Z -> Vec a n -> b n
foldlVec f b Nil = b
foldlVec f b (x :- xs) = unComp (foldlVec (c f) (Comp (f x b)) xs)
  where
    c :: (a -> b (S m) -> b (S (S m))) -> (a -> (b :.: S) m -> (b :.: S) (S m))
    c = coerce
    {-# INLINE c #-}

newtype VecCont a b n = VecCont { runVecCont :: Vec b n -> Vec (a,b) n }

revZip :: Vec a n -> Vec b n -> Vec (a,b) n
revZip = runVecCont . 
  foldlVec
      (\x k -> VecCont (\(y :- ys) -> (x,y) :- runVecCont k ys))
      (VecCont (const Nil))