Extraction to Haskell

[HuStmpHrrr]

I am using this library and attempting to extract it to Haskell. In Haskell, there are default library and syntactical supports for monad, so it would be nice if the extracted code can use this facilities.

Currently, the resulting extracted code looks something like this:

data Monad m =
   Build_Monad (() -> Any -> m) (() -> () -> m -> (Any -> m) -> m)

ret :: (Monad a1) -> a2 -> a1
ret monad x =
  case monad of {
   Build_Monad ret0 _ -> unsafeCoerce ret0 __ x}

bind :: (Monad a1) -> a1 -> (a2 -> a1) -> a1
bind monad x x0 =
  case monad of {
   Build_Monad _ bind0 -> unsafeCoerce bind0 __ __ x x0}

data PMonad m =
   Build_PMonad (() -> Any -> Any -> m) (() -> () -> Any -> m -> (Any -> m)
                                        -> m)

type MonP m x = Any

pbind :: (PMonad a1) -> (MonP a1 a3) -> a1 -> (a2 -> a1) -> a1
pbind pMonad pu x x0 =
  case pMonad of {
   Build_PMonad _ pbind0 -> unsafeCoerce pbind0 __ __ pu x x0}

pMonad_Monad :: (Monad a1) -> PMonad a1
pMonad_Monad m =
  Build_PMonad (\_ -> unsafeCoerce (\_ x -> ret m x)) (\_ _ ->
    unsafeCoerce (\_ c f -> bind m c f))

I am wondering if some modules can be added as a default extraction configuration to collide monads on both sides?

[gmalecha]

This would be very useful. A basic problem (but not one that is insurmountable) is that converting Coq classes into Haskell classes isn't really a local transformation because Coq classes are values while Haskell classes are not.

At the moment, I don't have the cycles to address this, but I'd welcome pull requests.