hs-to-coq icon indicating copy to clipboard operation
hs-to-coq copied to clipboard

Published 20 hours ago • verified publisher icon antalsz

"Safe" axiomatization

Open sweirich opened this issue 5 years ago • 0 comments

It would be good if hs-to-coq could help distinguish whether added axioms are trivially safe or not. i.e.

Axiom bad : forall {a}, a.

vs

Axiom ok: forall {a}, {Default a} -> a.
Axiom isUpper : Char -> bool.
Axiom newtype : Type.        
Instance Default_newtype : Default newtype.
Axiom str2new : String -> newtype.

The only tricky bit is that we have to approximate whether types are inhabited (i.e. whether default instances are available).

But it would good to be able to see in the edits file which axioms need more scrutiny.

sweirich avatar Jun 25 '19 10:06 sweirich