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.
On Thu, Mar 8, 2018 at 9:59 PM, Brandon Barker <[email protected]> wrote: > 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 <[email protected]> >> 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 [email protected]. >>> To post to this group, send email to [email protected]. >>> 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/ms >>> gid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%40go >>> oglegroups.com >>> <https://groups.google.com/d/msgid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%40googlegroups.com?utm_medium=email&utm_source=footer> >>> . >>> >> >> -- > 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 [email protected]. > To post to this group, send email to [email protected]. > 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 > <https://groups.google.com/d/msgid/ats-lang-users/033e5485-f0d2-4c2e-8cc3-f4d62134e102%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To post to this group, send email to [email protected]. 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/CAPPSPLpgLPuwCeFtc3OBwisC3RTV9FSFLcb3k4C5ex3RZFfq3A%40mail.gmail.com.
