(no) class (on) LaborDay extends Weekend

[tiedyedave]

This weekend was a non-uniform mixture of doing work, not doing work, and contemplation of each. Followed, of course, by barbecue today.

My social circle seems to have stopped expanding for the moment. Hopefully it will start growing again soon as I become more comfortable here. Which is weird, because I was very comfortable a couple of weeks ago just before classes started, so much so that Dr. Priebe (who is in charge of the 398T immigration-esque course) thought that I was either not a first-year, or that I had been an undergrad at UT, since I already seemed so well-adjusted. And then I kind of lost that.

For any of you PL-interested people: If you would like to explore a new language, try Scala. You have my testimony as a PL weenie that this language is T3H H0TT. It has the most powerful static type system I've seen to date; it beats {SML, OCaml, Haskell} like redheaded stepchildren.

Comments

[jcreed.livejournal.com]

Interesting, but its type-inference-fu is weak. ML challenge you to a fight! You will face the wrath of its Hindley-Milner style!

[tiedyedave]

I think it's "weak" (i.e. local) out of necessity. If adding the occasional type annotation also gives me the power to specify covariance/contravariance, type constraints, and view bounds, then so be it. Besides, ML's "full" type inference itself is weak in the sense that using signatures in the module system is tantamount to adding type ascriptions; they just all happen to be in the same place.

[jcreed.livejournal.com]

Good point. I still don't see why I should need to add any annotations to, say, factorial, which my brief skim of the documentation suggested that I need to. Am I wrong?

Anyway, I just wanted to construe type-checkers engaged in an eternal ninja battle.

[tiedyedave]

I assume you mean:


def fac(n: Int) = if (n == 0) 1 else n * fac(n - 1);


Yes, that seems suspicious to me too. I haven't yet been able to discern why one could not incorporate such inference into the checker. I assume it is because of situations more complicated than this, which I suspect might arise if one were dealing with arguments and return types that are subject to more constraints than Int is. :-)

I'll see if I can locate or invent an example.

[tiedyedave]

The short answer:

From "Local Type Inference" [Pierce,Turner 1998]
"In particular, we are concerned with languages whose type-theoretic core combines subtyping and impredicative polymorphism in the style of System F. This combination of features places us in the realm of partial type inference methods, since complete type inference for impredicative polymorphism alone is already known to be undecidable, and the addition of subtyping does not seem to make the problem any easier. (For the combination of subtyping with Hinley/Milner-style polymorphic type inference, promising results have recently been reported [list of citations], but practical checkers based on these results have yet to see widespread use.)"

The list of citations at the end includes at least one paper with Odersky as a co-author, and since Odersky is master and commander of Scala (i.e. he appears on every single Scala paper at all ever), I would assume that there is good reason why local type inference is as far as Scala goes.

Thanks for the challenge, by the way; I have at least four new papers to digest now, including Odersky's own "A Nominal Theory of Objects with Dependent Types" and "Colored Local Type Inference". Makes me wish I had taken a graduate type theory course at CMU, oh well.

[dr4b]

i dunno about the rest, dave, but i love your subject line!

[tiedyedave]

Thanks :-)

[ikeepaleopard]

The fact that there's an abstract base class that descends from java.lang.Object makes me sad. The regular expression pattern matching looks pretty cool. The object model looks confusing at least to my simple java mind. Also, it seems like keeping track of covariance and contravariance declarations would be complicated, but it also seems like it could be a good solution to the differentiating between mutable and immutable types.

[tiedyedave]

As I understand it, descending from java.lang.Object is for interoperability reasons; it doesn't mean that Scala is actually constrained to follow the stupidities of the Java object model. It's sad in the sense that java.lang.Object is sad, but it's also fortunate because this makes it easier to hoist Java programmers up into a strictly superior language, and engulf Java legacy code (slowly digesting and purifying it until only decent code remains).