2.6 KiB
Fine-grain call-by-value
Modelling environments in call-by-value programming languages
Mathematical structures
I don't understand what the introduction is writing about. Will update this section after reading those categorical structures.
- monoidal
- premonoidal
Moggi's Language
Computational lambda-calculus and monads
Notions of computation and monads
To summary, this paper introduces Moggi's lambda-c calculus for the global store model. In this model, if a term has no side-effect then it is a value, and denoted with a downward arrow. Generally, terms are considered with side-effect and are called producer.
In Moggi's lambda-c calculus, producers are typed as functions from (store, environment) to (store, type). But this model has a few problems, (which I don't fully understand yet). And it is solved in the monadic metalanguage. In this language model, a general term is typed as functions from (environment) to (type).
In my own concept, I often think of these as computations and values. Values are themselves the minimal term, result of some computations. Computations must be invoked to produce values, hence they are similar to this thinking of producer.
Fine-grain call-by-value
From Moggi's two languages, lambda-c calculus and monadic metalanguage, two special terminologies are introduced, value and producer.
Although monadic metalanguage solves all problems (by not having them in the first place) of lambda-c calculus, it is hard to give them operational semantics.
This is probably because monadic metalanguage only has value terms and they do not intefere with the global store.
Fine-grain call-by-value has two separated judgements for value terms and producer terms.
First observation, producer terms must be evaluated to a value and then it can be used. A value can be turned into a producer. Then type rules are given for each combinations of value, or producer.
Freyd category
This category is used to define call-by-value languages.
Freyd categories thus provide a categorical semantics for typed programming languages with side effects such as memory access or printing.
???
?? To be written
Conclusions
Categorical models of call-by-value programming with effects:
- Strong monads
- Freyd categories
- Strong K-categories
are equivalent to each other, and equivalent to fine-grain call-by-value equational theory (??).