dok/paper/programming-with-implicit-values
[1] J. Brachthäuser and D. Leijen, “Programming with Implicit Values, Functions, and Controlor, Implicit Functions: Dynamic Binding with Lexical ScopingMicrosoft Technical Report, MSR-TR-2019-7, v2.,” p. 27.
Define the semantic of a language with dynamic vars as optional named params, and with dynamic functions.
FACT in Dok they are called cntxs.
MAYBE in Dok a cntxs can be associated to a function that can be overwritten, or maybe only to a parametric function that can be instantiated with params
It uses implicit functions (i.e. dynamic functions) also for managing ad-hoc control operations like backtraking (maybe also effects).
The semantic is formalized using the lambda calculus of dynamic binds.
It maps the language to a calculus with effects.
All these features are implemented in Koka, that is a language: functional; typed; with effects; with implicit params; with implicit functions.
In Dok the implicit values are declarated as cntxs
of a data type or trait, and then they can be references by all methods. In Koka is something of similar, but it is a type derived for each function, and not for each class.
Probably I don’t need this approach, because I can reuse already existing Dok features:
- implicit functions can be normal methods reading cntx vars
- dynamic setting of implicit functions can be normal variants and inheritance or added params to the function
- effects are modelled extending the compiler and adding a new DSL
The semantic of Koka can become tricky because there are many different aspects to combine. Instead in Dok there is a simpler semantic, and then it is extended the compiler.