# Can proof functions be overloaded?

**URL:** <https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76>\
**Category:** Google Group\
**Created:** [August 7, 2014, 11:21pm UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76 "2014-08-07T23:21:38Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [August 7, 2014, 11:21pm UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/1 "2014-08-07T23:21:38Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [August 8, 2014, 12:55am UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/2 "2014-08-08T00:55:05Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 8, 2014, 12:23am UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/3 "2014-08-08T00:23:41Z")

</div>

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](mailto: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.
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 8, 2014, 1:39am UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/4 "2014-08-08T01:39:06Z")

</div>

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](mailto: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?
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/91b9c97f-bb5a-4ad4-adde-29e1a024ca42%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/91b9c97f-bb5a-4ad4-adde-29e1a024ca42%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/91b9c97f-bb5a-4ad4-adde-29e1a024ca42%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 8, 2014, 12:56am UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/5 "2014-08-08T00:56:40Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [August 8, 2014, 1:34am UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/6 "2014-08-08T01:34:27Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [August 7, 2014, 11:41pm UTC](https://discourse.ats-lang.org/t/can-proof-functions-be-overloaded/76/7 "2014-08-07T23:41:12Z")

</div>

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](mailto: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.
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/1521d46c-c103-427e-bb2e-0e7faa34b6ce%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .