[Haskell-cafe] Category theory as a design tool

[wren ng thornton]

On 6/23/11 1:39 AM, Arnaud Bailly wrote:
> Of course, we can always say that each
> system is a language of its own (rather than *has* a language...) which is
> what Eric Evans coined with its "Ubiquitous language" term. But I find it
> difficult to connect that particular dots.

That's certainly my take on things (which I argued for at a workshop last
week). Then again, I'm a linguist and type theorist, so viewing systems as
languages[1] comes naturally. Do you have a link to Evans' coinage and
argument?


[1] Or rather, APIs as languages, their implementations as (defining
their) semantics, and their execution as parsing.


>> As an example of this approach, see my comments in the thread about
>> anonymous sum types. For something to be a product means that a particular
>> diagram commutes: namely, a product is the limit of the two point category
>> (and coproducts are the colimit). One of the many things this tells us is
>> that if we posit that A*A ~ A in a category that "has products", we must
>> infer that the category is a meet-(pre)semilattice[1].
>
> I certainly won't argue with you on this given my limited knowledge of what
> a meet-(pre)semilattice could be :-)

A preorder is just a generalization of a partial order, which we can gloss
over here. A meet-semilattice is just a partial order with a "meet"
operation, i.e. every pair of elements has a greatest lower bound. (A
join-semilattice is the dual, with LUB instead of GLB.)

> But then, if I happen to understand
> what it is, how could that help me design and code "better" systems? I have
> the intuition it could help me but again I do not (yet) see how.

Well, for this example, there was the proposed idea to have anonymous
union types with the injectors given by the types of the components (e.g.,
for the type A|B we'd have data constructors A :: A -> A|B and B :: B ->
A|B). But this raises the issue of how to deal with A|A. Someone suggested
that we could just say that A|A is the same as A. However, doing so means
that the (|) type operator cannot be a coproduct. That's not a game-killer
per se ---afterall, Either isn't a corpoduct--- but it does suggest that
something fishy is going on. In this case, the better system is the one we
already have, where we use disjoint unions (Either) instead of
non-disjoint unions (|).

To put a different spin on it, in the dual case we can show that Haskell's
(,) is not a categorical product. There's a good deal of historical debate
about why it works the way it does, but if we're looking to make a better
system then the fact that tuples are not well-behaved suggests a place for
improvement. The current (,) is a compromise between two different notions
of product in domain theory. On the one hand we have domain products
(which do not produce domains) and on the other hand we have smash
products (which can "lose" information). I've had in mind for a while to
make a Haskell-like language with a total functional core. In a total
language (even a lazy one), we don't have bottom so we don't need domain
theory to reason about the language. So in a language which is only
partially total, it's reasonable to have two different kinds of
products--- which means we can get away from Haskell's compromise, but do
so in a way that's harmonious with the rest of the language. Would this
new system be "better"? I dunno. It would behave in a more lawful manner,
so it should be easier to reason about; but then we're making programmers
keep that reasoning in mind, and maybe that's too much work. A decent
system has to be both correct but also usable, and human factors are messy
and hard to predict.

-- 
Live well,
~wren