Can proof functions be overloaded? Or alternatively, do I really understand
what overloading means in ATS context? To me, an overloaded function is a
function of the same name as another, but with a different type (the type
may include the return type or not, depending on the language).
I’m still playing with the Beautiful example, and wanted to try this:
dataprop
BEAUTIFUL
(int)
= B_0 (0)
| B_3 (3)
| B_5 (5)
| {m, n: nat}
B_SUM (n + m)
of (BEAUTIFUL m, BEAUTIFUL n)
prfn
is_beautiful
{m: nat | m == 3}
(x: int (m))
: BEAUTIFUL m
= B_3 ()
prfn
is_beautiful
{m: nat | m == 5}
(x: int (m))
: BEAUTIFUL m
= B_5 ()
prfn
eight_is_beautiful
{m, n: nat | m == 3; n == 5}
(x: int (m), y: int (n))
: BEAUTIFUL (m + n)
= B_SUM
(is_beautiful x,
is_beautiful y)
The point here, is the two proof functions named is_beautiful. To my
understanding of overloading, both forms an overloading of the name is_beautiful, but patscc complains the third function is left with
unsolved constraints. When both function have different names, the third
proof function type‑checks.
I’m not able to guess if my issue is that it’s not an overloading as I
believe or if it’s that there are limitation(s) with proof function
overloading.
prfn is_beautiful
{m:int | m==3 || m==5}
(x: int(m)): BEAUTIFULE (m) =
sif m == 3 then B_3 () else B_5 ()On Thu, Aug 7, 2014 at 7:21 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Can proof functions be overloaded? Or alternatively, do I really
understand what overloading means in ATS context? To me, an overloaded
function is a function of the same name as another, but with a different
type (the type may include the return type or not, depending on the
language).
I’m still playing with the Beautiful example, and wanted to try this:
dataprop
BEAUTIFUL
(int)
= B_0 (0)
| B_3 (3)
| B_5 (5)
| {m, n: nat}
B_SUM (n + m)
of (BEAUTIFUL m, BEAUTIFUL n)
prfn
is_beautiful
{m: nat | m == 3}
(x: int (m))
: BEAUTIFUL m
= B_3 ()
prfn
is_beautiful
{m: nat | m == 5}
(x: int (m))
: BEAUTIFUL m
= B_5 ()
prfn
eight_is_beautiful
{m, n: nat | m == 3; n == 5}
(x: int (m), y: int (n))
: BEAUTIFUL (m + n)
= B_SUM
(is_beautiful x,
is_beautiful y)
The point here, is the two proof functions named is_beautiful. To my
understanding of overloading, both forms an overloading of the name is_beautiful, but patscc complains the third function is left with
unsolved constraints. When both function have different names, the third
proof function type‑checks.
I’m not able to guess if my issue is that it’s not an overloading as I
believe or if it’s that there are limitation(s) with proof function
overloading.
Overloading is resolved without using any type indices. Otherwise, it would
be too complex.On Thu, Aug 7, 2014 at 9:34 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Le vendredi 8 août 2014 02:56:40 UTC+2, gmhwxi a écrit :
Proof functions can be overloaded. But in this case,
overloading cannot be resolved.
Why? The type are different and there is no ambiguity (to my eyes), the
constraints are not the same. Or does it means there is some aspect of
types which are not counted when solving overloading?
Proof functions can be overloaded. But in this case,
overloading cannot be resolved.On Thursday, August 7, 2014 8:55:06 PM UTC-4, Yannick Duchêne wrote:
Le vendredi 8 août 2014 02:23:41 UTC+2, gmhwxi a écrit :
Proof functions can be overloaded. But in this case,
overloading cannot be resolved.
Why? The type are different and there is no ambiguity (to my eyes), the
constraints are not the same. Or does it means there is some aspect of
types which are not counted when solving overloading?
I tried adding this before your is_beautiful functions to introduce a
symbolic overloaded function name:
symintr is_beautiful
then these after the respective prfuns:
overload is_beautiful with is_beautiful1 of 10
overload is_beautiful with is_beautiful2 of 20
But still it could not resolve the type differences =(.
That said, I’m not at all very familiar with ATS/LF, and there may be other
specific syntax to be used in this case.
Brandon Barker
brandon…@gmail.comOn Thu, Aug 7, 2014 at 7:21 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Can proof functions be overloaded? Or alternatively, do I really
understand what overloading means in ATS context? To me, an overloaded
function is a function of the same name as another, but with a different
type (the type may include the return type or not, depending on the
language).
I’m still playing with the Beautiful example, and wanted to try this:
dataprop
BEAUTIFUL
(int)
= B_0 (0)
| B_3 (3)
| B_5 (5)
| {m, n: nat}
B_SUM (n + m)
of (BEAUTIFUL m, BEAUTIFUL n)
prfn
is_beautiful
{m: nat | m == 3}
(x: int (m))
: BEAUTIFUL m
= B_3 ()
prfn
is_beautiful
{m: nat | m == 5}
(x: int (m))
: BEAUTIFUL m
= B_5 ()
prfn
eight_is_beautiful
{m, n: nat | m == 3; n == 5}
(x: int (m), y: int (n))
: BEAUTIFUL (m + n)
= B_SUM
(is_beautiful x,
is_beautiful y)
The point here, is the two proof functions named is_beautiful. To my
understanding of overloading, both forms an overloading of the name is_beautiful, but patscc complains the third function is left with
unsolved constraints. When both function have different names, the third
proof function type‑checks.
I’m not able to guess if my issue is that it’s not an overloading as I
believe or if it’s that there are limitation(s) with proof function
overloading.