40
$\begingroup$

Since some computer scientists use category theory, I was wondering if there are any programming languages that use it extensively.

Improve this question
$\endgroup$
2
  • 6
    $\begingroup$ Strangely enough, I'm actually doing work on this subject at the moment, but for most likely a VERY different reason than why you'd have interest. I'm looking into the subject for educational reasons, trying to show that a mathematics background can be an asset in learning programming, and that computer programming can be an inroad to learning mathematics. $\endgroup$
    – Michael Hoffman
    Commented Nov 2, 2009 at 3:00
  • $\begingroup$ You might like my explanation of matrix math with Python: stackoverflow.com/questions/1016284/… $\endgroup$
    – Ilya Nikokoshev
    Commented Nov 3, 2009 at 19:59

16 Answers 16

Reset to default
15
$\begingroup$

Yes. I think that Haskell is the canonical example. Go here for more.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ Haskell is a canonical example of a functional programming language, I have a reference to a "categorical programming language" below, Hagino. $\endgroup$
    – Michael Hoffman
    Commented Nov 2, 2009 at 2:07
  • 5
    $\begingroup$ Relevant: "Hask is not a category" by Andrej Bauer math.andrej.com/2016/08/06/hask-is-not-a-category $\endgroup$
    – j.c.
    Commented Mar 28, 2019 at 19:44
15
$\begingroup$

There's Charity.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ IMHO Charity (and Squiggol) have a slightly stronger claim to being "a categorical programming language" than Haskell. $\endgroup$
    – Adam
    Commented Jan 18, 2010 at 23:35
  • 1
    $\begingroup$ Seen on the Charity website: "All Charity computations terminate (up to user input).". Is Charity Turing-complete? $\endgroup$
    – Samuele Giraudo
    Commented Mar 6, 2013 at 20:55
  • 2
    $\begingroup$ @SamueleGiraudo Technically it is not, however you could always supply non-termination primitives using similar mechanisms as for I/o (e.g. a non-termination monad). So the language alone may not be turing complete but the overall system might be. $\endgroup$
    – Dobes Vandermeer
    Commented May 4, 2015 at 3:29
14
$\begingroup$

Haskell is a purely functional language. However side-effects are (almost by definition) difficult to incorporate into a functional language. This is an important problem since I/O is a very important side-effect for most computer programs. Haskell's method of incorporating side-effects is to use monads.

One of the simplest ways to get a monad is from a pair of adjoint functors.

For more on monads see:

(1) Embûches tissues blog: Monads in Mathematics 1: examples

(2) A series of lectures on youtube by TheCatsters:

Pairs of adjoint functors are fairly common and I've found they provide a useful way for seeing part of the "big-picture" in many different branches of mathematics.

Here is one of several introductions to pairs of adjoint functors from the Concrete Nonsense blog.

Improve this answer
$\endgroup$
13
$\begingroup$

ML is used in

Computational Category Theory

Apparently there exists at least one "categorical programming language", namely Hagino

A Categorical Programming Language

(Hagino's Thesis)

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Oh, and I'm reading both of these currently, so I can say that they are at least initially quite readable, even at my level (advanced undergraduate) $\endgroup$
    – Michael Hoffman
    Commented Nov 2, 2009 at 3:09
  • 1
    $\begingroup$ That second link is broken, at present. $\endgroup$
    – David Roberts ♦
    Commented Jun 18, 2015 at 11:29
11
$\begingroup$

I'd say every statically typed functional language is such. Why? There's a well-known relation between propositions and types, or more precisely between certain theories of logic and certain type theories going by the name of Curry--Howard correspondence. This relation has a less well-known cousin known as Curry--Howard--Lambek correspondence that extends it to categories. Thus, because every reasonable statically typed functional language is based on type theory, it has direct connection to category theory as well. You simply cannot escape it, try as you might. Bob Harper likes to call this The Holy Trinity -- categories, languages and logic.

The list of such languages follows: Haskell, ML, OCaml, Idris, Coq, Agda, etc.

Of course, you have to take all of this with a grain of salt. Safe for Coq and Agda -- both of which are foremost theorem provers -- these languages contain many industry-driven quirks that make them less susceptible to the formal reasoning mentioned in the first paragraph.

In a bit different direction, because type theory is so expressive (for example, it can replace set theory as foundations of mathematics), it's fairly straightforward to express many algebraic structures in it. All of the above languages use this feature profoundly, with e.g. monads in Haskell playing a very prominent role.

Improve this answer
$\endgroup$
11
$\begingroup$

All of the answers so far are based on Cartesian closed categories. There are a few languages based on Cartesian categories, which reject use of higher-order functions in the base language:

  1. The key example are Joseph Goguen's OBJ languages for programming with algebras, based on order-sorted Cartesian categories. Goguen's rejection of higher-order functions is explained in his Higher-order functions considered unnecessary for higher-order programming.
  2. The programming language Maude, based on rewriting logic, is probably the fittest successor of OBJ. Cf. Goguen's OBJ Family page, which summarises the programming languages in this family.
  3. The mathematical payoff to rejecting the "closed" part of Cartesian closed categories is that this opens the possibility of easier modelling of colimit constructions; I'd love to see a good reference for this point, one that explores that practical difficulties higher-order functions cause, but the general issue is easy enough to see. This has been important for approaches to programming languages that are based on various pushout constructions for specifying rewrites. Cf. Gibbons (2002) Towards a colimit-based semantics for visual programming.
Improve this answer
$\endgroup$
9
$\begingroup$

CAML by definition is Categorical Abstract Machine Language,

however I am not cetain that you can say that an language explicitly uses category theory. Perhaps you are asking "Are there languages that allow Category Theory Concepts to be easily represented?" or perhaps you are asking if the compilation or interpretation of a particular programming language uses Category Theory in its implementation?

While technically, all Turing-complete capable languages should be equivalently able to express the same set of computations, some languages do so more elegantly than others, allowing the programmer or mathematician to be more eloquent.

I would say LISP and SCHEME, even though based on lambda-calculus, are more connected to the spirit of category theory in concept. While the numbers and integers are conceptually defined as atomic and can be built up from primitives in concept and in theory; in practice, the implementations of SCHEME and LISP and (CLU) tend to take shortcuts to speed up implementation.

The hierarchical ability to pass functions and functions of functions (etc.) as first-class parameters to functions in LISP and SCHEME let you be able to emulate the actions or morphisms of category theory better in that language than others. You just have to start from the ground up, as I have not yet seen a library or package in LISP or SCHEME for category theory.

Improve this answer
$\endgroup$
7
$\begingroup$

Here's (internet archive link) another one based on Hagino's thesis, asides charity. Implemented both in Haskell and Ruby.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ The Haskell code survives on github github.com/msakai/cpl $\endgroup$
    – j.c.
    Commented Apr 17, 2018 at 20:31
7
$\begingroup$

From the Categorical abstract machine entry on wikipedia:

"The notion of categorical abstract machine, or CAM arose in the mid-1980s and in computer science takes a place of a kind of theory of computation for programmers. In a theory CAM is represented by Cartesian closed category (c.c.c.) and embedded into the combinatory logic."

Caml (aka the basis for Microsoft's F#) is an acronym for Categorical Abstract Machine Language.

Other interesting reading is A Categorical Manifesto by Joseph Goguen.

His language project is the OBJ family of languages.

Improve this answer
$\endgroup$
4
$\begingroup$

CAML definitely uses it, but not extensively.

Improve this answer
$\endgroup$
3
$\begingroup$

See A Higher-Order Calculus for Categories by by Glynn Winskel and his student Mario Jose Cáccamo.

And also my related question.

Improve this answer
$\endgroup$
2
$\begingroup$

I have no horse in this race, as I program mostly in R, but a very good friend was very enthusiastic about F sharp as a categorical language. He claimed that it was based on category theory. I would google "F sharp category theory' for more information.

Improve this answer
$\endgroup$
1
  • 5
    $\begingroup$ F sharp is essentially ocaml + Microsoft's .NET framework. $\endgroup$
    – Najib Idrissi
    Commented Mar 28, 2019 at 14:57
2
$\begingroup$

The U.S. government has sponsored reseach in using category theory-based languages (e.g. https://www.kestrel.edu/home/projects/) with the hope specifying systems as the composition of theories using category theory to combine and refine these theories into executable robust code. The language used on some of the projects listed at the link above use the specification language Metaslang which has a subset which is executable. One side effect of this reseach led to our supporting the development of CRYPTOL, a good example of specifying a domain specific language using the functional language Haskell. In my use of Metaslang and the development environment (emacs/Specware), it is difficult to get "normal" programmers to use algebraic specification and functional programming. Despite being some of the nicest people I have met, Haskell programmers are definitely NOT normal. (;-)

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ Research in pure functional programming cannot have side-effects! $\endgroup$
    – Alex M.
    Commented May 30, 2019 at 19:09
1
$\begingroup$

https://www.npmjs.com/package/cte It's a javascript Library about Category Theory

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ This looks like implementing category-theoretical ideas, rather than using category theory itself (e.g. like Haskell, as described in other answers). $\endgroup$
    – user44191
    Commented Mar 28, 2019 at 15:16
0
$\begingroup$

Also see here.

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ That's Haskell. $\endgroup$
    – David Roberts ♦
    Commented Jun 18, 2015 at 7:16

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .