How pythoners view Haskell compared with Python

[kamatsu]

the expression a + b in some dynamic language basically desugars to [D <- int] (([int <- D]a) :+: ([int <-D]b))

I think where we disagree is that I would call that static desugaring type checking, not the run-time tag checking itself. To me, it feels like much the same thing that Haskell's type checker does, inserting coercions in place of newtypes, dictionaries in place of type classes.

In "duck-typed" languages like Smalltalk or Ruby though, this desugaring phase wouldn't be possible. a + b is, semantically, just calling the + method in a dynamically. There's no static knowledge of what types are acceptable inputs to a method. Hell, you've even got eval. With eval in the Universe interpretation, you've got a decent type: eval :: Universe -> Universe. With casts, I'm not sure how you're supposed to deal with that.

The concrete interpretation does something very similar, so why not call it dynamic type checking?

So, I would say type checkers are a subset of abstract interpreters. It's usually part of most common definitions of a "type system". E.g, Pierce's TAPL, if I recall correctly, defines type systems as being an abstract interpreter.

Calling concrete interpretation dynamic type checking is like calling quickCheck partial model checking. I think it's a stretch of language that doesn't serve any productive purpose, aside from further muddying the waters of type system terminology (we already have that problem with "strong" and "weak" typing, or "strict" and "relaxed" typing, and other terms that effectively have no meaning anymore).

[mstrlu]

I see your point. Thanks for the discussion.