Zippy Heterogeneous Lists

Zip.hs

{-# LANGUAGE DataKinds, GADTs #-}

module Zip where

import Data.Kind (Type)

data Zippy :: (k1 -> k2 -> Type) -> [k1] -> [k2] -> Type where
  Nil  :: Zippy f '[] '[]
  (:~) :: f x y -> Zippy f xs ys -> Zippy f (x:xs) (y:ys)

newtype Fst a b = Fst{ getFst :: a }
newtype Snd a b = Snd{ getSnd :: b }

zipApply :: Zippy (->) xs ys -> Zippy Fst xs ys -> Zippy Snd xs ys
zipApply  Nil       Nil          = Nil
zipApply (f :~ fs) (Fst x :~ xs) = Snd (f x) :~ zipApply fs xs