What is =>> for?

[gmhwxi]

Say we want to implement a function for testing whether a given list is nil:

fun{a:t@ype}
list_is_nil{n:int}
  (xs: list (a, n)): bool (n==0) =
  case+ xs of list_nil () => true  | _ => false
// end of [list_is_nil]

What the type for this function says is clear:

Given a list of length n, the return boolean value equals (n==0);
in other words, the return value is true if and only if n equals 0.

However, the above code does not typecheck as typechecking in ATS
does not handle pattern matching clauses sequentially. For instance, when
the second clause '_ => false' is checked, there is no assumption that
xs does not match the pattern list_nil().

If one wants to enforce sequentiality in typechecking clauses, than the
symbol =>> should be in place of =>. For instance, the following code
typechecks:

fun{a:t@ype}
list_is_nil{n:int}
  (xs: list (a, n)): bool (n==0) =
  case+ xs of list_nil () => true  | _ =>> false
// end of [list_is_nil]

Enforcing sequentiality in typechecking clauses is not by default because doing
so can be computationally expensive (exponential-time).

[Brandon Barker]

If we have more than one =>> in the same case, does it matter? Or does having a single =>> guarantee that each pattern is checked sequentially according to the written order?

I suppose this relates to having an exponential-growth structure (like an if-then-else with nesting allowed) versus linear growth with a sequential structure (if-elseif...elseif...else with no nesting). No sequentiality at all could, I guess, be done in parallel. My understanding is that the case clauses are more like the linear growth sequential structure - where does exponential growth come in? 

Thanks, 

[gmhwxi]

You can have several clauses using =>> in one case-expression.

A single =>> only guarantees that the particular clause using it needs to be checked under the assumption
that the clauses ahead of it are not matched.

Computing the complement of a pattern is exponential-time.