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