[Haskell-cafe] Categories (cont.)

wren ng thornton wren at freegeek.org
Sun May 12 00:24:01 CEST 2013


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




More information about the Haskell-Cafe mailing list