Aspects of Categorical Recursion Theory | Hacker News Reader

Aspects of Categorical Recursion Theory

arxiv.org

85 pointsjesuslop10 comments

This includes a fresh take on the foundations of the correspondence between cartesian closed categories with simply typed lambda calculus that underlies the beautiful work of Conal Elliott in http://conal.net/papers/compiling-to-categories.

Woah... watching his talk now and it's really motivating, thanks for sharing!

it's been so long since I've read anything about Conal :)

I am not sure I understand what are the strongest motivations behind "compiling to categories". Is this an improved formal verification motivation? What does it gain over existing programming languages? In what scenario does a working programmer decide to utilize these concepts? Genuine questions, btw.

It gives a turn-the-crank construction for programming languages.

* Describe the values you wish to study

* Find a category whose objects are the types of your values

* Give the category Cartesian closed structure

And now you have a lambda calculus with exactly the structures that you want to study!

MarshallB is an example of a language constructed this way.

ah ha, so it is a nice formal framework for domain-specific language creation.

I think it could be really useful to design a walk-through of how exactly it can be used as such for everyday programmers.

That's kind of like asking of the research being done at fermilab is on npm yet.

Read "Compiling to Categories" [0] for the basics of the conceptual framework and how it applies to everyday programming.

[0] http://conal.net/papers/compiling-to-categories/compiling-to...

> how

Well, looks like it doesn’t... (Not that it’s the point of this research.)

See also "Generalized Arrows" https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-...

Abstract:

> Multi-level languages and arrows both facilitate metaprogramming, the act of writing a program which generates a program. The arr function required of all arrows turns arbitrary metalanguage expressions into object language expressions; because of this, arrows may be used for metaprogramming only when the object language is a superset of the metalanguage.

> This thesis introduces generalized arrows, which are less restrictive than arrows in that they impose no containment relationship between the object language and metalanguage; this allows generalized arrows to be used for heterogeneous metaprogramming. This thesis also establishes a correspondence between two-level programs and one-level programs which take a generalized arrow instance as a distinguished parameter. A translation across this correspondence is possible, and is called a flattening transformation.

> The flattening translation is not specific to any particular object language; this means that it needs to be implemented only once for a given metalanguage compiler. Support for various object languages can then be added by implementing instances of the generalized arrow type class; this does not require knowledge of compiler internals. Because of the flattening transformation the users of these object languages are able to program using convenient multi-level types and syntax; the conversion to one-level terms manipulating generalized arrow instances is handled by the flattening transformation.

> A modified version of the Glasgow Haskell Compiler (GHC) with multi-level types and expressions has been produced as a proof of concept. The Haskell extraction of the Coq formalization in this thesis have been compiled into this modified GHC as a new flattening pass.

Reply on news.ycombinator.com