Before I get to the proof, what does this mean?<\/p>\n
A system is Turing complete when it can perform any<\/em> possible computation that could be performed on any other computing device. The Turing machine is, obviously, Turing complete. So is lambda calculus, the Minsky machine, the Brainfuck computing model, and the Scala programming language itself.<\/p>\n If type inference is Turing complete, then that means that you can write a Scala program where, in order to type-check the program, the compiler has to run an arbitrary program to completion. It means that there are, at least theoretically, Scala programs where the compiler will take forever – literally forever<\/em> – to determine whether or not a given program contains a type error. Needless to say, I consider this to be a bad thing. Personally, I’d really prefer to see the type system be less flexible. In fact, I’d go so far as to say that this is a fundamental error in the design of Scala, and a big strike against it as a language. Having a type-checking system which isn’t guaranteed to terminate is bad. <\/p>\n But let’s put that aside: Scala is pretty entrenched in the community that uses it, and they’ve accepted this as a tradeoff. How did the blog author, Michael D\u00fcrig, prove that Scala type checking is Turing complete? By showing how to implement a variant of lambda calculus called SKI combinator calculus entirely with types.<\/p>\n SKI calculus is seriously cool. We know that lambda calculus is Turing complete. It turns out that for any lambda calculus expression, there’s a way rewriting it without any variables, and without any lambdas at all, using three canonical master functions. If you’ve got those three, then you can write anything, anything at all<\/em>. The three are called S, K, and I.<\/p>\n They come from intuitionistic logic, where they’re fundamental axioms that describe how intuitionistic implication works. K is the rule Given any lambda calculus expression, you can rewrite it as a chain of SKIs. (If you’re interested in seeing how, please just ask in the comments; if enough people are interested, I’ll write it up.) What the author of the post id is show how to implement the S, K, and I combinators in Scala types. <\/p>\n He’s created a type He implements the S, K, and I combinators as traits that extend The apply “method” of So if have any type A, if you write something like The It's written in curried form, so it's a type trait The implementation is a whole lot trickier, but it's the same basic mechanics. Applying The Michid then goes on to show examples of how to use these beasts. He implements equality testing, and then shows how to test if different type-expressions evaluate to the same thing. And all of this happens at compile time<\/em>. If the equality test fails, then it's a type error at compile time!<\/p>\n It's a brilliant little proof. Even if you can't read Scala syntax, and you don't really understand Scala type inference, as long as you know SKI, you can look at the equality comparisons, and see how it works in SKI. It's really beautiful. <\/p>\n","protected":false},"excerpt":{"rendered":" Over the weekend, a couple of my Foursquare coworkers and I were chatting on twitter, and one of my smartest coworkers, a great guy named Jorge Ortiz, pointed out that type inference in Scala (the language we use at Foursquare, and also pretty much my favorite language) is Turing complete. Somehow, I hadn’t seen this […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[7,32],"tags":[],"class_list":["post-2004","post","type-post","status-publish","format-standard","hentry","category-bad-software","category-lambda-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-wk","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/2004","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=2004"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/2004\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=2004"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=2004"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=2004"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n
\ntrait Term {\n type ap[x <: Term] <: Term\n type eval <: Term\n}\n<\/pre>\nTerm<\/code>, which is the supertype of any computable fragment written in this type-SKI. Since everything is a function, all terms have to have two methods: one of them is a one-parameter “function” which applies the term to a parameter, and the second is a “function” which simplifies the term into canonical form.<\/p>\nTerm<\/code>. We’ll start with the simplest one, the I<\/code> combinator.<\/p>\n\ntrait I extends Term {\n type ap[x <: Term] = I1[x]\n type eval = I\n}\n\ntrait I1[x <: Term] extends Term {\n type ap[y <: Term] = eval#ap[y]\n type eval = x#eval\n}\n<\/pre>\nI<\/code> needs to take a parameter, so its apply type-function takes a parameter x<\/code>, and returns a new type I1[x]<\/code> which has the parameter encoded into it. Evaluating I1[x]<\/code> does exactly what you’d want from the I<\/code> combinator with its parameter – it returns it.<\/p>\nI1<\/code> looks strange. What you have to remember is that in lambda calculus (and in the SKI combinator calculus), everything is a function – so even after evaluating var a : I.ap[A].eval<\/code>, the type of a<\/code> will evaluate to A<\/code>. If you apply I.ap[A].ap[Z]<\/code>, it’s equivalent to taking the result of evaluating I.ap[A]<\/code>, giving you A<\/code>, and then applying that to Z<\/code>.<\/p>\nK<\/code> combinator is much more interesting:<\/p>\n\n\/\/ The K combinator\ntrait K extends Term {\n type ap[x <: Term] = K1[x]\n type eval = K\n}\n\ntrait K1[x <: Term] extends Term {\n type ap[y <: Term] = K2[x, y]\n type eval = K1[x]\n}\n\ntrait K2[x <: Term, y <: Term] extends Term {\n type ap[z <: Term] = eval#ap[z]\n type eval = x#eval\n}\n<\/pre>\nK<\/code>, which returns a type trait K1<\/code>, which takes a parameter and returns a type trait K2<\/code>.<\/p>\nK.ap[X]<\/code> gives you K1[X]<\/code>. Applying that to Y<\/code> with K1[X].ap[Y]<\/code> gives you K2[K, Y]<\/code>. Evaluating that gives you S<\/code> combinator is more of the same.<\/p>\n\n\/\/ The S combinator\ntrait S extends Term {\n type ap[x <: Term] = S1[x]\n type eval = S\n}\n\ntrait S1[x <: Term] extends Term {\n type ap[y <: Term] = S2[x, y]\n type eval = S1[x]\n}\n\ntrait S2[x <: Term, y <: Term] extends Term {\n type ap[z <: Term] = S3[x, y, z]\n type eval = S2[x, y]\n}\n\ntrait S3[x <: Term, y <: Term, z <: Term] extends Term {\n type ap[v <: Term] = eval#ap[v]\n type eval = x#ap[z]#ap[y#ap[z]]#eval\n}\n\n\n<\/pre>\n