I was trying to extract Functors for coq available from coq-ext-lib to haskell.

So I tried:

```
Require Import ExtLib.Structures.Functor.
Require Import ExtLib.Data.Option.
Require Extraction.
Extraction Language Haskell.
Require Import ExtrHaskellBasic.
Require Import ExtrHaskellNatInt.
Definition foo (n:option nat): option nat := fmap S n.
Compute foo (Some 2).
Recursive Extraction foo.
```

I was kind of hoping to get this:

```
foo :: Maybe Int -> Maybe Int
foo n = fmap succ n
```

But a separate `fmap`

function got generated as well (along with some other things):

```
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Main where
import qualified Prelude
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#if __GLASGOW_HASKELL__ >= 900
import qualified GHC.Exts
#endif
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
#if __GLASGOW_HASKELL__ >= 900
unsafeCoerce = GHC.Exts.unsafeCoerce#
#else
unsafeCoerce = GHC.Base.unsafeCoerce#
#endif
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif
__ :: any
__ = Prelude.error "Logical or arity value used"
type Functor f =
() -> () -> (Any -> Any) -> f -> f
-- singleton inductive, whose constructor was Build_Functor
fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
fmap functor x x0 =
unsafeCoerce functor __ __ x x0
functor_option :: Functor (Prelude.Maybe Any)
functor_option _ _ f x =
case x of {
Prelude.Just x0 -> Prelude.Just (f x0);
Prelude.Nothing -> Prelude.Nothing}
foo :: (Prelude.Maybe Prelude.Int) -> Prelude.Maybe Prelude.Int
foo n =
fmap (unsafeCoerce functor_option) (\x -> Prelude.succ x) n
```

How can this be remedied?

Can we make the extracted code simply use whatever is available in haskell instead of making a new `fmap`

and all?

Adding

```
Extract Inductive Functor => "Functor" [ "fmap" ].
```

to this didn't seem to make *much* difference:

```
__ :: any
__ = Prelude.error "Logical or arity value used"
fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
fmap functor x x0 =
case functor of {
fmap fmap0 -> unsafeCoerce fmap0 __ __ x x0}
functor_option :: Functor (Prelude.Maybe Any)
functor_option =
fmap (\_ _ f x ->
case x of {
Prelude.Just x0 -> Prelude.Just (f x0);
Prelude.Nothing -> Prelude.Nothing})
foo :: (Prelude.Maybe Prelude.Int) -> Prelude.Maybe Prelude.Int
foo n =
fmap (unsafeCoerce functor_option) (\x -> Prelude.succ x) n
```

Last updated: Sep 23 2023 at 14:01 UTC