3 ms·
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 al
by pseudonom- 12y ago
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).
- 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.)