[Haskell-cafe] Category theory as a design tool

[Arnaud Bailly]

On Wed, Jun 22, 2011 at 11:46 PM, wren ng thornton <wren at freegeek.org>wrote:

> One of the big benefits I see to using category theory for dealing with
> programming languages comes from using CT as a generalized logic for
> equational reasoning. In particular, making use of the ideas of (co)limits
> and adjunctions in order to prove that something must behave in a
> particular way. This requires a bit of work to contort your thinking into
> the patterns of CT, but it means that once you can prove that something is
> a foo, then all the theorems about foos will apply.
>
>
Yes, I can understand that and this is exactly what I am looking for. Except
that I am looking for it not to deal with programming languages but with
systems (and the way we design). 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.


> 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 :-) 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.

Thanks a lot for your answer
Arnaud
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110623/8609fd65/attachment.htm>