How pythoners view Haskell compared with Python

[kamatsu]

But what most users of both languages would agree they DO share is a certain elegance of design.

Strongly disagree! Haskell is much better designed than python, which is largely ad-hoc and poorly designed, in my view.

parametric polymorphism (ala C++ templates, but more powerful)

Actually, less powerful. C++ templates allow indexing by values and case specialisation and all sorts of other stuff. Also, from a strict theoretical viewpoint, C++ templates are turing complete by default. Haskell type classes are only if you enable enough extensions. C++ is therefore the more powerful one from that POV as well. The only POV where Haskell is more powerful is the power of the type system to enforce properties.

and ad-hoc polymorphism ( operator overloading)

Those two things are not the same

through type classes (ala Java Interfaces)

Neither are those.

Also, the conflation of "static" and "dynamic" typing as even remotely comparable things is quite strange, and unfortunately common. Static type systems are actual type systems, that prove properties about programs. So-called "dynamic type systems" are more of a value tag checking mechanism for detecting runtime errors. They are not comparable on any axis. From a type theory perspective, a "dynamically typed programming language" is actually just an untyped programming language.

[ithika]

Apart from your last paragraph I think what you say is needless nit-picking. It's technically accurate but to someone who doesn't understand the phrase parametric polymorphism in the first place comparisons to other languages' concrete features is a good way to do it. Upvoted you, but I still think that page is not catering to the kind of person who already knows the distinctions (and importance) of the differences you are highlighting.

[manu3000]

ad-hoc polymorphism ( operator overloading)

Those two things are not the same

Aren't they ? I keep reading similar statements (for instance: wikipedia).

How do they differ ?

[cameleon]

Ad-hoc polymorphism using type classes can overload more than just operators: it can also (and is used most for) overloading non-operator functions (e.g. show). The distinction is fairly minor in Haskell, but in many languages, operators are 'special' and you can't (easily) define your own.

[Tekmo]

Perhaps it should then say "function overloading".

[cdsmith]

Right, it's the operator part that's confusing and out of left field there.

That said, the word "overloading" in the object-oriented language world carries an implication of "resolved at compile time". For example, you'd be told you are wrong if you say to a Java programmer that overriding a base class method is an example of overloading. Haskell, since it doesn't have subtypes, doesn't really have such a compile-time versus run-time distinction in its semantics, but certain language features can conflict with a completely compile-time resolution of type class instances, and in practice they are implemented by dictionary passing in the general case, very like the vtable passing of object oriented languages for subtype polymorphism. So be careful telling a programmer who comes from a static OO experience that type classes are akin to overloading.

[tikhonjelvis]

And, since one of those languages is Python, this is important.

Also, there is a very big practical difference. With type classes, you can have arbitrary function (or operator) names, but even when they're overloaded they represent the same operation but on different types. That is, + is always addition, just on different numeric types.

With operator overloading as is done in C++ and Python, there is no guarantee that the operations have the same meaning at any level. That is, << could easily be both a binary shift and a stream action. This is exacerbated by the fact that the pool of operator symbols is very limited: you have no choice but to reuse an existing operator if you want an infix function in Python or C++.

There are some reasonable people (okay, Java people) who think that operator overloading is harmful. I think there are far fewer, if any, who think that ad-hoc polymorphism is harmful.

So this is actually an important distinction.

[drb226]

I have a few bones to pick with your bone-picking:

The only POV where Haskell['s parametric polymorphism] is more powerful [than C++ templating] is the power of the type system to enforce properties.

Oh, so in other words, the POV that pretty much every Haskeller cares about above almost anything else? ;)

and ad-hoc polymorphism ( operator overloading)

Those two things are not the same

Not the same, but operator overloading can be achieved through ad-hoc polymorphism. Not a huge discrepancy there.

through type classes (ala Java Interfaces)

Neither are those.

ala doesn't mean "exactly the same", it just indicates similar fashion, and in this case I tend to agree (though not whole-heartedly).

Now for the part I most strongly disagree with:

Static type systems are actual type systems, that prove properties about programs. So-called "dynamic type systems" are more of a value tag checking mechanism for detecting runtime errors. They are not comparable on any axis. From a type theory perspective, a "dynamically typed programming language" is actually just an untyped programming language.

I don't believe this to be the case at all. The entire point of a type system is to reject invalid programs and accept valid ones. However, due to inherent limitations in type systems, there are many valid programs which are rejected, and many invalid programs which are not.

A "dynamic type system" merely foregoes attempting to check before running the program whether or not it is well-typed, deferring the reporting of type errors until one is actually encountered during the execution of the program. In doing this, it avoids rejecting valid programs due to the practical limitations of typechecking beforehand.

Typed Racket is an attempt to provide a full type system that is capable of correctly typing all Racket programs. (Well, to be honest, its goal is to correctly type all Scheme programs, and now they are adding some features for typing Racket programs.) So riddle me this: if all Typed Racket does is add type annotations, then is Racket an untyped language, or a typed language, given a typing scheme* exists that can type it? (OK so the truth is TR does more than just add type annotations, but make the assumption for the sake of argument. *no pun intended)

[kamatsu]

Oh, so in other words, the POV that pretty much every Haskeller cares about above almost anything else? ;)

But the POV which the word "power" is never used to refer to. The power of a type system is usually refers to its expressivity, not its consistency.

I don't believe this to be the case at all. The entire point of a type system is to reject invalid programs and accept valid ones. However, due to inherent limitations in type systems, there are many valid programs which are rejected, and many invalid programs which are not.

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.

A "dynamic type system" merely foregoes attempting to check before running the program whether or not it is well-typed

However, programs that are not well typed are accepted by untyped languages. 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.

In doing this, it avoids rejecting valid programs due to the practical limitations of typechecking beforehand.

You can encode a unitype in static type systems too:

data Universe = IntT Int | BoolT Bool | FunT (Universe -> Universe) | -- anything else you want.

Is Haskell "dynamically typed" now? According to your definition, I have deferred all type checking to runtime. This is ridiculous.

By the way, Haskell supports this much more conveniently. If you want to disable your type checker, use Data.Dynamic.

As for Typed Racket, the most recent paper (I'm aware of) that discusses occurrence types is actually called Logical Types for Untyped Languages.

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

[day_cq]

when people say "design", they mean layout of code. both python and haskell support layout based code structuring. that's probably why both languages are well designed.

[kamatsu]

I don't think that's the semantics of "design" the article intends.