Prfn and prfun in ATS2 (fwd)

Google Group
1

I came to an example here:
http://bluishcoder.co.nz/2013/07/01/constructing-proofs-
with-dataprop-in-ats.html

 dataprop
 BEAUTIFUL (n: int) =
 | B_0 (0)
 | B_3 (3)
 | B_5 (5)
 | {m, n: nat} B_SUM (n+m) of (BEAUTIFUL m, BEAUTIFUL n)

 prfun three_is_beautiful () :<> BEAUTIFUL 3 = B_3

patscc complains “a termination metric is missing”. There is no need, but
I don’t bother am adding .<>. or alternatively, substituting prfn for
prfun:

 prfun three_is_beautiful () .<>. :<> BEAUTIFUL 3 = B_3
 prfn three_is_beautiful () :<> BEAUTIFUL 3 = B_3

Now it’s OK, although with this, it does not complain it’s not necessary
and .<>. should not be there:

 prfn three_is_beautiful () .<>. :<> BEAUTIFUL 3 = B_3

There is another strange point: why the :<>?

If I remove it:

 prfun three_is_beautiful () .<>. BEAUTIFUL 3 = B_3
 prfn three_is_beautiful () BEAUTIFUL 3 = B_3

patscc complains “pattern match is nonexhaustive”. How does :<> relates
to this? In the example, it’s supposed to mean the function is pure.

About this, another funny thing, is that if I use :<1> instead of :<>
or :<0>, this works, while :<1> means the function is not pure and has
“all effects, including everything we don’t know about yet”, at least
according to http://cs.likai.org/ats/ml-programmers-guide-to-ats

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Infragistics Professional
Build stunning WinForms apps today!
Reboot your WinForms applications with our WinForms controls. Build a
bridge from your legacy apps to the future.
http://pubads.g.doubleclick.net/gampad/clk?id=153845071&iu=/4140/ostg.clktrk
ats-lang-users mailing list
ats-lan...@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/ats-lang-users

2

Here is the proper way to do it:

prfn three_is_beautiful (): BEAUTIFUL 3 = B_3

Ah, yes of course: the : and the :<> are related (I should have
guessed)

which is equivalent to

prfun three_is_beautiful .<>. (): BEAUTIFUL 3 = B_3

About this, another funny thing, is that if I use :<1> instead of :<>

or :<0>, this works, while :<1> means the function is not pure and has
“all effects, including everything we don’t know about yet”,

‘is not pure and has effects’ → ‘may not be pure and may have
effects’

May… that indeed make a difference.

There is no need to add :<>; it is assumed here because ‘prfun’ is used.

If you add :<1>, then this function still typechecks but it cannot be
called in the body of another proof function.

I will remember of it Professor Xi :stuck_out_tongue: .

3

Here is the proper way to do it:

prfn three_is_beautiful (): BEAUTIFUL 3 = B_3

which is equivalent to

prfun three_is_beautiful .<>. (): BEAUTIFUL 3 = B_3

About this, another funny thing, is that if I use :<1> instead of :<>

or :<0>, this works, while :<1> means the function is not pure and has
“all effects, including everything we don’t know about yet”,

‘is not pure and has effects’ → ‘may not be pure and may have effects’

There is no need to add :<>; it is assumed here because ‘prfun’ is used.

If you add :<1>, then this function still typechecks but it cannot be
called in the body of another proof function.