[mhluongo]

Spec (and more generally, contracts) aren't just about "making up" for the lack of static typing. They can encode a variety of invariants that a type-system can't, and are also useful for parsing (see coercion) and generative testing. Unlike most type systems, they also aren't required across the whole code base.

[nilved]

It depends on how you implement the gradual typing as well. Through contracts is one way (probably the bad way, since they still apply at runtime) and static analysis with type annotations is another way. There isn't any reason a sufficient static analyzer couldn't be as powerful as an inbuilt static type system.

This is effectively dragging some of the benefits of static typing to dynamic typing. I wonder why you'd pay the cost of dynamic types though, instead of going the other direction. With type inference you don't need to explicitly write types the entire codebase, and you can opt-in to dynamic types in controlled, explicit scenarios.

[tel]

Parsing and generative testing are well-covered by static types, but I'll give you that contracts can enforcing things static types cannot. That said, static types can enforce things that contracts cannot, too.

Furthermore, in my experience I find use of the things that static types can catch and contracts cannot on a nearly hourly basis while I rarely to never use things that contracts can check but static types cannot.

[arohner]

> static types can enforce things that contracts cannot

Example, please?

[tel]

Sure. Consider the type

    forall a. a

With mild conditions on what the program fragment achieving this type can do I can be certain that this function does not return. It is an error, an infinite loop, or simply does not exist.

No contract can verify this because they inspect the value and thus get stuck by infinite loops.

I don't use that sort of thing often, but here's a simpler one:

    sort :: Ord a => [a] -> [a]

I know that `sort` only uses the ordering properties of the values within the list. It could be generalized to `forall a . (a -> a -> Ordering) -> [a] -> [a]` in which case it would be totally oblivious to the values inside of the list except in that it probably applies that function.

No contract system can examine functions. No contract system can prove universals. Types can do both (in certain, principled ways).

---

Another interesting example is handling something like a channel. In Haskell, we have the type `TChan a` which is a channel carrying values of type `a`. In Clojure, the best we can do for giving a contract to a core.async chan is to say it's a "chan containing something" or even "a dereffable thing returning something". To use a contract here we'd have to check every value that ever pops off the channel.

Contracts check shape, but cannot ensure usage.