recursion-schemeをGADTとDataKindsで

recursion-schemeではdata familiesを用いている為形状の違う関手毎に別のデータ構築子を用意してやらなければいけない。
そこでDependently Typed Programming in Agdaの3.2の手法をHaskellで実装した。
WrapFunctorは型族Evalに対して部分適用を行う為のラッパーである。

{-# LANGUAGE GADTs, TypeOperators, KindSignatures, TypeFamilies, DataKinds, PolyKinds, RankNTypes, FlexibleInstances, TemplateHaskell, ScopedTypeVariables, FlexibleContexts #-}
module Main where

import Unsafe.Coerce
import Numeric.Natural
import Test.QuickCheck

-- 関手の形状を定義するDSL
data Univ where
    (:+:) :: Univ -> Univ -> Univ
    (:*:) :: Univ -> Univ -> Univ
    Id :: Univ
    K :: (a :: *) -> Univ

infixr 7 :*:
infixr 6 :+:

-- Univと対象の型からUnivを実際の関手として適用した型を返す
type family Eval (u :: Univ) a :: *
type instance Eval Id a = a
type instance Eval (K b) a = b
type instance Eval (a :+: b) c = Either (Eval a c) (Eval b c)
type instance Eval (a :*: b) c = (Eval a c, Eval b c)

-- 不動点型
data Mu (u :: Univ) where
    InF :: Eval u (Mu u) -> Mu u

outF :: Mu u -> Eval u (Mu u)
outF (InF a) = a

-- type familyに対して部分適用する為のラッパー
newtype WrapFunctor u a = WrapFunctor { unwrapFunctor :: Eval u a }

instance Functor (WrapFunctor Id) where
    fmap f (WrapFunctor x) = WrapFunctor $ f x

instance Functor (WrapFunctor (K a)) where
    fmap _ (WrapFunctor a) = WrapFunctor $ unsafeCoerce $ a -- どうしても通らなかった
instance (Functor (WrapFunctor u), Functor (WrapFunctor v)) =>
    Functor (WrapFunctor (u :+: v)) where fmap = fmap_sum

instance (Functor (WrapFunctor u), Functor (WrapFunctor v)) =>
    Functor (WrapFunctor (u :*: v)) where fmap = fmap_prod

-- F代数
type Alg u a = Eval u a -> a
-- F余代数
type CoAlg u a = a -> Eval u a

-- aに対してUnivで定義できる型を対応付ける
type family Base a :: Univ

-- 始代数の逆射
class Functor (WrapFunctor (Base a)) => Initial a where
    proj :: a -> Eval (Base a) a

--　終余代数の逆射
class Functor (WrapFunctor (Base a)) => Terminal a where
    embed :: Eval (Base a) a  -> a

-- Nat =~ μ X. 1 + X
type instance Base Natural = K () :+: Id

instance Initial Natural where
    proj 0 = Left ()
    proj n = Right (pred n)

instance Terminal Natural where
    embed (Left _) = 0
    embed (Right n) = succ n

-- [a] =~ μ X. 1 + a * X
type instance Base [a] = K () :+: K a :*: Id

instance Initial [a] where
    proj [] = Left ()
    proj (x:xs) = Right (x,xs)

instance Terminal [a] where
    embed (Left ()) = []
    embed (Right (x,xs)) = x:xs

-- 明示的に型シグニチャを指定しないと型が合わない
cata :: forall a b. (Initial a) => Alg (Base a) b -> a -> b
cata beta = beta' . fmap (cata beta) . proj'
    where proj' :: a -> WrapFunctor (Base a) a
          proj' = WrapFunctor . proj
          beta' = beta . unwrapFunctor

ana :: forall a b. Terminal a => CoAlg (Base a) b -> b -> a
ana delta = embed' . fmap (ana delta) . delta'
    where delta' = WrapFunctor . delta
          embed' :: WrapFunctor (Base a) a -> a
          embed' = embed . unwrapFunctor

main = do
  quickCheck $ \ (xs :: [Int]) ->  cata (either (const []) (uncurry (:))) xs == xs
  quickCheck $ \ (xs :: [Int]) -> ana (\ xs -> if null xs then Left () else Right (head xs, tail xs)) xs == xs




fmap_sum :: forall a b u v. (Functor (WrapFunctor u), Functor (WrapFunctor v)) =>
         (a -> b) -> WrapFunctor (u :+: v) a -> WrapFunctor (u :+: v) b
fmap_sum f (WrapFunctor (Left x)) = WrapFunctor $ Left $ z
    where fmap'' :: WrapFunctor u a -> WrapFunctor u b
          fmap'' = fmap f
          y :: WrapFunctor u a
          y = WrapFunctor x
          z :: Eval u b
          WrapFunctor z = fmap'' y

fmap_sum f (WrapFunctor (Right x)) = WrapFunctor $ Right $ z
    where fmap'' :: WrapFunctor v a -> WrapFunctor v b
          fmap'' = fmap f
          y :: WrapFunctor v a
          y = WrapFunctor x
          z :: Eval v b
          WrapFunctor z = fmap'' y

fmap_prod :: forall a b u v. (Functor (WrapFunctor u), Functor (WrapFunctor v)) =>
         (a -> b) -> WrapFunctor (u :*: v) a -> WrapFunctor (u :*: v) b
fmap_prod f (WrapFunctor (x,y)) = WrapFunctor $ (z,w)
    where fmap' :: WrapFunctor u a -> WrapFunctor u b
          fmap' = fmap f
          fmap'' :: WrapFunctor v a -> WrapFunctor v b
          fmap'' = fmap f
          x' :: WrapFunctor u a
          x' = WrapFunctor x
          y' :: WrapFunctor v a
          y' = WrapFunctor y
          z :: Eval u b
          WrapFunctor z = fmap' x'
          w :: Eval v b
          WrapFunctor w = fmap'' y'