search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.85k stars 649 forks source link

Haskell extraction should use existential quantification for type parameters in constructors #5652

Open coqbot opened 7 years ago

coqbot commented 7 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5652 From: @tchajed Reported version: 8.8+alpha CC: coq-bugs-redist@lists.gforge.inria.fr

coqbot commented 7 years ago

Comment author: @tchajed

Haskell has a feature called existential quantification to put an existential type inside a data constructor. Coq could use this to give constructors more polymorphic types in Haskell extraction (below is a concrete example, including the desired extracted code). It looks like OCaml could almost do this, except that it doesn't support impredicative polymorphism inside constructors, though you can put explicit foralls in records (eg, [type t = { f: 'a. 'a list -> int }] is a record with a polymorphic function). See https://stackoverflow.com/questions/23323032/in-ocaml-what-type-definition-is-this-a-unit-a for some details, and https://wiki.haskell.org/Impredicative_types for a Haskell explanation.

Require Extraction.

Inductive IdMonad T := | Ret (v:T) | Bind T' (a: IdMonad T') (b: T' -> IdMonad T).

Extraction Language Ocaml.

Extraction IdMonad.

( output: data IdMonad t = Ret t | Bind (IdMonad Any) (Any -> IdMonad t) )

( would like: {-# LANGUAGE ExistentialQuantification #-} data IdMonad t = Ret t | forall t'. Bind (IdMonad t') (t' -> IdMonad t) )

( non-constructor definitions already work: ) Definition bind := Bind. Extraction bind.

( output: bind :: (IdMonad a2) -> (a2 -> IdMonad a1) -> IdMonad a1 bind a b = Bind (unsafeCoerce a) (unsafeCoerce b) )