Revenge of the Types

This is a very nice article showing some of the issues troubling python and the proposed type anotations.

I would summarize my view of the type annotation proposal as follows: Statically typed languages can introduce inference heuristics that minimize the amount of type declarations. They can "jump" into the dynamically typed world more easily. The other way around is a lot harder. Not only are all those type annotations lacking in the standard library and the tools around, but there is also a lack of function design by types.

Weird, it is enough on my machine (running ghc 7.6.3, unittyped 0.1), but unittyped does seem to use a lot of language extensions internally, it is seems possible that it would behave weirdly on different versions.

To answer the question of how it is possible, we can start by looking at the types. ":t" is a ghci command to show the type of an expression:

  ghci> :t 1
  1 :: Num a => a

This indicates that "1" can be any type that implements the "Num" typeclass.

Next, we want to determine what type "1" takes in the expression "1 meter". We can do this with:

  ghci> let a=1; b=a meter
  ghci> :t a
  a :: UnitTyped.Value Double LengthDimension Meter
     -> UnitTyped.Value
          Double
          ('UnitTyped.UnitCons
             * Length ('UnitTyped.Pos 'UnitTyped.One) 'UnitTyped.UnitNil)
          Meter

We can see that, in the expression "1 meter", "1" is actually a function. Looking at the source code [1], it seems like this is accomplished in a relativly hacky manner:

  instance (Fractional f, Convertable a b, t ~ Value f a b) => (Prelude.Num (Value f a b -> t)) where
	fromInteger i x = Prelude.fromInteger i . x
	(+) = error "This should not happen"
	(*) = error "This should not happen"
	abs = error "This should not happen"
	signum = error "This should not happen"

This works because the "+" being defined here is Prelude.+, not UnitTyped.NoPrelude.+ (which is defined seperatly).

[1] https://hackage.haskell.org/package/unittyped-0.1/docs/src/U...

People should be able to write on their blogs their thoughts. It's a really good way to learn, and to get feedback on your ideas.

Hopefully Armin listens to people who have been thinking about this for a long time, and done work in this area. But why should his ideas, which are admittedly uniformed, get spread wider than better ideas? This happens a lot anyway.

I don't think it's entirely positive when people rant when they don't have the knowledge to back it up. However, it can produce a reaction from other people to step up and argue their case better. Or even better, to put out their code. I think in this case Armin does have a bit of a clue, and this essay is informing himself, and others quite well.

You can statically check python with types now (pycharm pysonar2 etc), and you can use things like ABCs and interfaces to enforce constraints.

"Union types" and "intersection types" are the type systems people have used to statically type check python, and other dynamically typed languages. You can see the various types coming into or out of a function. This is what Armin is talking about with Option/Composite types.

So these various type systems which have been used to add extra type checking on top of python are now being blessed, and brought into the language proper.

There are plenty of places in Python where the types are not specified well, because mostly it doesn't matter to people using it. Since the type checking tools have added external type definitions, and fixed up inconsistencies outside of the python implementations. So Armin is pointing out a few examples of type inconsistencies within python. There are lots more. Especially at the C API level, where things are a bit weird. But they haven't really bothered people that much, so they haven't been fixed. As someone who has written C extensions for python, I can tell you that it is weird, and things have changed with every python release (even, and especially in the 2.x series).

However, these external type definitions are being brought together into the language (as per Guidos email) in the mypy format. There is a hope that the other definitions from tools like PyCharm can be translated automatically. These definitions are being used in useful tools today.

These external type definitions are in effect a specification of the types for the core language, the standard library, and even other popular libraries (like Django etc).

What came first the Duck or the specification of the Duck?

Absolutely - like the NoSQL guys don't realize that a DB enforcing a schema is helping you.

"I have seen no data to backup this claim which would override my personal experience"

There have been attempts at measuring the effect of type systems, see for example this excellent presentation for some references: http://www.slideshare.net/Felienne/putting-the-science-in-co.... One of the studies mentioned here does claim that, other things being equal, static typing helps find bugs quicker.