58 lines
2.6 KiB
Markdown
58 lines
2.6 KiB
Markdown
# Fine-grain call-by-value
|
|
|
|
[Modelling environments in call-by-value programming languages](https://www.sciencedirect.com/science/article/pii/S0890540103000889)
|
|
|
|
## 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](https://www.cs.cmu.edu/~crary/819-f09/Moggi89.pdf)
|
|
|
|
[Notions of computation and monads](https://www.cs.cmu.edu/~crary/819-f09/Moggi91.pdf)
|
|
|
|
[The Partial Lambda Calculus](https://era.ed.ac.uk/handle/1842/419)
|
|
|
|
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 (??).
|
|
|