antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Parameterized `order` edits #111

Open antalsz opened 6 years ago

antalsz commented 6 years ago

It might be nice to impose "default order" constraints, such as

(For the Eq_ / Ord one, we might be able to autogenerate this from the superclass constraints).

nomeata commented 6 years ago

The problem is that it is not always correct. You can have

instance Semigroup a where (<>) = mappend -- this is actually the default definition
instance Monoid a where mappend = …

So if you add a default order, you have to provide a clever way of allowing the user to disable them. (Just adding the conflicting orders to the set of oderings will cause cycles.) Doable, but unfortunately pretty complicate, also to explain to users.

antalsz commented 6 years ago

Damn, that's true >_<.

That opens up the option for more complex heuristics (e.g., "if the definition of mappend is <>, do this order; if the other way around, do that order"), but those are more of a pain.

The superclass constraint issue is always a necessary order, at least.

antalsz commented 6 years ago

Or a heuristic like "if a method C__T_method of type class C for the instance T is defined to be η-equivalent to a method of type class C', then add a dependency order C'__T C__T_method"

antalsz commented 6 years ago

(I don't know about implementation, I'm just thinking about possible solutions to the issue – using this as a repository of ideas)