5 ms·

This includes a fresh take on the foundations of the correspondence between cartesian closed categories with simply typed lambda calculus that underlies the bea

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 http://conal.net/papers/compiling-to-categories.

macawfish 7y ago
Woah... watching his talk now and it's really motivating, thanks for sharing!
- deleted 7y ago
  [deleted]
agumonkey 7y ago
it's been so long since I've read anything about Conal :)
StandardFuture 7y ago
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.
- lidHanteyk 7y ago
  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.
  - StandardFuture 7y ago
    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.
    - platz 7y ago
      That's kind of like asking of the research being done at fermilab is on npm yet.
    - lidHanteyk 7y ago
      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-categories.pdf http://conal.net/papers/compiling-to-categories/compiling-to...
      - Koshkin 7y ago
        > how Well, looks like it doesn’t... (Not that it’s the point of this research.)

macawfish 7y ago

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

deleted 7y ago
[deleted]

agumonkey 7y ago

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

StandardFuture 7y ago

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.

lidHanteyk 7y ago
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.
- StandardFuture 7y ago
  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.
  - platz 7y ago
    That's kind of like asking of the research being done at fermilab is on npm yet.
  - lidHanteyk 7y ago
    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-categories.pdf http://conal.net/papers/compiling-to-categories/compiling-to...
    - Koshkin 7y ago
      > how Well, looks like it doesn’t... (Not that it’s the point of this research.)