== and div on a recursive type

[mccraigmccraig]

I was having trouble with the div effect while trying to define == on a recursive type:

module recequals

pub rec type value
  String(s: string)
  Int(i: int)
  Array(a: list<value>)

pub fun value/(==)(a: value, b: value): bool
  match (a,b) 
    (String(aa),String(bb)) -> aa == bb
    (Int(aa),Int(bb)) -> aa == bb
    (Array(aa),Array(bb)) -> list/(==)(aa,bb)
    _ -> False

giving me an error:

effects do not match
context        :         value/(==)
term           :         value/(==)
inferred effect: total
expected effect: <div|_e>
because        : effect cannot be subsumed

so i tried re-arranging in various ways, including liberal use of pretend-decreasing like:

module recequals

import std/core/undiv

pub rec type value
  String(s: string)
  Int(i: int)
  Array(a: list<value>)

pub fun listvalue/(==)(a: list<value>, b: list<value>): bool
  match (a,b)
    ([],[]) -> True
    ([],_) -> False
    (_,[]) -> False
    (Cons(x,xs),Cons(y,ys)) -> 
      value/(==)(pretend-decreasing(x), pretend-decreasing(y)) && 
      listvalue/(==)(pretend-decreasing(xs),pretend-decreasing(ys))

pub fun value/(==)(a: value, b: value): bool
  match (a,b) 
    (String(aa),String(bb)) -> aa == bb
    (Int(aa),Int(bb)) -> aa == bb
    (Array(aa),Array(bb)) -> listvalue/(==)(aa,bb)
    _ -> False

but without any success - until i made the mutual-recursion into single-recursion:

module recequals

import std/core/undiv

pub rec type value
  String(s: string)
  Int(i: int)
  Array(a: list<value>)

pub fun value/(==)(a: value, b: value): bool
  match (a,b) 
    (String(aa),String(bb)) -> aa == bb
    (Int(aa),Int(bb)) -> aa == bb
    (Array(aa),Array(bb)) -> 
      match (aa,bb)
        ([],[]) -> True
        ([],_) -> False
        (_,[]) -> False
        (Cons(x,xs),Cons(y,ys)) -> 
          value/(==)(pretend-decreasing(x), y) && 
          value/(==)(pretend-decreasing(Array(xs)),Array(ys))
    _ -> False

and now it checks and runs fine

I'm not sure what I'm observing here - any clues greatfully received - does mutual recursion break using pretend-decreasing to remove the div effect, or have i missed something about the mutually recursive setup ?

[TimWhiting]

By the way your datastructure isn't actually rec, you can just use a plain type here.

But yes, it is known that mutual indirect recursion breaks pretend-decreasing.

Note that I think direct mutual-recursion doesn't break with pretend-decreasing (if they are both named top level functions that refer to each other directly, and not via higher order functions).

[TimWhiting]

I've raised this issue with Daan before when discussing #426 .

[TimWhiting]

In particular, some core functions (show/(==)) really need to be effect polymorphic.