ROSCOQ.shim.Haskell.RoshaskNodeMonad
Require Import String.
Require ExtrHaskellBasic.
Extraction Language Haskell.
Axiom Node : Type → Type.
Extract Constant Node "a" ⇒ "Ros.Node.Node a".
Require ExtrHaskellBasic.
Extraction Language Haskell.
Axiom Node : Type → Type.
Extract Constant Node "a" ⇒ "Ros.Node.Node a".
I doubt that Coq typeclasses
get extracted to Haskell typeclasses. It makes sense to do the resolution in Coq.
So, we have extraction directives specifically for the return and bind functions of Node.
Axiom nreturn : ∀ {a:Type}, a → Node a.
Extract Constant nreturn ⇒ "Ros.ROSCoqUtil.nreturn".
Axiom nbind : ∀ {a b:Type}, Node a → (a → Node b) → Node b.
Extract Constant nbind ⇒ "Ros.ROSCoqUtil.nbind".
Require Import MathClasses.interfaces.monads.
Instance ReturnInstanceNodeHaskell : MonadReturn Node := (fun A ⇒ @nreturn A).
Instance BindInstanceNodeHaskell : MonadBind Node := (fun A B f x⇒ @nbind A B x f).
Axiom AssumeMonadNodeHaskell: ∀ nodeEq, @Monad Node nodeEq _ _.
Instance MonadInstanceNodeHaskell : ∀ nodeEq, @Monad Node nodeEq _ _ :=
AssumeMonadNodeHaskell.