Assumptions generated from case statements?

Google Group
1

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .. (n: int step): void =
if n = 0 then () else loop(n - 1)

This one don’t:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ => loop(n - 1)

So I wanted to try to be explicit:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ =>
let prval () = prop_verify_and_add{step > 0}()
in loop{step - 1}(n - 1)
end

It seems not ovious to the checker, that step is greater than zero. It
knows it when an if statement is used, and don’t when a case statement
is used.

This raises the question: what are the assumptions automatically generated
by a case statement, if there are?

Or may be to be more general: what statements generates what assumptions?

A question aside: the “add” in prop_verify_and_add means “add to the
store of available assumptions”, isn’t it? (just to be sure)

2

_ => …

should be changed into

_ =>> …

See:

Redirecting to Google Groups Tue, May 12, 2015 at 7:29 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .. (n: int step): void =
if n = 0 then () else loop(n - 1)

This one don’t:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ => loop(n - 1)

So I wanted to try to be explicit:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ =>
let prval () = prop_verify_and_add{step > 0}()
in loop{step - 1}(n - 1)
end

It seems not ovious to the checker, that step is greater than zero. It
knows it when an if statement is used, and don’t when a case statement
is used.

This raises the question: what are the assumptions automatically generated
by a case statement, if there are?

Or may be to be more general: what statements generates what assumptions?

A question aside: the “add” in prop_verify_and_add means “add to the
store of available assumptions”, isn’t it? (just to be sure)

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/bbf20cec-7ce3-44a7-8be9-a9c079a1a3cf%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

If you really want to do it this way, you need to add the following line
first:

val () = assertloc (n > 0)

I don’t know if “need” means “should” or “must” here, as it seems to
type-check without it and the =>> is enough. Or may that’s because the
sample is simple.

4

A question aside: the “add” in prop_verify_and_add means “add to the
store of available assumptions”, isn’t it? (just to be sure)

Yes, that is true.

If you really want to do it this way, you need to add the following line
first:

val () = assertloc (n > 0)On Tuesday, May 12, 2015 at 7:29:14 PM UTC-4, Yannick Duchêne wrote:

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .. (n: int step): void =
if n = 0 then () else loop(n - 1)

This one don’t:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ => loop(n - 1)

So I wanted to try to be explicit:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ =>
let prval () = prop_verify_and_add{step > 0}()
in loop{step - 1}(n - 1)
end

It seems not ovious to the checker, that step is greater than zero. It
knows it when an if statement is used, and don’t when a case statement
is used.

This raises the question: what are the assumptions automatically generated
by a case statement, if there are?

Or may be to be more general: what statements generates what assumptions?

A question aside: the “add” in prop_verify_and_add means “add to the
store of available assumptions”, isn’t it? (just to be sure)

5

Using =>> is the right way to address the issue here.

However, I want to make a point that I think is rather important in
practice.

ATS has a lot of features. Compare it to C++. To use a feature, one has to
know it first. If one tries to do everything in ATS rigorously, then the
learning
curve would be too steep to be acceptable. So my point is that one should be
ready to use features like $UN.cast and assertloc to bypass typechecking,
sometimes.

Being rigorous means very little if proofs/programs could not be effectively
constructed in the first place. So I keep emphasizing here on program-first
program verification.On Tuesday, May 12, 2015 at 8:02:27 PM UTC-4, Yannick Duchêne wrote:

Le mercredi 13 mai 2015 01:38:30 UTC+2, gmhwxi a écrit :

If you really want to do it this way, you need to add the following line
first:

val () = assertloc (n > 0)

I don’t know if “need” means “should” or “must” here, as it seems to
type-check without it and the =>> is enough. Or may that’s because the
sample is simple.

6

Using =>> is the right way to address the issue here.

However, I want to make a point that I think is rather important in
practice.

ATS has a lot of features. Compare it to C++. To use a feature, one has to
know it first. If one tries to do everything in ATS rigorously, then the
learning
curve would be too steep to be acceptable. So my point is that one should
be
ready to use features like $UN.cast and assertloc to bypass typechecking,
sometimes.

I see: assertloc is a runtime check, which adds an assumption. I
always though it was just like a debugging utility method as is assert or
similar in other languages.

Indeed, that make it a good path to go toward check ahead without being
blocked on an unsolvable case on the beginning. It happened I wished the
languages with dynamic assertions (ex. Python), could make some assumptions
based on the assertions statement. So ATS has this… very good to know.

7

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .. (n: int step): void =
if n = 0 then () else loop(n - 1)

This one don’t:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ => loop(n - 1)

[…]

Something similar with conjunctions. Doing this:

if cond1 && cond2 then
…

Conclusions from cond1 are seen, but not conclusions from cond2, and
this, has to be used instead:
if cond1 then
if cond2 then
…

(I don’t mind, I’m noting this here for documentation)

8

*which adds an assumption

Yes!!! :slight_smile:

This is the point. Trying to use run-time checks to establish
static assumptions is cheap and effectively. A lot of people
are kind of shy about using run-times checks; they prefer to prove
these assumptions. More likely than not, these people do not get
to write a lot of code at the end. Actually, more likely than not, they
do not get to write much functioning code at the end :(On Tuesday, May 12, 2015 at 11:25:16 PM UTC-4, Yannick Duchêne wrote:

Le mercredi 13 mai 2015 03:01:59 UTC+2, gmhwxi a écrit :

Using =>> is the right way to address the issue here.

However, I want to make a point that I think is rather important in
practice.

ATS has a lot of features. Compare it to C++. To use a feature, one has to
know it first. If one tries to do everything in ATS rigorously, then the
learning
curve would be too steep to be acceptable. So my point is that one should
be
ready to use features like $UN.cast and assertloc to bypass typechecking,
sometimes.

I see: assertloc is a runtime check, which adds an assumption. I
always though it was just like a debugging utility method as is assert or
similar in other languages.

Indeed, that make it a good path to go toward check ahead without being
blocked on an unsolvable case on the beginning. It happened I wished the
languages with dynamic assertions (ex. Python), could make some assumptions
based on the assertions statement. So ATS has this… very good to know.

9

You could also write:

If cond1 * cond2 then …

Note that ‘*’ is a function; both cond1 and cond2 are evaluates even if
cond1 is false.On Thursday, May 14, 2015 at 1:25:29 AM UTC-4, Yannick Duchêne wrote:

Le mercredi 13 mai 2015 01:29:14 UTC+2, Yannick Duchêne a écrit :

Hi there,

Here is a sample which pass type‑checking:

fun loop {step: nat} .. (n: int step): void =
if n = 0 then () else loop(n - 1)

This one don’t:

fun loop {step: nat} .. (n: int step): void =
case+ n of
| 0 => ()
| _ => loop(n - 1)

[…]

Something similar with conjunctions. Doing this:

if cond1 && cond2 then
…

Conclusions from cond1 are seen, but not conclusions from cond2, and
this, has to be used instead:
if cond1 then
if cond2 then
…

(I don’t mind, I’m noting this here for documentation)