6 ms·

I believe this is what John Wiegley talked about in this Haskell Cast[1] which, as I understand it, should allow translating Haskell into Coq. I’m just beginni

by runeks 9y ago

I believe this is what John Wiegley talked about in this Haskell Cast[1] which, as I understand it, should allow translating Haskell into Coq. I’m just beginning to understand all of this category stuff but, as far as I can see, a Haskell function of type f :: a -> b should be equivalent to a Coq function of type f :: a -> Either SomeException a to account for the Hask category’s “bottom” value. [1] http://www.haskellcast.com/episode/013-john-wiegley-on-categories-and-compilers http://www.haskellcast.com/episode/013-john-wiegley-on-categ... (skip to “compiling to categories”)

fmap 9y ago
In a constructive metatheory, partiality is both a richer and more subtle concept than just adding option types everywhere. It's possible to model partiality correctly using e.g. quotient inductive types or countable choice (https://link.springer.com/chapter/10.1007/978-3-662-54458-7_31 https://link.springer.com/chapter/10.1007/978-3-662-54458-7_...) or by working with setoids throughout. Neither is a particularly satisfying solution if you want to reason about programs, which typically have richer notions of effects. My own recommendation is to embed programs via weakest preconditions (or strongest postconditions as in Chargueraud's characteristic formulas http://www.chargueraud.org/softs/cfml/ http://www.chargueraud.org/softs/cfml/). This does not allow you to directly evaluate potentially diverging programs, but is far more flexible when reasoning about programs. For example, you can use separation logic to deal with state and concurrency. If you really want to extract to categories for some reason then I would recommend restricting to concrete categories of presheaves or sheaves - I know of no useful application that doesn't already fit into this framework. Using categories requires you to encode everything into a first-order language which is uneccesarily complicated when working with higher-order functions.
dmytrish 9y ago
How can one automatically translate any Haskell containing unbounded recursion into Coq?
- tome 9y ago
  Some sort of partiality monad, I presume.

by runeks 9y ago

fmap 9y ago

In a constructive metatheory, partiality is both a richer and more subtle concept than just adding option types everywhere. It's possible to model partiality correctly using e.g. quotient inductive types or countable choice (https://link.springer.com/chapter/10.1007/978-3-662-54458-7_31 https://link.springer.com/chapter/10.1007/978-3-662-54458-7_...) or by working with setoids throughout. Neither is a particularly satisfying solution if you want to reason about programs, which typically have richer notions of effects. My own recommendation is to embed programs via weakest preconditions (or strongest postconditions as in Chargueraud's characteristic formulas http://www.chargueraud.org/softs/cfml/ http://www.chargueraud.org/softs/cfml/). This does not allow you to directly evaluate potentially diverging programs, but is far more flexible when reasoning about programs. For example, you can use separation logic to deal with state and concurrency. If you really want to extract to categories for some reason then I would recommend restricting to concrete categories of presheaves or sheaves - I know of no useful application that doesn't already fit into this framework. Using categories requires you to encode everything into a first-order language which is uneccesarily complicated when working with higher-order functions.

dmytrish 9y ago

How can one automatically translate any Haskell containing unbounded recursion into Coq?

tome 9y ago
Some sort of partiality monad, I presume.