Stream: Coq users

Topic: Extracting coq-ext-lib fmap to haskell

view this post on Zulip Julin S (Aug 25 2022 at 09:36):

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?

view this post on Zulip Julin S (Aug 25 2022 at 09:44):

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: Apr 20 2024 at 00:02 UTC