Koka for loops

for.kk

effect leq<a> {
    fun leq(first: a, second: a) : bool
}

fun for(
    from: a, 
    incr: a -> <div,leq<a>|e> a, 
    to: a, 
    do: () -> <div,leq<a>|e> ()
) : <div,leq<a>|e> () {
    if (from.leq(to)) then {
        do();
        for(from.incr, incr, to, do)
    } else ()
}

fun using-for () {
    var something := 0
    with fun leq(first: int, second: int) {first <= something}
    for(0, fn (a) {a+1}, 10) {
        something := something + 1
    }

    var something-else := "a"
    with fun leq(first: string, second: string) {first <= second}
    for("", fn (a) {a+"a"}, "aaaaaaa") {
        something-else := something-else + "a"
    }

    (something, something-else)
}

Koka has a built in for loop that is better in almost every scenario, but it is specific to integers as the state of the loop. I was curious what it would look like to make a for loop that could be used with any state type.

The trickiest thing about this is making the function generic over some concept of "less or equal to", but this seems like a perfectly good case for an effect. While in the example the effect is handled directly over the for loop, in a practical code base I imagine there would be an entry point with handlers that injected a variety of such things, and that most of the code below that entry point would just carry the leq effect for any types that needed it.

Unfortunately the effect can't use (<=) as the name of the function it implements because that would collide with the built in (<=). It would be nice if things like Ord, Eq, etc. that are type classes in haskell and traits in rust were implemented generally as effects in koka, so it would be easier to abstract over them, but I don't know how feasible that is.

An alternative approach would be to have an effect which implemented both a leq function and a incr function, since those are probably related by some equational laws in any sane implementation.

The latest release of Koka supports implicit parameters, which are a better fit for this kind of polymorphism. A lot of people have independently thought about using effects for type class implementations. However, in talking with the author of Koka there were a lot of downsides of using effects that didn't justify trying to adapt effects to work well for these use cases. In contrast implicit parameters fit well. See https://github.com/koka-lang/koka/releases/tag/v3.0.1 for installation instructions for the latest version.

@TimWhiting neat! reading through the syntax sample here. That does mean that you need to "drill" implementations of the function down through the stack still though, right? As opposed to just letting the stack be generic over effect?

Effects with type parameters are no different than generic parameters as being stack generic or whatever the term might be. One major difference with implicits is that the compiler automatically applies as much as it can at the place most close to the function that needs it. So if you want to show a list<(a,a)> you don't need to "drill" down the implementation of show for lists or tuples, just for the generic type a. Also, at the place you call the function, if a is instantiated to something non-generic the compiler automatically supplies the correct show function as long as it is unambiguous. In other words, you trade adding a generic effect on the return type for adding a generic function in the parameter list, and you don't have to provide a handler in the dynamic scope. You also get more clear lexically scoped passing of the implementation, instead of an implicit dynamically scoped implementation, which could unexpectedly be overridden by a user function passed in.

But don't you need a generic function parameter for each "type class" you're handling? Or is there a way that your one generic function argument can be row typed?