1

It may sound naive, but is there any programming language, or research thereof, based entirely on category theory?

I mean this as opposed to embedding CT concepts as an additional feature (like for Haskell or scala).

Would it be too abstract or too complex as an approach, or are there any known reasons that makes it impossible or impractical?

I have only a relative understanding of the theory as related to programming, so please give me some explanation if the question doesn't makes sense at all

EDIT

What I mean is to define a language where categories are first class concepts, instead of let's say types.

E.g. haskell is defined in terms of types and functions over those. Does it makes sense to design a language where fundamental entities are categories and arrows?

From there you would, for example, define algebraic operations on numbers as individual "intances" of the proper algebraic category (ring, monoid, group...) instead of starting from standard integer/float operations and defining the corresponding categorical typeclass.

Does it makes sense?

1
  • Actually I found a PhD thesis from Tatsuya Hagino (1987) which explored the idea of Categorical Data Types and a syntax and interpreter for a Categorical Programming Language (CPL). The language is build around definition of adjunct pair of Functors and their morphisms. A concrete implementation in haskell is available.
    – pagoda_5b
    Commented Jan 8, 2014 at 13:38

1 Answer 1

3

Category theory provides a tool. It wouldn't entirely make sense to decide "Oh hey, I'm going to make my programming language form a category" so much as one builds a kernel, and notices that it forms a category, and from there begins applying the free abstractions/theorems that come with it.

A perfect example of this is simply typed lambda calculus. This forms a closed cartesian category where types are objects and functions are arrows. Now, because of this, we can start to apply common abstractions, like endofunctors, adjoints, sub-categories, and similar. In fact, this is exactly what happened in Haskell where the type system is rooted in STLC's.

So I'd say what happens with Haskell is a great example of applying category theory to build abstractions. Many libraries in Haskell, mtl, pipes, lens, void, comonads are all very very useful abstractions that come from noticing that something is a category, and consequently generalizing and applying concepts.

The same thing happens on the research side of things. People have this concept that they notice has a parallel in category theory land, and extrapolate from there. For example, many problems in domain theory are greatly simplified by limits in category theory, and implicit coercions are nicely modeled by category theory.

So I'd say you're thinking of this wrong, don't think of category theory as the thing you build from, it's a bit too abstract for that, it's more that you use parallels between your problem and category theory for free theorems and abstractions in your problem.

5
  • edited the question to try and be more specific about what I had in mind.
    – pagoda_5b
    Commented Nov 6, 2013 at 8:46
  • @pagoda_5b Oh, no. Categories are often very large and difficult to represent, consider Set Commented Nov 6, 2013 at 9:00
  • You mean that there could be no suitable "declarative" definition of categories (like with generators, or through functional properties) that could be used to represent infinite categories or the likes?
    – pagoda_5b
    Commented Nov 6, 2013 at 10:21
  • I'll wait just a little while for other possible answers, otherwise I will consider myself satisfied with yours.
    – pagoda_5b
    Commented Nov 6, 2013 at 10:24
  • @pagoda_5b Well there is.. as a typeclass in Haskell, but it's not limited since it requires that all the objects are the same as Hask. Commented Nov 6, 2013 at 14:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.