Pre-SIP: Divergence Checking for Match Type Reduction

[bishabosha]

@lluc

type Tail [ X ] = X match
    case _ *: t = > t

type Apply [ C [ _ ] , T ] = T match
    case h *: _ = > C [ h ] *: Apply [C , Tail [ T ]]

@lluc

the check can’t use the fact that Tail shrinks a concrete tuple

in the case h *: _ => branch you call Tail[T], so isnt case _ *: t => t guaranteed to reduce as we already have the evidence that _ *: _ matches?

[etaconversion]

Hi,

There seems to be a misunderstanding: I was summoned on the question by @bjornregnell whether a SIP is necessary, or not. And that is what I tried to answer. The context of the OP should make it clear they decided to proceed with a SIP, which I merely pointed out. If they want to start the process instead of just merging the PR, then that’s how it’s going to be.

As to the concrete merits of this proposal, I leave it to you to have productive discussions in this thread with the student who put a lot of work into this and would like to contribute his first ever SIP.

[lluc]

Both forms terminate. The difference is only in what the algorithm can see:

• With case h *: t => Apply[C, t], the check can see t is smaller than T, so termination is provable.
• With Apply[C, Tail[T]], the argument is an unreduced match type application. Tail[T] will in fact reduce to something smaller, but to the size measure it looks bigger, and each recursive step wraps another Tail on top: Tail[T], Tail[Tail[T]], …

An analogy of this false positive is an airport scanner: it flags every liquid because it can’t tell water from anything else. Tail[T] is a water bottle

[Sporarum]

@lluc

Both forms terminate. The difference is only in what the algorithm can see:

• With case h *: t => Apply[C, t], the check can see t is smaller than T, so termination is provable.
• With Apply[C, Tail[T]], the argument is an unreduced match type application. Tail[T] will in fact reduce to something smaller, but to the size measure it looks bigger, and each recursive step wraps another Tail on top: Tail[T], Tail[Tail[T]], …

@lluc

We apply a grace threshold to recover cases like this and keep the full community build green.

Oh!
So that allows it to “unsafely” reduce the Tail to peek at what it becomes, right ?

[bishabosha]

@lluc

With Apply[C, Tail[T]], the argument is an unreduced match type application. Tail[T] will in fact reduce to something smaller, but to the size measure it looks bigger, and each recursive step wraps another Tail on top: Tail[T], Tail[Tail[T]], …

what i was trying to get at is before you do this size estimate, is it not possible to use knowledge that Tail looks at the the same shape as the case currently matched, so then you can use that as proof it wont grow?

[lluc]

Yes — in this example the compiler could use that knowledge: h *: _ matched, and Tail’s pattern is _ *: t, so Tail[T] is guaranteed to reduce. But knowing it reduces isn’t enough; the checker needs to know it gets smaller, and the pattern doesn’t tell you that. Compare:

type Tail[X] = X match
  case _ *: t => t                  // shrinks

type Grow[X] = X match
  case _ *: t => Int *: Int *: t    // grows

Same pattern, same “proof it will match” — but recursing on Grow[T] really does diverge. And it can get worse — sometimes you can’t even tell which case will fire:

type Magic[X] = X match
  case Int *: t   => Int *: Int *: t
  case Float *: t => t

type Walk[T] = T match
  case _ *: _     => Walk[Magic[T]]
  case EmptyTuple => Int

Walk[(Float, Float)] terminates (and compiles), while Walk[(Int, Int)] diverges (and is rejected) — same code, different arguments. No local rule based on shape can separate these.

That’s the trade-off behind the check: it only looks at the arguments as written, which keeps it simple, fast, and easy to specify — at the price of a few false positives like Tail, which the grace threshold recovers.

[lluc]

Not exactly. The checker never reduces anything: it sees match type arguments as written, so to it Tail[T] stays Tail[T] (the reduction itself happens as usual, independently of the check). The grace threshold just says: don’t start checking until 10 iterations have already passed.

[bishabosha]

@lluc

which keeps it simple, fast, and easy to specify

thanks for the explaination!, it would definitely be more complex to verify, and “fast and easy to spec” are much more important.

[mbovel]

Empirically, the community build is currently our only data point. Lluc tweaked his algorithm so that all its tests pass. We should probably also try running the open community build.