proofs vs statics?

[Brandon Barker]

I saw the following  at the beginning of "A Tutorial on Programming Features in ATS":  

The code in the dynamics of ATS is colored red unless it represents proofs, for which the color dark green is used

This is slightly confusing to me. (And I get the sense, maybe I asked this question before, years ago - if so, apologies): aren't proofs a static construct, in the sense that they aren't executed during a program's runtime?

[Hongwei Xi]

>> Aren't proofs a static construct ...

No. This is a common misconception. Proofs are dynamic

but the evaluation of proofs cause no effect on the evaluation

of a program (containing proofs) and can thus be omitted. Often

this is referred to as proof irrelevance.

You can think about it like this:

Static terms are used to clarify dynamic terms. Proofs are clarified

by static terms (props) but they themselves cannot be used to clarify
dynamic terms.

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%40googlegroups.com.

[gmhwxi]

The following article in the Effective-ATS series should be helpful:

http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/index.html

On Thursday, March 8, 2018 at 9:54:13 PM UTC-5, gmhwxi wrote:

>> Aren't proofs a static construct ...

No. This is a common misconception. Proofs are dynamic

but the evaluation of proofs cause no effect on the evaluation

of a program (containing proofs) and can thus be omitted. Often

this is referred to as proof irrelevance.

You can think about it like this:

Static terms are used to clarify dynamic terms. Proofs are clarified

by static terms (props) but they themselves cannot be used to clarify
dynamic terms.

[Brandon Barker]

Thanks, that makes good sense from what I remember. When integrating proofs in one's program, should one remember to use a compiler switch to disable a proof's evaluation in production code for performance?

On Thursday, March 8, 2018 at 9:54:13 PM UTC-5, gmhwxi wrote:

>> Aren't proofs a static construct ...

No. This is a common misconception. Proofs are dynamic

but the evaluation of proofs cause no effect on the evaluation

of a program (containing proofs) and can thus be omitted. Often

this is referred to as proof irrelevance.

You can think about it like this:

Static terms are used to clarify dynamic terms. Proofs are clarified

by static terms (props) but they themselves cannot be used to clarify
dynamic terms.

On Thu, Mar 8, 2018 at 9:47 PM, Brandon Barker <brandon...@gmail.com> wrote:

I saw the following  at the beginning of "A Tutorial on Programming Features in ATS":  

The code in the dynamics of ATS is colored red unless it represents proofs, for which the color dark green is used

This is slightly confusing to me. (And I get the sense, maybe I asked this question before, years ago - if so, apologies): aren't proofs a static construct, in the sense that they aren't executed during a program's runtime?

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

[Hongwei Xi]

Proofs are automatically eliminated after type-checking.

Proof construction offers an approach to internalizing constraint-solving.

For instance, with proofs, constraints involving multiplication can be simplified

to only involve addition.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/033e5485-f0d2-4c2e-8cc3-f4d62134e102%40googlegroups.com.

[Yannick Duchêne]

Within ATS, is it correct to say a proof is usually a dependant type? (whose value just get discarded from the generated program).

P.S. Just wanted to have a quick look at some interesting talk here. Unfortunately, I still don’t have time to get back at ATS.

[gmhwxi]

No, a proof is not a type. A proof is a total program (that is pure and terminating).

[Yannick Duchêne]

Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “proof” used alone is typically to mean proof function (I was unclear).