[psygnisfive]

When Bob says that it's restrictive, what he means is simply that you cannot say more. Which is true -- you can't express things when your only type is "something". You're allowed to saying nothing, and that's it. And that's pretty darn restrictive!

[tantalor]

I take it oppositely.

In C++, if I declare the type of something incorrectly, the compiler yells at me. That's restrictive. I have to get it "right".

Python doesn't ask me, because it doesn't care, so I can't be wrong. That's freeing.

[chc]

You have to get it right in Python too, and you can certainly be wrong — the information is just implicit and the compiler won't check it for you. You find out whether you're wrong when your program either behaves correctly or doesn't. A lot of the errors I've found debugging Python code have boiled down to "This code wasn't expecting that type."

[psygnisfive]

As CHC says below, "dynamic" typing is no different. It's just a deferment of wrongth, not a lack of it.

But if I were to take a staunch SPJian-McBridian position, I would say this attitude arises from really useless type systems.

A good type system is EITHER capable of letting you say as little as necessary, and only telling you when something is messed up (like Haskell or ML, which have type inference and therefore don't require you to write types) OR is capable of letting you say what you mean, and then doing a lot of work for you.

This is the wonderful benefit of dependent types: you can say enough about your intention that you stop fighting the type checker, and actually get the type checker to do work for you.

This is really something that hasn't percolated into the mainstream of programming yet, but is slowing creeping into Haskell with typed holes, but in dependently typed languages like Agda or Epigram, types can be expressive enough that your editor can write half the program for you just because the type you wrote has only one program as its inhabitant.

McBride likes to describe it as, Dependent Types warp code space so that the direction we want to travel is "down", and all we have to do is let ourselves fall.

As an example, here's a demonstration of some simple (but exemplary) interaction with Agda. If we define this type:

    data Vec (A : Set) : Nat -> Set where
      Nil : Vec A 0
      Cons : forall {n} -> A -> Vec A n -> Vec A (1 + n)

where `Nat` is the type of natural numbers and `Vec` is the type of lists indexed by their length, then we might be inclined to write this function:

    append : forall {A m n} -> Vec A m -> Vec A n -> Vec A (m + n)
    append xs ys = {! !}0

where the `{! !}0` is a portion of the program that hasn't yet been defined, called a hole. We can put the cursor in the hole (hole 0) and ask the editor to do a case split on `xs` with `Control-c Control-c x`, and the program will change to be

    append : forall {A m n} -> Vec A m -> Vec A n -> Vec A (m + n)
    append Nil ys = {! !}0
    append (Cons x xs) ys = {! !}1

if we put the cursor in hole 0, we can hit `Control-c Control-a` (a for agsy, or auto) and itll fill in the hole with the solution `ys`, and if we do the same in hole 1, itll fill in `Cons x (append xs ys)`.

The type of the function we're defining is enough that agda can actually find the definition with almost no help from us.

Not knuckle wrapping here :)

[adamwk]

C++ is probably in that land of bad languages the author was referring to.