Parameterized `order` edits

[lastland]

Issue by antalsz Wednesday Oct 17, 2018 at 07:51 GMT Originally opened as https://github.com/antalsz/hs-to-coq/issues/111

---

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).

[lastland]

Comment by nomeata Wednesday Oct 17, 2018 at 08:38 GMT

---

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.

[lastland]

Comment by antalsz Wednesday Oct 17, 2018 at 18:05 GMT

---

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.

[lastland]

Comment by antalsz Wednesday Oct 17, 2018 at 21:26 GMT

---

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"

[lastland]

Comment by antalsz Wednesday Oct 17, 2018 at 21:27 GMT

---

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