{-# OPTIONS --without-K #-}
module Dialogue.Core where
open import Basis
data π (X Y Z : Set) : Set where
return
: Z
β π X Y Z
ask
: X
β (Y β π X Y Z)
β π X Y Z
data π
(Y Z : Set) : Set where
spit
: Z
β π
Y Z
bite
: (Y β π
Y Z)
β π
Y Z
private
variable {X Y} : Set
π-bind : {A B : Set} β (A β π X Y B) β π X Y A β π X Y B
π-bind f (return x) = f x
π-bind f (ask i m) = ask i Ξ» x β π-bind f (m x)
π-bind/Ο : {A : Set} (m : π X Y A) β π-bind return m β‘ m
π-bind/Ο (return x) = refl
π-bind/Ο (ask i m) =
β‘.cong
(ask i)
(funext Ξ» x β
π-bind/Ο (m x))
π-bind/Ξ± : {A B C : Set} {f : A β π X Y B} {g : B β π X Y C} (m : π X Y A) β π-bind g (π-bind f m) β‘ π-bind (π-bind g β f) m
π-bind/Ξ± (return x) = refl
π-bind/Ξ± (ask i m) =
β‘.cong
(ask i)
(funext Ξ» x β
π-bind/Ξ± (m x))
instance
π-monad : Monad (π X Y)
Monad.ret π-monad = return
Monad.bind π-monad = π-bind
Monad.law/Ξ» π-monad = refl
Monad.law/Ο π-monad = π-bind/Ο
Monad.law/Ξ± π-monad = π-bind/Ξ±
private
variable Z W : Set
π[_β_] : π X Y Z β (X β Y) β Z
π[ return x β Ξ± ] = x
π[ ask i m β Ξ± ] =
π[ m (Ξ± i) β Ξ± ]
π
[_β_] : π
Y Z β (β β Y) β Z
π
[ spit x β Ξ± ] = x
π
[ bite m β Ξ± ] = π
[ m (Ξ± 0) β (Ξ± β suc) ]
generic : π X Y X β π X Y Y
generic m = do
i β m
ask i ret
module β’ where
β-extensional
: (m : π X Y Z)
β {Ξ± Ξ² : X β Y}
β (β i β Ξ± i β‘ Ξ² i)
β π[ m β Ξ± ] β‘ π[ m β Ξ² ]
β-extensional (return _) _ =
refl
β-extensional (ask i m) {Ξ±} {Ξ²} h =
β‘.seq
(β-extensional (m (Ξ± i)) h)
(β‘.cong
(Ξ» β β π[ m β β Ξ² ])
(h i))
β-natural
: (f : Z β W)
β (m : π X Y Z)
β (Ξ± : X β Y)
β f π[ m β Ξ± ] β‘ π[ map f m β Ξ± ]
β-natural f (return x) Ξ± =
refl
β-natural f (ask _ m) Ξ± =
β-natural f (m _) Ξ±
β-commutes-with-bind
: {m : Z β π X Y W}
β (n : π X Y Z)
β (Ξ± : X β Y)
β π[ m π[ n β Ξ± ] β Ξ± ] β‘ π[ (n >>= m) β Ξ± ]
β-commutes-with-bind (return _) _ =
refl
β-commutes-with-bind (ask _ m) Ξ± =
β-commutes-with-bind (m _) Ξ±
generic-diagram
: (Ξ± : X β Y)
β (m : π X Y X)
β Ξ± π[ m β Ξ± ] β‘ π[ generic m β Ξ± ]
generic-diagram Ξ± (return x) =
refl
generic-diagram Ξ± (ask _ m) =
generic-diagram Ξ± (m _)