[erlang-questions] Runtime checking for types

[Jesper Louis Andersen]

On Wed, Apr 20, 2011 at 16:21, Tony Finch <dot@REDACTED> wrote:
> Richard O'Keefe <ok@REDACTED> wrote:
>> On 18/04/2011, at 10:58 PM, Jesper Louis Andersen wrote:
>> >
>> > Remember, dynamic typing is a straitjacket, in which you cannot fully
>> > express yourself, whereas static typing give you a rich language for
>> > doing so.
>>
>> This sounds very much like a crab telling humans how limited they
>> are by the absence of a shell.  Think of the problems of moulting.
>
> Sounds like Robert Harper.
>
> http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/

Indeed.

There are, more or less, two opposing views to take: You can go from a
statically typed world to a dynamically typed one by erasure of the
types. Just ignore them. The other way is what Harper advocates in
which you create a single type which you then proceed to assign to any
term. To understand why you in the world would want to have static
knowledge of a type you need something which is at least as expressive
as SML or Ocaml though. Otherwise static type systems are usually not
giving anything worthwhile back.

The Erlang approach with the dialyzer is an extremely interesting
middle-ground in my opinion. It is not types in the usual sense, but
it allows for gradually explaining more and more about the program in
specifications. I believe that for any language to succeed in the long
run, you need to approach both disciplines - static and dynamic - and
provide some support for both worlds.



-- 
J.