Also derive alpha-respecting Ord instance

[GoogleCodeExporter]

We currently generically derive aeq. It would be nice to also derive an 
acompare, so that terms can be used as keys for Maps etc.

Original issue reported on code.google.com by [email protected] on 26 Oct 2010 at 10:45

[GoogleCodeExporter]

That is a great idea, but it sounds tricky to me for the nominal version. 

For example, how should we order \x.\y. x y  and  \x.\y. y x ? Which one is 
less?
For consistency sake, we should probably choose the same order as in the 
locally nameless version, but I don't know how to implement that in the nominal 
case.

For the locally nameless version, the tricky part is that when we do 
instance (Ord a, Ord b) => Ord (Bind a b) where
   compare (B a1 b1) (B a2 B2) = 
        case compare_ignore_names a1 a2 of 

Original comment by stephanie.weirich on 27 Oct 2010 at 1:41

[GoogleCodeExporter]

That is a great idea, but it sounds tricky to me for the nominal version. 

For example, how should we order \x.\y. x y  and  \x.\y. y x ? Which one is 
less?
For consistency sake, we should probably choose the same order as in the 
locally nameless version, but I don't know how to implement that in the nominal 
case.

For the locally nameless version, the tricky part is that when we compare the 
patterns in bind. We need to ignore the variable names (except those that 
appear 
in an Annot.) Therefore, we need a version of compare that is parameterized by 
an AlphaCtx so we know where we are.

Original comment by stephanie.weirich on 27 Oct 2010 at 1:43