Indexed free monadでCoqのタクティクスのようなものを実装

IndexedTools.hs

{-# LANGUAGE GADTs, TemplateHaskell #-}
module IndexedTools where

import Control.Monad.Indexed
import Language.Haskell.Meta
import Language.Haskell.TH
import Language.Haskell.TH.Quote

data IxFree f i j x where
    Pure :: a -> IxFree f i i a
    Free :: f i j (IxFree f j k a) -> IxFree f i k a

instance IxFunctor f => IxFunctor (IxFree f) where
    imap f (Pure a) = Pure (f a)
    imap f (Free w) = Free (imap (imap f) w)

instance IxFunctor f => IxPointed (IxFree f) where
    ireturn = Pure

instance IxFunctor f => IxApplicative (IxFree f) where
    iap (Pure a) (Pure b) = Pure (a b)
    iap (Pure a) (Free fb) = Free (imap a `imap` fb)
    iap (Free fa) mb = Free $ imap (`iap` mb) fa

instance IxFunctor f => IxMonad (IxFree f) where
    ibind k (Pure a) = k a
    ibind k (Free fm) = Free $ imap (ibind k) fm

ido :: QuasiQuoter
ido = QuasiQuoter { quoteExp = \str -> case parseExp str of
        Right (DoE ss) -> return (go ss)
        , quotePat = undefined
        , quoteType = undefined
        , quoteDec = undefined
        } where
    go [NoBindS e] = e
    go (BindS p e : ss) = VarE 'ibind `AppE` LamE [p] (go ss) `AppE` e
    go (NoBindS e : ss) = VarE 'ibind `AppE` LamE [WildP] (go ss) `AppE` e
    go (LetS ds : ss) = LetE ds (go ss)

tactic.hs

{-# LANGUAGE TemplateHaskell, GADTs, ImplicitParams, ScopedTypeVariables #-}
import Control.Monad.Indexed
import Control.Applicative
import Control.Monad.State
import Language.Haskell.TH
import IndexedTools

import Data.Void

data Proof i j x where
    Intro :: (p -> a) -> Proof (p -> q) q a
    Apply :: (p -> q) -> a -> Proof q p a

instance IxFunctor Proof where
    imap f (Intro g) = Intro (f . g)
    imap f (Apply e a) = Apply e (f a)

intro :: IxFree Proof (a -> b) b a
intro = Free $ Intro ireturn

apply :: (a -> b) -> IxFree Proof b a ()
apply p = Free $ Apply p (ireturn ())

exact :: a -> IxFree Proof a () ()
exact p = Free $ Apply (const p) (ireturn ())

-- 証明の例

ex0 :: IxFree Proof ((a -> b) -> (b -> c) -> a -> c) () ()
ex0 = [ido|do
    ab <- intro
    bc <- intro
    a <- intro 
    apply bc
    apply ab
    exact a
    |]

ex1 :: IxFree Proof (Either a b -> (a -> c) -> (b -> c) -> c) () ()
ex1 = [ido|do
    e <- intro
    ac <- intro
    bc <- intro
    exact $ either ac bc e
    |]

ex2 :: IxFree Proof (((a, b) -> c) -> b -> a -> c) () ()
ex2 = [ido|do
    f <- intro
    b <- intro
    a <- intro
    exact $ f (a, b)
    |]