3 ms·
It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and
by adultSwim 12y ago
It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions.
So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list and returns a list. However the computation being done is still the same.
The target language doesn't even need types. I don't know if it's still maintained but there used to be an extraction back-end to Scheme (also one for Haskell).
Being a functional language makes things much easier. Need to have something to map algebraic data types, functions, and function application.
- pseudonom- 12y agoMy understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).
- vilhelm_s 12y agoYes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)