Another non-argument in type systems

http://tratt.net/laurie/tech_articles/articles/another_non_argument_in_type_systems

by ltratt • 14 years ago

15 5 14 years ago

lmm• 14 years ago

Sure, having dynamic multityping allows one to express things that one cannot express in a dynamically unityped language. But I think the original point stands - a language with static multityping and dynamic multityping (not all staticly typed languages provide the latter, and they certainly don't all make it easy) is more expressive than one with static unityping and dynamic multityping.

ltratt• 14 years ago

If you have a static type system and it's sound, it'll reject some programs that would execute without type errors, whereas a dynamically typed language will allow such programs to execute: it's what I called "dynamic expressivity". That's why saying "more expressive" without qualifying whether one is considering "static" or "dynamic" is problematic.

vlasta2• 14 years ago

I believe the example ("abc" + 123) given in the article is not 100% correct. Let's take C++ as a statically typed language and define a custom class MegaType. Then, in the whole program, we may use only variables of this single type. Any program can be trivially transformed to use just this single type. The piece of code would then look like MegaType("abc") + MegaType(123). When executed, it would behave exactly as a language with dynamic types. So, a dynamically typed language really is a specialization of statically typed language - you only need to define and use this one MegaType and implement all needed operators for this type (and they may of course work differently in runtime: "123" + 123 may result in 246 if you decide it should).

chalst• 14 years ago

> The following program (in pseudo-Python) shows a program which will fail to type check in any sound static type system which I know of ...

I think (haven't checked) that the equivalent of that code will type just fine in Typed Scheme [1] and this kind of type system has been studied since the 70s as intersection types and have found a fair amount of application in type systems for compiler intermediate representations (because they fit well with optimisations involving type specialisation).

He's quite right to say that you can always find such untypeable examples for static type systems that are reasonable (esp. that they have an acceptable complexity for type inference).

[1] http://www.ccs.neu.edu/home/samth/typed-scheme/

noblethrasher• 14 years ago

The concept of of a sum type is simple. It's just the type-theoretic notion of logical disjunction, how a particular language expresses that is sort of high-level implementation detail.

Java and its ilk do have sum types: they're called abstract classes; the derived types are the variants.

In C# (and probably Java) you can easily define both open and closed sum types simply by marking the base class constructor as either `public` or `protected`.

Another non-argument in type systems

Related Stories