Dynamically Typed Languages (2009)

Re:Dynamically Typed Languages (2009) by groovy2shoes on Thursday August 21, 2014 @02:05PM (#8208710)

The "unityped" descriptor is not meant to be pejorative. It's an observation that, from a type-theoretic point of view every expression in an untyped language can be given the same type. In a dynamically checked language, the type is the sum of all possible dynamic types (in Lua, for example: [1]). In an unchecked language, the type can be something else (in BCPL, for example, it's simply word; in the untyped lambda calculus, it's function). It's important to note that, according to type theory, types are a syntactic feature, not a semantic one.

It's just an observation rather than a judgment, and -- again from a type-theoretic perspective -- it's true. It's nothing to be offended about!

Note that if you were to write a type checker for a unityped language, then every program would trivially type check. So, while technically accurate, the notion of a language being "unityped" is not very useful. It's more of an intellectual curiosity than anything.

[1]: https://github.com/LuaDist/lua/blob/lua-5.1/src/lobject.h#L5...

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by gw on Thursday August 21, 2014 @02:29PM (#8208851)

You may not mean it as a pejorative, but it's clear that Harper did, and so do those who adopt the term as a rhetorical device. I also have to question your use of the phrase "according to type theory". You are implying that there is a single type theory with a single view on the nature of types. I recommend the link I put in my previous comment.

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by tel on Thursday August 21, 2014 @04:19PM (#8209350)

Harper is frequently pejorative. He's also accurate. He has an agenda and it is difficult to interpret him unbiasedly without accounting for it. But if you achieve it then you realize you can no longer argue with the factual points he makes.

That said, it's a completely true point in the notion of "static-types-as-type-theory-defines-them" that dynamic typing is a mode of use of static typing which is completely captured in large (potentially infinite/anonymous) sums. Doing this gives dynamic languages a rich calculus.

Refusing to doesn't strip them of that calculus, it just declares that you're either not willing to use it or not willing to admit you're using it. Both of which are fine by me, but occasionally treated pejoratively because... well, it's not quite clear why you would do such a thing. There's benefit with no cost.

Then sometimes people extend this to a lack of clarity about why you don't adopt richer types. Here, at least, there's a clear line to cross as you begin to have to pay.

---

The "Church view" and "Curry view" are psychological—the Wikipedia article even stresses this! So, sure, you can take whatever view you like.

But at the end of the day type systems satisfy theories. Or they don't. That satisfaction/proof is an essential detail extrinsic to your Churchiness or Curritude.

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by groovy2shoes on Thursday August 21, 2014 @07:36PM (#8210236)

Can you elaborate a bit on what the benefits of embracing that calculus are? Or maybe provide some pointers? I'm having trouble imagining what utility there is in treating untyped languages as (uni)typed. I said in another comment that it's pretty much a useless notion, but I'm genuinely curious if I'm overlooking something.

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by tel on Thursday August 21, 2014 @07:53PM (#8210311)

Probably the best one I can think of is that it gives you a natural way of looking at gradual typing. Doing gradual typing well is still tough, but you can see it as an obvious consequence of the unityping argument.

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by groovy2shoes on Thursday August 21, 2014 @08:09PM (#8210347)

I see. Looks like I have some reading to do :) Thanks.

[ Parent | on HN ]

Re:Dynamically Typed Languages (2009) by groovy2shoes on Thursday August 21, 2014 @03:11PM (#8209073)

The article you linked makes little sense to me. They do mention Clojure's core.typed as an example of the "Curry perspective", as opposed to the "Church perspective", so I decided to check that out.

The core.typed user guide and it uses the same definition[1] of type that I'm familiar with from "Church" type theory. It even makes the same observation that Clojure is unityped! It seems to me that core.typed does not use a "different" type theory at all. Rather, it is a testament to the great extensibility of the Lisps that a type system can be bolted on as a library. Perhaps unfortunately, most languages are not so flexible.

[1]: https://github.com/clojure/core.typed/wiki/User-Guide#what-a...

P.S.: I re-read Harper's original unitype article, and it does seem pretty combative. I still don't consider the term pejorative myself. I dislike the term, but because of its lack of utility above any other reason.

[ Parent | on HN ]