Proofs affecting the dynamic semantics?

Google Group
1

Hi all,

In ATS, I expected proof terms only to prove some properties of dynamic
terms at compile-time,
but not to affect the dynamic semantics at run-time.

I think the following example should be rejected because function 'f’
contains a case-expression
by proof term ‘p’ as a dynamic value, but the ATS2 compiler accepts it:

dataprop PROP (int) =
| case1 (1)
| case2 (2)

fn f {n : int} (p : PROP n | a : int n) : int n =
case p of
| case1 () => (println!(“case1”); 1)
| case2 () => (println!(“case2”); a)

implement main0 () = {
val one : int(1) = f (case1 | 1) // case1
val () = println!(one) // 1
val two : int(2) = f (case2 | 2) // case1
val () = println!(two) // 1
}

It actually runs outputting such like the comments. The case-expression
seems to always match
the first clause regardless of the proof. Indeed this behavior is not
affected by the proof, but
differs from what I expected and seems to break type safety.

Then my questions are:

  1. Is it a bug of the compiler that the example passes type-checking?
  2. Is there another kind of dynamic expressions that appear to be
    affected by a proof?
  3. If we reject such dynamic case-expressions by a proof as the example,
    can another problem arise?

Thank you.

2

Thank you for fixing it quickly!

I feel relieved that it was just a bug.

2015年5月21日木曜日 1時14分57秒 UTC+9 gmhwxi:

3

I feel relieved that it was just a bug. :slight_smile:

The issue is actually handled correctly in ATS1.
I once wrote a paper on the issue of proof erasure:

Attributive Types for Proof Erasure. In the post-workshop proceedings of
the international workshop TYPES’07, LNCS vol. 4941, December 2007On Friday, May 22, 2015 at 10:20:11 AM UTC-4, Koji Hattori wrote:

Thank you for fixing it quickly!

I feel relieved that it was just a bug.

2015年5月21日木曜日 1時14分57秒 UTC+9 gmhwxi:

I think I have fixed this bug. The changes are now in
Github and will be included in the next release.

Is it a bug of the compiler that the example passes type-checking?

As it stands now, this example will pass typechecking. It only fails
during the phase of proof erasure.

On Wednesday, May 20, 2015 at 3:27:02 AM UTC-4, gmhwxi wrote:

This is definitely a bug in the compiler.

When ‘f’ is being compiled, ‘p’ should have already been erased. I will
try to fix this bug.

1: Yes
2: No
3: Should not

Thanks for reporting it!

On Wed, May 20, 2015 at 3:12 AM, Koji Hattori <k-…> wrote:

Hi all,

In ATS, I expected proof terms only to prove some properties of dynamic
terms at compile-time,
but not to affect the dynamic semantics at run-time.

I think the following example should be rejected because function ‘f’
contains a case-expression
by proof term ‘p’ as a dynamic value, but the ATS2 compiler accepts it:

dataprop PROP (int) =
| case1 (1)
| case2 (2)

fn f {n : int} (p : PROP n | a : int n) : int n =
case p of
| case1 () => (println!(“case1”); 1)
| case2 () => (println!(“case2”); a)

implement main0 () = {
val one : int(1) = f (case1 | 1) // case1
val () = println!(one) // 1
val two : int(2) = f (case2 | 2) // case1
val () = println!(two) // 1
}

It actually runs outputting such like the comments. The case-expression
seems to always match
the first clause regardless of the proof. Indeed this behavior is not
affected by the proof, but
differs from what I expected and seems to break type safety.

Then my questions are:

  1. Is it a bug of the compiler that the example passes
    type-checking?
  2. Is there another kind of dynamic expressions that appear to be
    affected by a proof?
  3. If we reject such dynamic case-expressions by a proof as the
    example, can another problem arise?

Thank you.

–

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/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com?utm_medium=email&utm_source=footer
.

4

I think I have fixed this bug. The changes are now in
Github and will be included in the next release.

Is it a bug of the compiler that the example passes type-checking?

As it stands now, this example will pass typechecking. It only fails
during the phase of proof erasure.On Wednesday, May 20, 2015 at 3:27:02 AM UTC-4, gmhwxi wrote:

This is definitely a bug in the compiler.

When ‘f’ is being compiled, ‘p’ should have already been erased. I will
try to fix this bug.

1: Yes
2: No
3: Should not

Thanks for reporting it!

On Wed, May 20, 2015 at 3:12 AM, Koji Hattori <k- k-hatt...@r3.dion.ne.jp…> wrote:

Hi all,

In ATS, I expected proof terms only to prove some properties of dynamic
terms at compile-time,
but not to affect the dynamic semantics at run-time.

I think the following example should be rejected because function ‘f’
contains a case-expression
by proof term ‘p’ as a dynamic value, but the ATS2 compiler accepts it:

dataprop PROP (int) =
| case1 (1)
| case2 (2)

fn f {n : int} (p : PROP n | a : int n) : int n =
case p of
| case1 () => (println!(“case1”); 1)
| case2 () => (println!(“case2”); a)

implement main0 () = {
val one : int(1) = f (case1 | 1) // case1
val () = println!(one) // 1
val two : int(2) = f (case2 | 2) // case1
val () = println!(two) // 1
}

It actually runs outputting such like the comments. The case-expression
seems to always match
the first clause regardless of the proof. Indeed this behavior is not
affected by the proof, but
differs from what I expected and seems to break type safety.

Then my questions are:

  1. Is it a bug of the compiler that the example passes type-checking?
  2. Is there another kind of dynamic expressions that appear to be
    affected by a proof?
  3. If we reject such dynamic case-expressions by a proof as the
    example, can another problem arise?

Thank you.

–

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/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

It’s there: https://www.cs.bu.edu/~hwxi/academic/papers/types07.pdf
Got it from here: https://www.cs.bu.edu/~hwxi/academic/publications.htmlLe vendredi 22 mai 2015 17:35:51 UTC+2, gmhwxi a écrit :

I feel relieved that it was just a bug. :slight_smile:

The issue is actually handled correctly in ATS1.
I once wrote a paper on the issue of proof erasure:

Attributive Types for Proof Erasure. In the post-workshop proceedings of
the international workshop TYPES’07, LNCS vol. 4941, December 2007

On Friday, May 22, 2015 at 10:20:11 AM UTC-4, Koji Hattori wrote:

Thank you for fixing it quickly!

I feel relieved that it was just a bug.

2015年5月21日木曜日 1時14分57秒 UTC+9 gmhwxi:

I think I have fixed this bug. The changes are now in
Github and will be included in the next release.

Is it a bug of the compiler that the example passes type-checking?

As it stands now, this example will pass typechecking. It only fails
during the phase of proof erasure.

On Wednesday, May 20, 2015 at 3:27:02 AM UTC-4, gmhwxi wrote:

This is definitely a bug in the compiler.

When ‘f’ is being compiled, ‘p’ should have already been erased. I will
try to fix this bug.

1: Yes
2: No
3: Should not

Thanks for reporting it!

On Wed, May 20, 2015 at 3:12 AM, Koji Hattori <k-…> wrote:

Hi all,

In ATS, I expected proof terms only to prove some properties of
dynamic terms at compile-time,
but not to affect the dynamic semantics at run-time.

I think the following example should be rejected because function ‘f’
contains a case-expression
by proof term ‘p’ as a dynamic value, but the ATS2 compiler accepts it:

dataprop PROP (int) =
| case1 (1)
| case2 (2)

fn f {n : int} (p : PROP n | a : int n) : int n =
case p of
| case1 () => (println!(“case1”); 1)
| case2 () => (println!(“case2”); a)

implement main0 () = {
val one : int(1) = f (case1 | 1) // case1
val () = println!(one) // 1
val two : int(2) = f (case2 | 2) // case1
val () = println!(two) // 1
}

It actually runs outputting such like the comments. The
case-expression seems to always match
the first clause regardless of the proof. Indeed this behavior is not
affected by the proof, but
differs from what I expected and seems to break type safety.

Then my questions are:

  1. Is it a bug of the compiler that the example passes
    type-checking?
  2. Is there another kind of dynamic expressions that appear to be
    affected by a proof?
  3. If we reject such dynamic case-expressions by a proof as the
    example, can another problem arise?

Thank you.

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/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com?utm_medium=email&utm_source=footer
.

6

This is definitely a bug in the compiler.

When ‘f’ is being compiled, ‘p’ should have already been erased. I will try
to fix this bug.

1: Yes
2: No
3: Should not

Thanks for reporting it!On Wed, May 20, 2015 at 3:12 AM, Koji Hattori k-hatt...@r3.dion.ne.jp wrote:

Hi all,

In ATS, I expected proof terms only to prove some properties of dynamic
terms at compile-time,
but not to affect the dynamic semantics at run-time.

I think the following example should be rejected because function ‘f’
contains a case-expression
by proof term ‘p’ as a dynamic value, but the ATS2 compiler accepts it:

dataprop PROP (int) =
| case1 (1)
| case2 (2)

fn f {n : int} (p : PROP n | a : int n) : int n =
case p of
| case1 () => (println!(“case1”); 1)
| case2 () => (println!(“case2”); a)

implement main0 () = {
val one : int(1) = f (case1 | 1) // case1
val () = println!(one) // 1
val two : int(2) = f (case2 | 2) // case1
val () = println!(two) // 1
}

It actually runs outputting such like the comments. The case-expression
seems to always match
the first clause regardless of the proof. Indeed this behavior is not
affected by the proof, but
differs from what I expected and seems to break type safety.

Then my questions are:

  1. Is it a bug of the compiler that the example passes type-checking?
  2. Is there another kind of dynamic expressions that appear to be
    affected by a proof?
  3. If we reject such dynamic case-expressions by a proof as the
    example, can another problem arise?

Thank you.

–
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/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/807ddb90-a3a2-4fdb-970b-1f9964a12818%40googlegroups.com?utm_medium=email&utm_source=footer
.