monad-open-0.1.0.0: Open recursion for when you need it

Safe HaskellNone
LanguageHaskell2010

Control.Monad.Trans.Open.Example

Contents

Description

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

Synopsis

Syntax

data Ty Source

The syntax of terms in our theory.

Constructors

Unit 
Prod Ty Ty 

Instances

data Tm Source

The syntax of terms in our theory.

Constructors

Ax 
Pair Tm Tm 

Instances

Judgement Forms

data J a where Source

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 Source

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 Source

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

prodThy :: Theory J Source

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

combinedThy :: Theory J Source

The horizontal composition of the two above theories.

combinedThy = unitThy <> prodThy

Result

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

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 Source

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

data Pack φ Source

Constructors

forall a . Pack (φ a) 

Instances

Show (Pack J) 

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

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)])