On 5/8/13 12:14 PM, Conal Elliott wrote:

Hi Wren,

Have you taken this "constrained categories" experiment further, particularly for adding products? As I mentioned in a haskell-cafe note yesterday, I tried and got a frightening proliferation of constraints when defining method defaults and utility functions (e.g., left- or right-associating).

I haven't investigated further since my previous emails on the idea. When working with them, though, I did notice that things work out a lot better with separate unary constraints on domains and codomains, as opposed to having a binary constraint that relates domains to codomains. (The latter is, of course, strictly more powerful; which may be the problem.) As another part of that project, however, I've been working on type-level arithmetic, and that also leads to a frightening proliferation of constraints. The problem is that even though we can implement the definitions of addition, comparison, etc, there's no good way to teach the constraint solver facts like: m < S m m <= m+n -- For natural numbers, not integers. m <= n -> exists o. n == m+o m <= n -> n <= o -> m <= o etc The introduction of these facts would introduce nondeterminism into the resolution of constraints--- since the solver would need to decide between using the inductive definitions vs these auxilliary facts. My impression is that the difficulties here are the same for both cases... -- Live well, ~wren