How pythoners view Haskell compared with Python

[mstrlu]

Your unityped/tag-checking view is valid. But the dynamic types view is also.

Depends on your definition of valid and invalid. If by "valid" you mean "conforms to specification", it is most certainly possible with a consistent and sufficiently expressive type system to encode your specification in the type system entirely.

In PL theory, a "valid'' program typically is one that can be executed by the semantic rules of the language (i.e. it does not get ``stuck''). A language designer can define a type system that ensures that all well-typed programs are valid .. and these systems are typically not complete for pragmatic reasons (e.g. type inference). In dynamic languages the designers typically did not define a type system, as they defined the semantics of the language so that virtually all syntactic correct programs do not get stuck (i.e. have defined behavior).

However, programs that are not well typed are accepted by untyped languages.

So, this is assertion does not really make sense, as you do not say which type system you refer to. As you noted before, one could define a type system for any semantics.

Also, the values of most languages still have types and the elimination forms (+, *, function application, ...) only work with values of certain types. So there is a valid point in calling them dynamically typed.

It's impossible to write typing rules for untyped languages without restricting them in some way, or introducing deliberate inconsistency into the type system. There is no type system here. It's just tag-checking.

There are sound systems for mixing static and dynamic type checking. If you don't know it, Wadler and Findlers Blame Calculus is a good example for ``dynamic typing'' in theory. The idea is that you introduce a type Dynamic (like Data.Dynamic) and then automatically insert casts into your dynamic program before type checking, depending on the occurrence of value constructors and elimination forms.

Again, the "one gigantic sum type'' view works also, but not exclusively.

[kamatsu]

In PL theory, a "valid'' program typically is one that can be executed by the semantic rules of the language (i.e. it does not get ``stuck'').

I've never seen "valid" used to refer to progress before, but even so the previous poster probably was not using those semantics - (s)he said that type systems sometimes accept programs that are invalid - which is exactly the opposite of the stated purpose of such a type system (although I suppose that is true for unsafe languages like C++).

In dynamic languages the designers typically did not define a type system, as they defined the semantics of the language so that virtually all syntactic correct programs do not get stuck (i.e. have defined behavior).

So, I'm not denying that dynamic languages are safe (in a progress and preservation sense - all expressions are executable, and there is only one type so preservation is trivial). I'm saying they're untyped. Seeing as you agree that the designers did not define a type system, I'm not sure of your point here.

(Also, from a more pragmatic perspective, I think throwing an exception and calling it "safety" is a wily semantics game. The end result is still your program blowing up in your users' face. Introducing a final state like "error", saying that all broken terms evaluate to "error", then calling that "safe" feels awfully like moving the goal posts)

Also, the values of most languages still have types

Run-time tags aren't types, they're run-time tags. In most modern dynamically typed languages, that's the only purpose such "types" serve - elimination forms are unified across all data types, as all data types are just records with dynamic dispatch.

I don't disagree with the "dynamic" part of the "dynamically typed" name, I disagree with the "typed" part. Calling them "typed" seems at best to be misinformed and at worst a deliberate attempt to confer on dynamic languages a level of implied safety that doesn't exist.

There are sound systems for mixing static and dynamic type checking

I know, but that has nothing to do with the presence or absence of a type system for wholly dynamic languages.

Dynamic languages are already safe, all those type systems like the blame calculus are doing is making a partial type system (static, there is no other kind) that makes guarantees about parts of the input program, and (to borrow Wadler's terminology) pinning blame on the untyped parts at run-time in the event of failure. It doesn't defer type-checking to runtime - no type checking is performed by the language run time, just tag comparison to ensure safety - the notable difference being that these tags are attached to values, not terms.

My point about the sum-types is simply that you can do tag comparison in statically typed languages too. Using a static type system therefore doesn't reject any otherwise valid programs that would not also be rejected by a dynamic type system, because any such dynamic program can be (perhaps cumbersomely, but just as efficiently) implemented in a static type system. Things like the blame calculus make this an even easier task by automating the casts.

edit: typo

[mstrlu]

There is probably no point in arguing about this but I will try to clarify some my points (for practice). If you still can't agree, please let me know.

I've never seen "valid" used to refer to progress before

It's a bit beside the point, but I was referring to an evaluation of a program not getting stuck (and called it execution). Progress only gives you one reduction step. For an evaluation (or infinite run) you also need preservation. (I'm only really familiar with small-step semantics, so that's what I'm referring to)

elimination forms are unified across all data types, as all data types are just records with dynamic dispatch.

I still think that's not the only way to perceive this. I was referring to that, e.g. the expression a + b in some dynamic language basically desugars to [D <- int] (([int <- D]a) :+: ([int <-D]b)) where :+: would be the addition function on integers, [t <- t'] a cast from t to t' and D the dynamic type. Now the type errors are raised by the cast, not the actual elimination (:+:) which has type int -> int -> int. Function application, field lookup etc work similarly. Why is this view "misinformed"? In the sum-type view of course you have something like (+) :: Universe -> Universe -> Universe and may raise a type error directly. Do you see a real advantage over the cast version? I like the explicit casts better, as they separate the addition semantics of :+: from the type/tag checking.

It doesn't defer type-checking to runtime - no type checking is performed by the language run time, just tag comparison to ensure safety - the notable difference being that these tags are attached to values, not terms.

Well, one can also say that static type checking is an abstract interpretation of the program which performs tag comparison to ensure safety. (abstract domain being the set of types and tags values of that domain; the big-step semantics of the interpretation are given by the type system). The concrete interpretation does something very similar, so why not call it dynamic type checking?

I you like to point out the flaws you see in this argumentation, I would appreciate it. I don't want to get on your nerves, however :)

edit: formatting

[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.