Stream: Coq users

Topic: Multi-parameter type haskell extraction

view this post on Zulip Julin Shaji (Jan 04 2024 at 05:21):

Hi.

I have a vector type in haskell (made with some extensions) like:

data Vector :: Nat → Type → Type
  Nil :: forall a. Vector Zero a
 Cons :: forall a n. a -> Vector n a -> Vector (Succ n) a

with values like:

v1 :: Vector (Succ Zero) Bool
v1 = Cons True Nil

Is there a way to map Coq's Vector.t type to this type while extracting to haskell?
So that v1 can be mapped to [true]%vector?

By default, extracting Vector.t changes the structure a bit:

Example vec := [true].
Recursive Extraction vec.

(*
data T a =
   Nil
 | Cons a Int (T a)

vec :: T Bool
vec =
  Cons True 0 Nil
*)

Is it possible to extract as multi-parameter type itself?
Does anyone know?

Last updated: Oct 13 2024 at 01:02 UTC