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.