Can proof functions be overloaded?

[Yannick Duchêne]

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.

[Brandon Barker]

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

--
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/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com.

[Hongwei Xi]

No, overloading does not work here. You can have:

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:

[Yannick Duchêne]

Le vendredi 8 août 2014 02:23:41 UTC+2, gmhwxi a écrit :

No, overloading does not work here. You can have:

prfn is_beautiful
  {m:int | m==3 || m==5}
  (x: int(m)): BEAUTIFULE (m) =

  sif m == 3 then B_3 () else B_5 ()

So proof functions are indeed a special case.

Thanks for the notice.

 

[gmhwxi]

Proof functions can be overloaded. But in this case,
overloading cannot be resolved.

[Yannick Duchêne]

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?

[Hongwei Xi]

Overloading is resolved without using any type indices. Otherwise, it would be too complex.

--

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/91b9c97f-bb5a-4ad4-adde-29e1a024ca42%40googlegroups.com.