Proofs affecting the dynamic semantics?

[Koji Hattori]

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.

[Hongwei Xi]

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!

--
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.

[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!

--

[Koji Hattori]

Thank you for fixing it quickly!

I feel relieved that it was just a bug.


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

[gmhwxi]

>>I feel relieved that it was just a bug. :)

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

[Yannick Duchêne]

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.html