Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- data Ty
- data Tm
- data J a where
- type Theory j = (Monad m, Alternative m, MonadOpen (j a) a m) => Op (j a) m a
- unitThy :: Theory J
- prodThy :: Theory J
- combinedThy :: Theory J
- judge :: (Monad m, Alternative m) => J b -> m b
- traceThy :: (Monad m, Alternative m, MonadOpen (j a) a m, MonadWriter [Pack J] m) => Op (J a) m a
- data Pack φ = forall a . Pack (φ a)
- tracedJudge :: J b -> (Maybe b, [Pack J])

# Syntax

# Judgement Forms

Next, the forms of judgements are inductively defined. We index the
`J`

type by its synthesis.

# Theories

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`

`>>>`

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

`>>>`

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

`>>>`

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

`>>>`

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

## 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!

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

`>>>`

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

`>>>`

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