antalsz/hs-to-coq

Parameterized `order` edits

Opened this issue · 4 comments

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

  • For all types T, put Semigroup before mappend (i.e., Semigroup__T before Monoid__T_mappend)
  • For all types T, put Eq_ before Ord (i.e., Eq___T before Ord__T)

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

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.

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.

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"

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