4 ms·

Aspects of Categorical Recursion Theory

85 points by jesuslop 7y ago

jesuslop 7y ago
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.)
carapace 7y ago
See also "Generalized Arrows" https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.html 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.

85 points by jesuslop 7y ago

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.)

carapace 7y ago

See also "Generalized Arrows" https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.html 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.