Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthormaxsnew
   • CommentTimeOct 2nd 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexIn "Direct Models of the Computational $\lambda$-calculus$ [pdf link](https://www.irif.fr/~mellies/mpri/mpri-ens/articles/fuhrmann-direct-models-of-computational-lambda-calculus.pdf), Fuhrmann introduces the informal concept of a "direct model" of a programming language as a semantic notion (category-like structure) whose operations directly correspond to the syntactic constructions of the syntax. Informally, a direct model "doesn't compile". For instance, they call the interpretation of call-by-value languages in the Kleisli category of a monad $T$ on a category $C$ "indirect" because you "compile" the terms of the language into morphisms of $C$ and operations in $C$ (like composition) don't correspond to something in the syntax. Instead, they propose a "direct model" with [[thunk-force categories]] that axiomatizes the structure oft he Kleisli category of a monad directly, so that for instance, composition in the thunk-force category directly corresponds to a let-binding in the original syntax. Then the Kleisli category construction is seen as a functor from categories with a monad to thunk-force categories. Munch-Maccagnoni's [[duploids]] are also presented in this vein. This seems very similar in spirit to multi-categorical approaches to syntax, as I believe the original motivation for multi-categories was similarly to have a category-like structure with closer correspondence to syntax, and then to move constructions like the [[category of contexts]] completely over to the semantic realm. What do peopl that are interested in multicategories think about this comparison? Do you have a similar term to "direct model"? I think it would be nice to have a page to collect examples of this idea and connect them.

   In “Direct Models of the Computational $\lambda$-calculus$ pdf link, Fuhrmann introduces the informal concept of a “direct model” of a programming language as a semantic notion (category-like structure) whose operations directly correspond to the syntactic constructions of the syntax. Informally, a direct model “doesn’t compile”.

   For instance, they call the interpretation of call-by-value languages in the Kleisli category of a monad $T$ on a category $C$ “indirect” because you “compile” the terms of the language into morphisms of $C$ and operations in $C$ (like composition) don’t correspond to something in the syntax. Instead, they propose a “direct model” with thunk-force categories that axiomatizes the structure oft he Kleisli category of a monad directly, so that for instance, composition in the thunk-force category directly corresponds to a let-binding in the original syntax. Then the Kleisli category construction is seen as a functor from categories with a monad to thunk-force categories. Munch-Maccagnoni’s duploids are also presented in this vein.

   This seems very similar in spirit to multi-categorical approaches to syntax, as I believe the original motivation for multi-categories was similarly to have a category-like structure with closer correspondence to syntax, and then to move constructions like the category of contexts completely over to the semantic realm.

   What do peopl that are interested in multicategories think about this comparison? Do you have a similar term to “direct model”? I think it would be nice to have a page to collect examples of this idea and connect them.