[plt-scheme] Why do folks implement *dynamically* typed languages?

On May 30, 2007, at 1:47 AM, Michael Vanier wrote:

> That sounds great, in principle.  How do you check your types  
> statically?

Let's distinguish between idea and real because the
operative word in Carl's prose is 'can.' And let's go
slowly for everyone here.

A type systems is a logic for reasoning about the
run-time actions of your program. Like in plain old
logic, a sound logic is the only one that matters,
though CS has shown that even unsound logics are
used as successful crutches in the real world.
(Relevance logic anyone?)

Carl alluded to the important word in the preceding
paragraph: 'a'. Depending on what type language you
choose, you can express certain theorems (the value
of this expression is always an integer), eh, types
and not express others (the integer is always in a
certain range). Equally important, depending on the
proof rules you throw in, a type system may or may
not be able to prove your chosen theorems. That is,
even though a theorem about a piece of your program
is true (holds at run-time), your type system is probably
unable to prove it. In general, existing and practical
type system can only prove/check shallow thruths, which
is as useful as a typo-checker in prose (don't forget
it's vs its, their vs there, etc).

The checking of types (aka theorems) can happen in three
ways:

  -- writing down so many lemma, eh, auxiliary
     type annotations that it is just a question
     of proof checking. This is an explicitly
     statically typed language. (Think Java.)

  -- writing down a very small number of type
     annotations and using a theorem prover,
     aka, a type inference mechanism to create
     the proof for you.

     There are two variants:

     ++ those that reject programs for which
     you can't create a proof of conformance with
     the type system. ML is the prime example.

     ++ those that inform you of the failure
     and allow you to run the program anyway.
     Soft type systems, such as Soft Scheme
     and MrSpidey, are examples here.

  -- prove the types, eh, theorems, "by hand."

The boundaries between the first two options aren't
hard, indeed, they are quite fluid.

So here is Carl's message in this context.

A statically typed language (explicit or implicit) chooses
a proof system and a language of theorems once and for all.
If it can't check your chosen theorems, it'll reject the
program. You can't run it. Period.

A dynamically typed language allows programmers to ignore
theorems about programs (for a while) and to act in
blissful ignorance. Good programmers always think about
programs and to think means to prove theorems in this context.
Since nobody has chosen a type system for you, you can
choose your own type system for a DL and, best of all,
you can switch around. Yes, you can use two distinct
type systems at the same time. The disadvantage is that
you must establish the theorems by hand, that your
successor-in-maintenance can't modify the program and
re-establish the theorems quickly, etc. Indeed, programmers
in this world tend not to write down theorems, eh, types,
and so these truths that they established in their minds
and by hands get lost. Every time you touch the program
you must re-establish them.

Given that, I like to work with DLs for at least three reasons:

1. It is easy to prototype in them. (This is not only due to
the lack of types but also because these languages are dynamic,
not just dynamically typed.)

2. As a researcher, I can explore programming paradigms without
being constrained by a type system. If I were to use ML, I'd
have to develop a type system for mutually recursive modules
before I start programming with units. At the time I did that,
I experienced tremendous push-back from the ML community about
this issue. (It's impossible. It's bad. You shouldn't do that.)
If I had been an MLer, I probably wouldn't have tried.

3. I have been interested and I have worked on importing type-based
idea into the software design process for DLs for almost 20 years.
It's a great area with lots of opportunities and little competition.

If I were to write batch programs for a living and a company, I
may choose OCAML simply to restrict the pool of programmer-applicants
to the intelligent ones. And also because my priorities would shift
from invention to fear of maintenance. But I may also stick with
PLT Scheme and pour the necessary energy into Typed Scheme to make
it fully operational.

-- Matthias







>
> Mike
>
> Carl Eastlund wrote:
>> Which way are you asking?  Your subject line asks one question, but
>> your content asks another.  I guess you are trying to ask "why  
>> dynamic
>> languages?"
>> Here's why I like dynamically typed languages: because types are far
>> too important too me.  I'm not going to let some tyrannical type
>> checker decide in advance what type system I'm going to use for all
>> programs.  I'm going to use whatever notion of types is appropriate
>> for my current task, and check as much of that statically as I can.
>> If ML's type checker, or Haskell's type checker, or Java's type
>> checker can't verify my invariants, or worse reject my program as an
>> error - all static type checkers are guaranteed to reject some 100%
>> correct programs as errors - I'd be out of luck in those languages.
>> I'm always in luck with Scheme.
>> It puts a lot of responsibility on me to get the system right, but I
>> can live with that.
>> On 5/29/07, Grant Rettke <grettke at acm.org> wrote:
>>> Hi folks,
>>>
>>> Why do people design dynamically typed (DL) languages over  
>>> statically
>>> typed languages (Sl)?
>>>
>>> In the case of Lisp, it seems obvious, metaprogramming. That  
>>> said, you
>>> can metaprogram in SLs, so maybe it is not so obvious.
>>>
>>> Are there any good papers or books on this matter?
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme