Over 4000 free audio and video lectures, seminars and teaching resources from Oxford University.
Skip to Content Skip to Navigation

Thank you for visiting! Please consider filling out our questionnaire. This will help us improve our service providing free educational media recorded from the University of Oxford. Many thanks!

Click here to access the survey (3 minutes to complete).

Compiling to Categories

Loading Video...
Duration: 0:18:14 | Added: 16 Jan 2018
Conal Elliott, Target, USA, gives the first talk in the fourth panel, Program Construction, on the 2nd day of the ICFP conference.

It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea is as a collection of meaning-preserving transformations added to an existing compiler, such as GHC for Haskell. This paper describes such an implementation and demonstrates its use for a variety of interpretations including hardware circuits, automatic differentiation, incremental computation, and interval analysis. Each such interpretation is a category easily defined in Haskell (outside of the compiler). The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages.

People:
Copy and paste this HTML snippet to embed the audio or video on your site: