human-facing documentation?

[AntC2]

Hi Edward, Ryan,

I'm looking at Edward's comments on this libraries thread, and SPJ's follow-up in January linking to the QuantifiedConstraints work/Trac #2893 just Phab'd.

I have a possible use case in mind for implication constraints, so I came here to look at the package. But I'm finding no helpful documentation about it. I've tried reading the commets in the source. Do I need to understand Category Theory and what is a Heyting Algebra to use this? Then I won't bother.

To give a hint of my use case: I'm wondering if constraint implication can help express the logic in an anonymous/extensible records system. If I have a base constraint Has r l a expressing record r has label l at type a, can I express the constraint on record append :: r1 -> r2 -> r3 such that

(forall l1 a1 . Has r1 l1 a1 => Has r3 l1 a1, forall l2 a2 . Has r2 l2 a2 => Has r3 l2 a2) => ...

Ideally record append should go beyond that to say that if Has r3 l a then either Has r1 l a or Has r2 l a. Then perhaps I need to understand Edward's comment

3.) Constraint also admits a sum type, (\/) but it acts more like a least upper bound than an either.