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).
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,On Thursday, November 21, 2013 8:59:29 PM UTC-5, gmhwxi wrote:
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).
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.On Friday, November 22, 2013 12:20:54 PM UTC-5, Brandon Barker wrote:
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,
On Thursday, November 21, 2013 8:59:29 PM UTC-5, gmhwxi wrote:
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).