Coinductive Types and Totality

[bracevac]

Thank you for this amazing language! I am intrigued about interactions between algebraic effect handlers and coinductive types, which is interesting in the context of reactive programming.

The effect inference seems to reject simple functions on coinductive streams, e.g.,

cotype stream<a> {
  SCons(hd: a, tl: stream<a>)
}

fun hist_helper(s: stream<a>, state: list<a>): stream<list<a>> {
  val next = Cons(s.hd, state)
  SCons(next, hist_helper(s.tl, next))
}

fun stake(s: stream<a>, n: int): list<a> {
  if (n <= 0) return Nil
  else return Cons(s.hd, stake(s.tl, n - 1))
}

Both functions are rejected:

error: effects do not match
  ...
  inferred effect: total
  expected effect: <div|_e>
  because        : effect cannot be subsumed

From my understanding of coinductive types, I would expect that the inferred total effect is correct in both cases. Why is divergence expected? Can we massage the definitions so that they are accepted as total functions? Thanks for any help.

[bracevac]

I can at least partially answer my own question: The second function stake is accepted if we use peano numbers instead if int, e.g.,

type nat {
   Zero
   Succ(pred: nat)
}

fun stake(s: stream<a>, n: nat): total list<a> {
   match(n) {
     Zero -> Nil
     Succ(m) -> Cons(s.hd, ptake(s.tl, m))
   }
}

However, I am still curious if it is currently possible to declare functions likehist_helper as total by some reformulation of the definition.

[anfelor]

@bracevac I was just looking at this and realized it was still unsolved. Even the reformulation:

co type stream<a> {
  SCons(hd: a, tl: stream<a>)
}

fun hist_helper(s: stream<a>, state: list<a>): stream<list<a>> {
  match(s) {
      SCons(hd, tl) {
        val next = Cons(hd, state)
        SCons(next, hist_helper(tl, next))
      }
  }
}

still requires the div effect. Together with #149 this could be a good opportunity for an intern to work on. What do you think @daanx ?