This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Re: deconstruction of subtyping

3 replies
James Iry
Joined: 2008-08-19,
User offline. Last seen 1 year 23 weeks ago.
Oops, reply all.

On Thu, Jul 1, 2010 at 7:35 AM, James Iry <jamesiry [at] gmail [dot] com> wrote:
Determining totality, i.e. determining that a function is defined for all elements of the domain, is impossible for any Turing complete language.  That's the definition of the halting problem.  Statically determining if PF's isDefinedAt is 100% accurate is an equivalent problem - you can map a partial function into a function that returns an option so proving a PF is 100% accurate is the same as proving that option returning function is total.
So rather than saying that Scala "opted for runtime checking of the domain" it's more accurate to say that "Scala opted to be Turing complete with all that that implies."

On Thu, Jul 1, 2010 at 6:20 AM, Josh Suereth <joshua [dot] suereth [at] gmail [dot] com> wrote:

Theoretically though, you are right.  A Partial function is only available for some portion of the domain.   In that theoretical ideal world, you'd also want the compile to catch when you use the partial function on a portion of the domain where it is not defined.   Scala opted for runtime checking of the domain, so the only "enforcing" it could do is make sure you called "isDefinedAt" and that is less than useful.

Jesper Nordenberg
Joined: 2008-12-27,
User offline. Last seen 42 years 45 weeks ago.
Re: deconstruction of subtyping

Incorrect. For example, it's trivial to prove that "(x : Int) => 3" is
defined for all values of its domain. I think you meant it's impossible
to determine totality of all possible functions in a TC language.

/Jesper Nordenberg

James Iry skrev 2010-07-01 16:35:
> Oops, reply all.
>
> On Thu, Jul 1, 2010 at 7:35 AM, James Iry > wrote:
>
> Determining totality, i.e. determining that a function is defined
> for all elements of the domain, is impossible for any Turing
> complete language. That's the definition of the halting problem.
> Statically determining if PF's isDefinedAt is 100% accurate is an
> equivalent problem - you can map a partial function into a function
> that returns an option so proving a PF is 100% accurate is the same
> as proving that option returning function is total.
>
> So rather than saying that Scala "opted for runtime checking of the
> domain" it's more accurate to say that "Scala opted to be Turing
> complete with all that that implies."
>
>
> On Thu, Jul 1, 2010 at 6:20 AM, Josh Suereth
> > wrote:
>
>
> Theoretically though, you are right. A Partial function is only
> available for some portion of the domain. In that theoretical
> ideal world, you'd also want the compile to catch when you use
> the partial function on a portion of the domain where it is not
> defined. Scala opted for runtime checking of the domain, so
> the only "enforcing" it could do is make sure you called
> "isDefinedAt" and that is less than useful.
>
>

James Iry
Joined: 2008-08-19,
User offline. Last seen 1 year 23 weeks ago.
Re: deconstruction of subtyping
"It's impossible to determine totality of any possible function in a TC language using any computable function." Better?  Please allow me to roll my eyes and file under "pedantic."

On Thu, Jul 1, 2010 at 1:49 PM, Jesper Nordenberg <megagurka [at] yahoo [dot] com> wrote:
Incorrect. For example, it's trivial to prove that "(x : Int) => 3" is defined for all values of its domain. I think you meant it's impossible to determine totality of all possible functions in a TC language.

/Jesper Nordenberg

James Iry skrev 2010-07-01 16:35:
Oops, reply all.

On Thu, Jul 1, 2010 at 7:35 AM, James Iry <jamesiry [at] gmail [dot] com
<mailto:jamesiry [at] gmail [dot] com>> wrote:

   Determining totality, i.e. determining that a function is defined
   for all elements of the domain, is impossible for any Turing
   complete language.  That's the definition of the halting problem.
     Statically determining if PF's isDefinedAt is 100% accurate is an
   equivalent problem - you can map a partial function into a function
   that returns an option so proving a PF is 100% accurate is the same
   as proving that option returning function is total.

   So rather than saying that Scala "opted for runtime checking of the
   domain" it's more accurate to say that "Scala opted to be Turing
   complete with all that that implies."


   On Thu, Jul 1, 2010 at 6:20 AM, Josh Suereth
   <joshua [dot] suereth [at] gmail [dot] com <mailto:joshua [dot] suereth [at] gmail [dot] com>> wrote:


       Theoretically though, you are right.  A Partial function is only
       available for some portion of the domain.   In that theoretical
       ideal world, you'd also want the compile to catch when you use
       the partial function on a portion of the domain where it is not
       defined.   Scala opted for runtime checking of the domain, so
       the only "enforcing" it could do is make sure you called
       "isDefinedAt" and that is less than useful.




Jesper Nordenberg
Joined: 2008-12-27,
User offline. Last seen 42 years 45 weeks ago.
Re: deconstruction of subtyping

:) Even though there are functions for which totality can't be
determined, it would be very useful to have a totality checker which
could give the answer "total/partial/don't know" for any function given
to it as input. The hard part is minimizing the number of functions
falling into the "don't know" category.

/Jesper Nordenberg

James Iry skrev 2010-07-01 22:55:
> "It's impossible to determine totality of any possible function in a TC
> language using any computable function." Better? Please allow me to
> roll my eyes and file under "pedantic."
>
> On Thu, Jul 1, 2010 at 1:49 PM, Jesper Nordenberg > wrote:
>
> Incorrect. For example, it's trivial to prove that "(x : Int) => 3"
> is defined for all values of its domain. I think you meant it's
> impossible to determine totality of all possible functions in a TC
> language.
>
> /Jesper Nordenberg
>
> James Iry skrev 2010-07-01 16:35:
>
> Oops, reply all.
>
> On Thu, Jul 1, 2010 at 7:35 AM, James Iry
> >> wrote:
>
> Determining totality, i.e. determining that a function is
> defined
> for all elements of the domain, is impossible for any Turing
> complete language. That's the definition of the halting
> problem.
> Statically determining if PF's isDefinedAt is 100%
> accurate is an
> equivalent problem - you can map a partial function into a
> function
> that returns an option so proving a PF is 100% accurate is
> the same
> as proving that option returning function is total.
>
> So rather than saying that Scala "opted for runtime checking
> of the
> domain" it's more accurate to say that "Scala opted to be Turing
> complete with all that that implies."
>
>
> On Thu, Jul 1, 2010 at 6:20 AM, Josh Suereth
>
> >> wrote:
>
>
> Theoretically though, you are right. A Partial function
> is only
> available for some portion of the domain. In that
> theoretical
> ideal world, you'd also want the compile to catch when
> you use
> the partial function on a portion of the domain where it
> is not
> defined. Scala opted for runtime checking of the
> domain, so
> the only "enforcing" it could do is make sure you called
> "isDefinedAt" and that is less than useful.
>
>
>
>

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland