Source of Scala's Undeciability

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

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?

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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 <[hidden email]> 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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

atomly

atomly

On Thu, Nov 19, 2015 at 3:17 AM, Ken Scambler <[hidden email]> wrote:
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 <[hidden email]> 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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

martin odersky-2
On Tue, May 17, 2016 at 2:57 PM, atomly <[hidden email]> 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

> atomly
>
> On Thu, Nov 19, 2015 at 3:17 AM, Ken Scambler <[hidden email]>
> wrote:
>>
>> 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 <[hidden email]> 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 [hidden email].
>>> For more options, visit https://groups.google.com/d/optout.
>>
>>
>> --
>> 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 [hidden email].
>> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> 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 [hidden email].
> For more options, visit https://groups.google.com/d/optout.



--

Martin Odersky
EPFL and Lightbend

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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.

On Tuesday, May 17, 2016 at 9:37:29 AM UTC-4, Martin wrote:
On Tue, May 17, 2016 at 2:57 PM, atomly <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="HSHheSy_DQAJ" rel="nofollow" onmousedown="this.href=&#39;javascript:&#39;;return true;" onclick="this.href=&#39;javascript:&#39;;return true;">ato...@...> wrote:
> <a href="https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/" target="_blank" rel="nofollow" onmousedown="this.href=&#39;https://www.google.com/url?q\x3dhttps%3A%2F%2Fmichid.wordpress.com%2F2010%2F01%2F29%2Fscala-type-level-encoding-of-the-ski-calculus%2F\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHiHsRfdKOmK0dIf_L0CwfhiBGl9A&#39;;return true;" onclick="this.href=&#39;https://www.google.com/url?q\x3dhttps%3A%2F%2Fmichid.wordpress.com%2F2010%2F01%2F29%2Fscala-type-level-encoding-of-the-ski-calculus%2F\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHiHsRfdKOmK0dIf_L0CwfhiBGl9A&#39;;return true;">https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/
>

Which, incidentally, will go away:

  <a href="http://www.scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html" target="_blank" rel="nofollow" onmousedown="this.href=&#39;http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.scala-lang.org%2Fblog%2F2016%2F02%2F17%2Fscaling-dot-soundness.html\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNEAPilk20GP1ZGAfGxCkb15TTLyog&#39;;return true;" onclick="this.href=&#39;http://www.google.com/url?q\x3dhttp%3A%2F%2Fwww.scala-lang.org%2Fblog%2F2016%2F02%2F17%2Fscaling-dot-soundness.html\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNEAPilk20GP1ZGAfGxCkb15TTLyog&#39;;return true;">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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

Martin Odersky
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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 <[hidden email]> 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 [hidden email].
> For more options, visit https://groups.google.com/d/optout.



--
Prof. Martin Odersky
LAMP/IC, EPFL

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="Nj_N1AnEDQAJ" rel="nofollow" onmousedown="this.href=&#39;javascript:&#39;;return true;" onclick="this.href=&#39;javascript:&#39;;return true;">david...@...> 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

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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?

On Tue, May 17, 2016 at 2:32 PM, David Hagen <[hidden email]> wrote:
Is this the only source of undecidability in Scala or are their other features that can do this as well?

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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"!

On 17 May 2016 at 20:11, Luke Vilnis <[hidden email]> 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?

On Tue, May 17, 2016 at 2:32 PM, David Hagen <[hidden email]> wrote:
Is this the only source of undecidability in Scala or are their other features that can do this as well?

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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

On 17 May 2016 at 20:34, Paul Hudson <[hidden email]> wrote:
Given Scala's referenced in the first paragraph and Martin was a reviewer of the paper, I think it's safe to say "yes"!

On 17 May 2016 at 20:11, Luke Vilnis <[hidden email]> 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?

On Tue, May 17, 2016 at 2:32 PM, David Hagen <[hidden email]> wrote:
Is this the only source of undecidability in Scala or are their other features that can do this as well?

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.


--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

David Hagen
In reply to this post by Luke Vilnis
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.


On Tuesday, May 17, 2016 at 3:11:44 PM UTC-4, Luke Vilnis wrote:
Contravariance makes Java's type system undecidable, as per this paper: <a href="http://research.microsoft.com/pubs/64041/fool2007.pdf" target="_blank" rel="nofollow" onmousedown="this.href=&#39;http://www.google.com/url?q\x3dhttp%3A%2F%2Fresearch.microsoft.com%2Fpubs%2F64041%2Ffool2007.pdf\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHgTQb7aOcghvi2juvz2IzgCv2XKA&#39;;return true;" onclick="this.href=&#39;http://www.google.com/url?q\x3dhttp%3A%2F%2Fresearch.microsoft.com%2Fpubs%2F64041%2Ffool2007.pdf\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNHgTQb7aOcghvi2juvz2IzgCv2XKA&#39;;return true;">http://research.microsoft.com/pubs/64041/fool2007.pdf

I would imagine Scala has problems with this too?

On Tue, May 17, 2016 at 2:32 PM, David Hagen <<a href="javascript:" target="_blank" gdf-obfuscated-mailto="F5cz7GnRDQAJ" rel="nofollow" onmousedown="this.href=&#39;javascript:&#39;;return true;" onclick="this.href=&#39;javascript:&#39;;return true;">david...@...> wrote:
Is this the only source of undecidability in Scala or are their other features that can do this as well?

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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

--
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 <a href="javascript:" target="_blank" gdf-obfuscated-mailto="F5cz7GnRDQAJ" rel="nofollow" onmousedown="this.href=&#39;javascript:&#39;;return true;" onclick="this.href=&#39;javascript:&#39;;return true;">scala-debate...@googlegroups.com.
For more options, visit <a href="https://groups.google.com/d/optout" target="_blank" rel="nofollow" onmousedown="this.href=&#39;https://groups.google.com/d/optout&#39;;return true;" onclick="this.href=&#39;https://groups.google.com/d/optout&#39;;return true;">https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

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!




On Tue, May 17, 2016 at 3:38 PM, David Hagen <[hidden email]> wrote:
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.


On Tuesday, May 17, 2016 at 3:11:44 PM UTC-4, Luke Vilnis 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?

On Tue, May 17, 2016 at 2:32 PM, David Hagen <[hidden email]> wrote:
Is this the only source of undecidability in Scala or are their other features that can do this as well?

On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.
Reply | Threaded
Open this post in threaded view
|

Re: Source of Scala's Undeciability

Martin Odersky
In reply to this post by Luke Vilnis
On Tue, May 17, 2016 at 9:11 PM, Luke Vilnis <[hidden email]> 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

>
> On Tue, May 17, 2016 at 2:32 PM, David Hagen <[hidden email]> wrote:
>>
>> Is this the only source of undecidability in Scala or are their other
>> features that can do this as well?
>>
>> On Tuesday, May 17, 2016 at 11:06:37 AM UTC-4, martin odersky wrote:
>>>
>>> On Tue, May 17, 2016 at 4:46 PM, David Hagen <[hidden email]> 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
>>
>> --
>> 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 [hidden email].
>> For more options, visit https://groups.google.com/d/optout.
>
>
> --
> 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 [hidden email].
> For more options, visit https://groups.google.com/d/optout.



--
Prof. Martin Odersky
LAMP/IC, EPFL

--
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 [hidden email].
For more options, visit https://groups.google.com/d/optout.