Modular Implicits

[TimWhiting]

Using structs for implicits can help with collections / monads etc: See for example the .?struct examples: https://github.com/koka-lang/koka/blob/dev/test/overload/monad3.kk.

However in some cases you'd really like the assurance that there is only one sort function that your type uses for example, so that you don't end up sorting forwards then backwards, etc.

Consider modules as an implicit scope. For example imagine defining implicit functions needed for the module:

module treeset<?a>(?cmp: (a, a) -> order)
struct tree<?a>
  ...

pub empty = Empty
pub add(t: tree<?a>..)
   ?cmp()

Now consider importing it like this:

import treeset<int>() = ti

ti/empty 
...

Now if the map escapes this module you probably want to pub import treeset<int>() = ti and you want the imports to see all of the functions from treeset as being qualified by ti as well, so we need to propagate import maps. We almost want the types defined to be in a new scope / distinguished from types imported into another module explicitly.

For example:

module a 
pub import treeset<int>(?cmp=backwards) = ti
fun create()
  ti/empty

module b
pub import treeset<int>() = ti // infer implicits
fun create()
  ti/empty 

module c
import a
import b
val x = a/create()
val y = b/create()
x.add() // This is the type a/ti/tree, and uses the implicit given by a
y.add() // This is the type b/ti/tree, and uses the implicit given by b

Implementation:

The add function in the treeset module uses the module's implicit, so it get's translated to a function with an implicit parameter by that name. But maybe a special implicit parameter name scheme so it cannot be resolved with regular implicits. (note that regular implicits still have their uses for most functions, like sort-by on lists, or addition of numbers, etc. It is only when a datatype is constructed using an invariant that needs to be preserved when you want modular implicits.

The implicits for the module are resolved at the import statement, in other words all definitions in the module are partially applied using the implicits provided.

So in other words, we don't actually monomorphize the module's code, we just instantiate all the definitions, and qualify the types (so that two of the same type but imported from different modules will use the module's instantiation of the imported functions).

[TimWhiting]

One alternative to this is to just have tree carry it's own sort function - bad idea for a recursive datastructure - because of wasted space, or wrap tree with a treeset datastructure - which then requires unwrapping / rewrapping all the time. The advantage of the wrapping approach is that it is less 'magic' type system stuff or extra compiler work. After all the tree datastructure could be used in different contexts where it might be okay to switch the sort function you use. Or maybe you have a function that changes the sort function and resorts everything in the datastructure (or rehashes a datastructure). So in one sense it is the set wrapper of the tree that requires the invariant and not the tree itself.

However using the wrapping technique, I wish there were better syntax / support for unwrapping / rewrapping a struct with one constructor. It's essentially a mostly transparent wrapper that just ensures the implicits are resolved the same. Ideally I want to be able to match on the tree when I add functionality to the set, and not match on the wrapper.

In other words ideally this:

fun add(t: unwrap treeset<a>, a: a)
  match t
     Node(l, c, r) -> add(...)
     Leaf -> Node(Leaf, a, Leaf)

turns into the following where the struct is unwrapped, and the functionality is proxied, note that the outer wrapper can always be used in-place, and that this only really makes sense for structs - not any datatype.

fun add(t: treeset<a>, a: a)
  match t
    Treeset(t', cmp) -> Treeset(unwrap/add(t', a, cmp), cmp)

fun unwrap/add(t: tree<a>, a: a, cmp: (a, a) -> order): tree<a>
  match t
     Node(l, c, r) -> add(...)
     Leaf -> Node(Leaf, a, Leaf)

[chtenb]

In your example code it says val y = a/create(), but should that be val y = b/create()?