Program Monad

axiom ext : ∀ A B (f g : Π x : A, B x), (∀ x, f x = g x) -> f = g

inductive Prompt (inst) : Type -> Type :=
| Ret {} : Π r,
    Prompt inst r
| Bind : Π {a r},
    (a -> Prompt inst r) -> (Prompt inst a) -> (Prompt inst r)
| Tag : Π {r}, inst r -> Prompt p r

-- reverse concat, allso known as "then"
infixl `∙`:50 := fun f g x := g (f x)

structure functor (F : (Type -> Type)) : Type :=
    (fmap : Π A B, (f : A -> B) -> F A -> F B)
    (id_rule : ∀ A, fmap id = (id : F A -> F A))
    (comp_rule : ∀ f g, fmap (f ∙ g) = (fmap f) ∙ (fmap g))

end

abbreviation Prompt := Type -> Type -> Type

definition type_has_zero : has_zero Type₁ :=
    {| has_zero Type₁, zero := empty |}

definition type_has_one [instance] : has_one Type₁ :=
    {| has_one Type₁, one := unit |}

definition type_has_add [instance] : has_add Type :=
    {| has_add Type, add := sum |}

inductive StateP (S : Type₁) : Type₁ -> Type₁ -> Type₁ :=
| Get : StateP S S
| Set : StateP S (S -> 1)

abbreviation StateM S := FreeM (StateP S)

definition