- About Scala
- Documentation
- Code Examples
- Software
- Scala Developers

# Re: deconstruction of subtyping

Thu, 2010-07-01, 15:35

Oops, reply all.

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

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.

Thu, 2010-07-01, 22:07

#2
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:

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.

Thu, 2010-07-01, 22:17

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

>

>

>

>

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.

>

>