gistfile1.txt

{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators #-}

module Traversals where

import Control.Monad.Free

type (~>) f g = forall x. f x -> g x

data Nat = Z | S Nat

data HVec n f a
  where
  HNil :: a -> HVec Z f a
  HCons :: f (HVec n f a) -> HVec (S n) f a

data HFunList a b t x
  where
  HFunList :: HVec n a x -> (HVec n b x -> t x) -> HFunList a b t x

type HTraversal s t a b = s ~> HFunList a b t

test :: (Functor a, Functor b) => HTraversal (Free a) (Free b) a b
test (Pure a) = HFunList (HNil a) (\(HNil b) -> Pure b)
test (Free ar) = HFunList (HCons (_ <$> ar)) (\(HCons br) -> Free (_ <$> br))