Stream: Coq users

Topic: Dependent type haskell extraction


view this post on Zulip Julin Shaji (Jan 04 2024 at 06:30):


There will be a change when extracting Fin.t type as well.

I guess extraction will change the structure whenever there's a dependent type.

Example f1: Fin.t 2 := FS F1.
Recursive Extraction f1.
(*
data T =
   F1 Int
 | FS Int T

f1 :: T
f1 =
  FS (succ 0) (F1 0)
*)

view this post on Zulip Matthieu Sozeau (Feb 08 2024 at 11:49):

Indeed extraction erases the indexing which is quite different for Haskell’s GADTs and Coq’s indexed types. The best you could do I guess is to write wrappers between the extracted type and Haskell’s vectors

view this post on Zulip Julin Shaji (Feb 10 2024 at 05:06):

Makes sense. Thanks!


Last updated: Jun 13 2024 at 19:02 UTC