Source of Scala's Undeciability

[David Hagen]

Scala's type system is well known to be Turing complete. I am curious (for purely self-enrichment reasons, not feature-request reasons) what would have to be removed from Scala in order to make compilation decidable?

[Ken Scambler]

While I can't directly answer your question, Runar's blog post from 2011 has a clue: https://apocalisp.wordpress.com/2011/01/13/simple-ski-combinator-calculus-in-scalas-type-system/

Implementing the S, K and I combinators is sufficient for universal computation; their existence proves the Turing completeness of the type system.  Perhaps if you could somehow disallow at least one of the SKI expressions in the post, then presumably you would have something more limited.

On 5 September 2015 at 00:54, David Hagen <david...@gmail.com> wrote:

Scala's type system is well known to be Turing complete. I am curious (for purely self-enrichment reasons, not feature-request reasons) what would have to be removed from Scala in order to make compilation decidable?

--
You received this message because you are subscribed to the Google Groups "scala-debate" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-debate...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[atomly]

https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

atomly

[martin odersky]

On Tue, May 17, 2016 at 2:57 PM, atomly <ato...@gmail.com> wrote:
> https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/
>

Which, incidentally, will go away:

http://www.scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html

- Martin

Martin Odersky
EPFL and Lightbend

[David Hagen]

May I check that I understand this correctly: One way to obtain undecidable behavior in Scala is to use the expression T#A when T is not a concrete type. The SKI examples use T#A when T is itself an abstract type parameter/member (x#eval, eval#ap[x], etc.) and this is what will be disallowed in dotty.

[martin odersky]

On Tue, May 17, 2016 at 4:46 PM, David Hagen <david...@gmail.com> wrote:
> May I check that I understand this correctly: One way to obtain undecidable
> behavior in Scala is to use the expression T#A when T is not a concrete
> type. The SKI examples use T#A when T is itself an abstract type
> parameter/member (x#eval, eval#ap[x], etc.) and this is what will be
> disallowed in dotty.
>

Yes, precisely.

- Martin

> On Tuesday, May 17, 2016 at 9:37:29 AM UTC-4, Martin wrote:
>>
>> On Tue, May 17, 2016 at 2:57 PM, atomly <ato...@gmail.com> wrote:
>> >
>> > https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/
>> >
>>
>> Which, incidentally, will go away:
>>
>> http://www.scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html
>>
>> - Martin
>

> --
> You received this message because you are subscribed to the Google Groups
> "scala-debate" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to scala-debate...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.



--

Prof. Martin Odersky
LAMP/IC, EPFL

[David Hagen]

Is this the only source of undecidability in Scala or are their other features that can do this as well?

[Luke Vilnis]

Contravariance makes Java's type system undecidable, as per this paper: http://research.microsoft.com/pubs/64041/fool2007.pdf

I would imagine Scala has problems with this too?

--

[Paul Hudson]

Given Scala's referenced in the first paragraph and Martin was a reviewer of the paper, I think it's safe to say "yes"!

[Paul Hudson]

Oh foo, where's the "retrieve stupid email" feature when you need it. I retract my previous statement :(

[David Hagen]

I wonder if this is the same problem that Ceylon addresses when it restricts where contravariant types can occur. From the spec:

Furthermore, a type with a contravariant type parameter may only appear in a covariant position in an extended type, satisfied type, case type, or upper bound type constraint.
Note: this restriction exists to eliminate certain undecidable cases described in the paper Taming Wildcards in Java's Type System, by Tate et al.

[Luke Vilnis]

Yeah, this looks to be the same issue. Apparently you can implement a cycle-detection algorithm and avoid these cases so it shouldn't be a problem in practice.

I just tried in Scala 2.11 and it handles this issue:

trait IN[-U] {}
trait IC[X] extends IN[IN[IC[IC[X]]]] {}

Gives an error message of:

Error:(75, 12) class graph is not finitary because type parameter X is expansively recursive

  trait IC[X] extends IN[IN[IC[IC[X]]]] {}

           ^

So it looks like this is not a problem for Scala after all. Cool!

[martin odersky]

On Tue, May 17, 2016 at 9:11 PM, Luke Vilnis <lvi...@gmail.com> wrote:
> Contravariance makes Java's type system undecidable, as per this paper:
> http://research.microsoft.com/pubs/64041/fool2007.pdf
>
> I would imagine Scala has problems with this too?

No, that one was fixed (with the scheme proposed in the paper). But
there are other sources of undecidability analogous to F-sub.

- Martin