Control.Monad.Trans.Open.Example

This is a demonstration of using open recursion to implement the judgements of a small theory modularly.

Syntax

data Ty

The syntax of terms in our theory.

Constructors

Unit

Prod Ty Ty

Instances

Eq Ty

Show Ty

data Tm

The syntax of terms in our theory.

Constructors

Ax

Pair Tm Tm

Instances

Eq Tm

Show Tm

Judgement Forms

data J a where

Next, the forms of judgements are inductively defined. We index the J type by its synthesis.

DisplayTy

To know DisplayTy α is to know the textual notation for the type α.

DisplayTm

To know DisplayTm m is to know the textual notation for the term m.

Check

To know Check α m is to know that m is a canonical verification of α.

Constructors

DisplayTy :: Ty -> J String

DisplayTm :: Tm -> J String

Check :: Ty -> Tm -> J Bool

Instances

Show (Pack J)

Show (J a)

Theories

type Theory j = (Monad m, Alternative m, MonadOpen (j a) a m) => Op (j a) m a

A Theory j is an open, partial implementation of the judgements defined by the judgement signature j. Theories may be composed, since Monoid (Theory j) holds.

unitThy :: Theory J

A Theory implementing the judgements as they pertain to the Unit type former.

prodThy :: Theory J

A Theory implementing the judgments as they pertain to the Prod type former.

combinedThy :: Theory J

The horizontal composition of the two above theories.

combinedThy = unitThy <> prodThy

Result

judge :: (Monad m, Alternative m) => J b -> m b

Judgements may be tested through the result of closing the theory.

judge = close combinedThy

>>> judge $ DisplayTy $ Prod Unit (Prod Unit Unit)
"(unit * (unit * unit))"

>>> judge $ DisplayTm $ Pair Ax (Pair Ax Ax)
"<ax, <ax, ax>>"

>>> judge $ Check (Prod Unit Unit) Ax
False

>>> judge $ Check (Prod Unit (Prod Unit Unit)) (Pair Ax (Pair Ax Ax))
True

Injecting Effects

traceThy :: (Monad m, Alternative m, MonadOpen (j a) a m, MonadWriter [Pack J] m) => Op (J a) m a

We can inject a log of all assertions into the theory!

data Pack φ

Constructors

forall a . Pack (φ a)

Instances

Show (Pack J)

tracedJudge :: J b -> (Maybe b, [Pack J])

A traced judging routine is constructed by precomposing traceThy onto the main theory.

tracedJudge j = runIdentity . runWriterT . runMaybeT $ (close $ traceThy <> combinedThy) j

>>> tracedJudge $ Check (Prod Unit Unit) (Pair Ax Ax)
(Just True,[Check (Prod Unit Unit) (Pair Ax Ax),Check Unit Ax,Check Unit Ax])

>>> tracedJudge $ Check (Prod Unit Unit) (Pair Ax (Pair Ax Ax))
(Just False,[Check (Prod Unit Unit) (Pair Ax (Pair Ax Ax)),Check Unit Ax,Check Unit (Pair Ax Ax)])