Skip to content

Instantly share code, notes, and snippets.

@oisdk

oisdk/taba.hs

Last active Feb 12, 2020
Embed
What would you like to do?
{-# 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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.