Re:A blog engine written and proven in Coq
by pseudonom- on Thursday February 12, 2015 @02:02PM
(#9040628)
My 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).
Re:A blog engine written and proven in Coq
by vilhelm_s on Thursday February 12, 2015 @04:41PM
(#9041577)
Yes, 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.)
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.