[erlang-questions] Runtime checking for types

[Richard O'Keefe]

On 21/04/2011, at 2:21 AM, Tony Finch wrote:
> 
> Sounds like Robert Harper.
> 
> http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/

The question Harper tries very hard to evade there is

    "Are there any usable type systems that are sufficiently expressive?"

The only type systems he blesses are the ones in ML and Haskell.
As a Haskell programmer, I find ML's type system crippling.  (No type classes?
Relying on ad hoc overloading to deal with + and < ?  Feh!)
And there are enough people who find the Haskell type system limiting that
Epigram, Cayenne, and Agda exist.

Make no mistake, a *good* type system *can* do wonders for you.
See the whole "generic programming" stuff, such as Template Haskell,
and contrast the elegance of QuickCheck in Haskell (driven by the types)
with the clunkier version for Erlang.

At the high end, type systems trail off into things like PVS, where proving
that a specification is type-correct is a non-trivial exercise.  (If anyone
reading this knows PVS and would give me a bit of hand-holding, I'd _really_
like to be able to use it; the language is clear enough, but driving the
theorem prover is very far from obvious.)

When it comes to writing programs, few things are as straitjackety as
a language that isn't finished yet (Epigram) or one where persuading
the compiler your program makes sense requires manual guidance of a
theorem prover.