Compiler inferring exn effect that I believe is not true... how to eliminate?

[dcurrie]

In my evolving bbtree exploration, I'm having trouble eliminating an inferred exn that (if I understand what Koka is saying) is provably impossible. Here is the function in question:

private fun glue(left: bbtree<k,v>, right: bbtree<k,v>): bbtree<k,v> {
    fun extract-min(node: bbtree<k,v>): (k, v, bbtree<k,v>) {
        match(node) {
            Node(BbNil, tr, _, tk, tv) ->
                (tk, tv, tr)
            Node(tl, tr, _, tk, tv) ->
                match(extract-min(tl)) {
                    (mink, minv, nodep) -> (mink, minv, balance(nodep, tk, tv, tr))
                }
        }
    }
    fun extract-max(node: bbtree<k,v>): (k, v, bbtree<k,v>) {
        match(node) {
            Node(tl, BbNil, _, tk, tv) ->
                (tk, tv, tl)
            Node(tl, tr, _, tk, tv) ->
                match(extract-max(tr)) {
                    (maxk, maxv, nodep) -> (maxk, maxv, balance(tl, tk, tv, nodep))
                }
        }
    }
    match (left, right) {
        (l, BbNil) -> l
        (BbNil, r) -> r
        _ ->
            if (node-size(left) > node-size(right)) {
                match(extract-max(left)) {
                    (maxk, maxv, leftp) -> new-node(leftp, maxk, maxv, right)
                }
            }
            else {
                match(extract-min(right)) {
                    (mink, minv, rightp) -> new-node(left, mink, minv, rightp)
                }
            }
    }
}

and as before:

public type bbtree<k,v> {
  BbNil
  Node(left: bbtree<k,v>, right: bbtree<k,v>, size: int, key: k, value: v)
}

but note that I renamed Nil to BbNil to eliminate "identifier Nil is ambiguous" errors.

Koka is complaining that extract-min and extract-max and later glue need exn effect, I suspect because it thinks the match is not exhaustive... but it is since I test for BbNil above, e.g., before the call to extract-min and extract-max and in their recursive calls. The argument node in those functions can never be BbNil.

check  : bbtree
bbtree.kk(158,61): error: effects do not match
  context        :     fun extract-min(node: bbtree<k,v>): (k, v, bbtree<k,v>) {
                   ...
                       }
  term           :                                                             {
                   ...
                       }
  inferred effect: <exn|_e>
  expected effect: (<>)

Is there a way to work around this? I don't want all my library functions that call glue to be non-total.

If you want more context the code is in this github repo

[daanx]

Hi @dcurrie. Well, Koka is very predictable with inferring exn and div on purpose -- this is to make the type inference stable and predictable. But it comes at a price that it does not do cross-function analysis but just per-match. One thing we can do is change our attitude: in the most "pure" language out there, Haskell, all functions are pure which is <div,exn> in Koka :-) So, exn is not too bad ;-)

In the above case though, I think it is easiest to make the match more apparent to Koka, especially since extract-min and extract-max are "double" matching on Node each time and then match one level deeper in there. We can lift that out and pass the fields of the node directly as parameters:

fun glue(left: bbtree<k,v>, right: bbtree<k,v>): bbtree<k,v> {
  fun extract-min(l,r,k,v) {
    match(l) {
      BbNil -> (k,v,r)
      Node(ll, lr, _, lk, lv) -> match(extract-min(ll,lr,lk,lv)) {
        (mink, minv, nodep) -> (mink, minv, balance(nodep, k, v, r))
      }
    }
  }
  fun extract-max(l,r,k,v) {
    match(r) {
      BbNil -> (k,v,l)
      Node(rl, rr, _, rk, rv) -> match(extract-max(rl,rr,rk,rv)) {
        (maxk, maxv, nodep) -> (maxk, maxv, balance(l, k, v, nodep))
      }
    }
  }
  match (left, right) {
    (l, BbNil) -> l
    (BbNil, r) -> r
    (Node, Node(l,r,_,k,v)) | node-size(left) > node-size(right)
      -> match(extract-max(l,r,k,v)) {
           (maxk, maxv, leftp) -> new-node(leftp, maxk, maxv, right)
         }
    (Node(l,r,_,k,v),Node) 
      -> match(extract-min(l,r,k,v)) {
           (mink, minv, rightp) -> new-node(left, mink, minv, rightp)
         }
  }
}

this is total now. Maybe rename BbNil to Leaf or Tip ?

[dcurrie]

That same thought, reorganize to pass fields rather than nodes to the recursion, occurred to me as I woke up this morning. You beat me to it, and wrote the code! Thank you for your help. I will try Tip to avoid the "identifier Nil is ambiguous" errors.