Lambda the Ultimate

inactiveTopic Kent M. Pitman's Second Wind
started 11/13/2001; 12:31:04 PM - last post 11/15/2001; 7:44:54 AM
Chris Rathman - Kent M. Pitman's Second Wind  blueArrow
11/13/2001; 12:31:04 PM (reads: 602, responses: 4)
Kent M. Pitman's Second Wind
Part deuce of a Q&A of Kent Pitman over at slashdot. More discussion of Lisp and various other programming language issues.
Posted to general by Chris Rathman on 11/13/01; 12:31:56 PM

pixel - Re: Kent M. Pitman's Second Wind  blueArrow
11/13/2001; 5:05:04 PM (reads: 616, responses: 0)
What i don't really like is the easy/non-argumented way of discarding the benefit of static typing. Moreover stating that "type analysis of Common Lisp is no big deal" is hard to believe since soft-typing is still in research-stage. soft-typing's goal is to keep the whole expressiveness of dynamic typing, but this goal doesn't go along with existing dynamic languages.

http://www.cis.upenn.edu/~bcpierce/types/archives/current/msg00294.html

Noel Welsh - Re: Kent M. Pitman's Second Wind  blueArrow
11/14/2001; 5:20:30 AM (reads: 594, responses: 0)
Regarding the type analysis assertion there was an interesting post on this topic a while ago on Slashdot (believe it or not). I think the post was by the main implementor of CMU Common Lisp and the claim was that the CMU compiler does type inference for the monomorphic subset of Common Lisp. This is normally the bits where speed matters the most (e.g. numerical processing) so it works well in practice.

As for the static/dynamic typing debate as a DrScheme user I use their soft typer (MrSpidey) every time I use DrScheme. The message you reference talks about an old soft typer. MrSpidey is a lot better and gets around the issues raised in the message.

For me the static/dynamic debate comes down to this: do I want my programs restricted to what the type system can currently prove? I prefer to lead theory with practice rather than the other way round. YMMV.

pixel - Re: Kent M. Pitman's Second Wind  blueArrow
11/14/2001; 9:12:49 AM (reads: 596, responses: 1)
Regarding the type analysis assertion there was an interesting post on this topic a while ago on Slashdot (believe it or not). I think the post was by the main implementor of CMU Common Lisp and the claim was that the CMU compiler does type inference for the monomorphic subset of Common Lisp. This is normally the bits where speed matters the most (e.g. numerical processing) so it works well in practice.

The aim of this is optimizing. It tries to find code that is used mono-morphically. I'm only interested in the safety part of static typing, not the performance part. Performance is mainly the pb of the critical path, whereas safety must take care of the whole program.

As for the static/dynamic typing debate as a DrScheme user I use their soft typer (MrSpidey) every time I use DrScheme. The message you reference talks about an old soft typer. MrSpidey is a lot better and gets around the issues raised in the message.

I've been trying MrSpidey to see how some pbs were solved. But I must have missed something. Even trivial examples give unreadable "error" messages:

(define (sum l)
  (if (empty? l) null
      (+ (car l) (sum (cdr l)))))

the analyser display a nice window the source code with supposed errors colored red. You have to click on one red expression to get a box containing the type:

(rec
 ((y1 (list (union nil num))))
 ((union nil y1 (cons num y1)) *-> num))

the error here must be <tt>(union nil num)</tt>, but i have not tried to understand the full recursive type meaning.

As a comparison, ocaml would say:

let rec sum = function
| [] -> []
| e::l -> e + sum l
              ^^^^^
This expression has type 'a list but is here used with type int

I've also tried using a simple "<tt>let</tt>" but with no luck... Doesn't it handle simple scheme?

Noel Welsh - Re: Kent M. Pitman's Second Wind  blueArrow
11/15/2001; 7:44:54 AM (reads: 658, responses: 0)
I agree with you on safety, and appreciate the benefits that arise from static typing. I just wanted to add what I know about CMU Common Lisp's type inference as you had raised a query about its effectiveness.

As for MrSpidey, I agree that the types are often hard to comprehend. The reason, as I understand it, is that MrSpidey's type system is more expressive than ML (it includes union and recursive types) and consequentially the type definitions it infers are more complex.