Source of Scala's Undeciability

413 views
Skip to first unread message

David Hagen

unread,
Sep 4, 2015, 10:54:33 AM9/4/15
to scala-debate
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

unread,
Nov 19, 2015, 4:17:03 AM11/19/15
to David Hagen, scala-debate
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

unread,
May 17, 2016, 8:58:06 AM5/17/16
to Ken Scambler, David Hagen, scala-debate

martin odersky

unread,
May 17, 2016, 9:37:29 AM5/17/16
to atomly, Ken Scambler, David Hagen, scala-debate
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

unread,
May 17, 2016, 10:46:37 AM5/17/16
to scala-debate, ato...@gmail.com, ken.sc...@gmail.com, david...@gmail.com, martin....@epfl.ch
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

unread,
May 17, 2016, 11:06:37 AM5/17/16
to David Hagen, scala-debate, atomly lee, Ken Scambler
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

unread,
May 17, 2016, 2:32:18 PM5/17/16
to scala-debate, david...@gmail.com, ato...@gmail.com, ken.sc...@gmail.com, martin....@epfl.ch
Is this the only source of undecidability in Scala or are their other features that can do this as well?

Luke Vilnis

unread,
May 17, 2016, 3:11:44 PM5/17/16
to David Hagen, scala-debate, ato...@gmail.com, Ken Scambler, martin....@epfl.ch
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

unread,
May 17, 2016, 3:34:56 PM5/17/16
to Luke Vilnis, David Hagen, scala-debate, ato...@gmail.com, Ken Scambler, martin odersky
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

unread,
May 17, 2016, 3:36:26 PM5/17/16
to Luke Vilnis, David Hagen, scala-debate, ato...@gmail.com, Ken Scambler, martin odersky
Oh foo, where's the "retrieve stupid email" feature when you need it. I retract my previous statement :(

David Hagen

unread,
May 17, 2016, 3:38:57 PM5/17/16
to scala-debate, david...@gmail.com, ato...@gmail.com, ken.sc...@gmail.com, martin....@epfl.ch
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

unread,
May 17, 2016, 3:42:01 PM5/17/16
to David Hagen, scala-debate, ato...@gmail.com, Ken Scambler, martin....@epfl.ch
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

unread,
May 17, 2016, 3:43:20 PM5/17/16
to Luke Vilnis, David Hagen, scala-debate, atomly lee, Ken Scambler
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
Reply all
Reply to author
Forward
0 new messages