Re: Why I don't believe in static typing

From: Erann Gat (gat_at_jpl.nasa.gov)
Date: 11/18/03 

Date: Tue, 18 Nov 2003 12:05:02 -0800

In article <q72q81-fu7.ln1@ID-7776.user.dfncis.de>, Dirk Thierbach
<dthierbach@gmx.de> wrote:

> Frank A. Adrian <fadrian@ancar.org> wrote:
> > Dirk Thierbach wrote:
> >
> >> Types encode invariants. They form a contract about the behaviour
> >> of some part of my code. If I break this contract in such a way that
> >> it changes the type, the type checker will point out all places
> >> I have to think about.
>
> > Why do you believe that all variables and parameters need this very strict
> > invariant during all phases of program development,
>
> Because unless I explicitely say so, this invariant will be the minimal
> invariant needed to make the program work at all. Let's again have a
> look at the type of map
>
> map :: (a -> b) -> [a] -> [b]
>
> This just says that one argument should be a function, and the other
> argument should be a list. Duh. Moreover, the function should be able
> to deal with the elements that are in the list. In return, I am
> promised a list of whatever things the function produces.
>
> If any of these invariants is invalidated, map cannot possibly work.
> So either I have made a typo somewhere, or I have made a design error.

What is the type of this function:

(defun mapn (fn &rest lists)
  (if (every #'null lists)
    nil
    (cons (apply fn (remove nil (mapcar #'car lists)))
          (apply #'mapn fn (mapcar #'cdr lists)))))

in light of this example:

? (mapcar 'type-of (mapn (compose 'sqrt '+) '(1 2 3) '(nil 5 -41/4 1)
'(-101.7 5 5 -3/4 nil)))
((COMPLEX FLOAT) DOUBLE-FLOAT (COMPLEX RATIONAL) RATIO FIXNUM)

E.

Relevant Pages

  • Re: invariant checking in exception case
    ... >cell to the right and an item. ... So, it is possible to add a Void item, and have a void reference to ... Suppose, though, that the application used lists with the property that no ... >With invariant checking enabled in which this property could be evaluated, ...
    (comp.lang.eiffel)
  • Re: freebsd-5.4-stable panics
    ... If I could also have you generate a dump of the KSE group ... > for walking those thread lists? ... an invariant is violated, ... testing the above patch to see if this is a workable work-around, ...
    (freebsd-hackers)
  • Re: The Traditional Superficial Explanation of Relativity
    ... invariant expressions as easily as Poincaré ... lists 8 distinct but elementary invariants in his paper. ... Some authors define special relativity only for kinematics. ... You can built different invariant mathematical objects. ...
    (sci.physics.relativity)
  • Re: Einsteinss, Dirk The Dims, And Ghostys simultaneous absurdities
    ... >> you can prove that with a spacetime diagram. ... >> Think of the familiar example of the city whose map differs by a rotation. ... The analogy is that the Pythagorean-derived distance is the invariant when ... the interval is the invariant. ...
    (sci.physics)
  • Re: Einsteinss, Dirk The Dims, And Ghostys simultaneous absurdities
    ... >> you can prove that with a spacetime diagram. ... >> Think of the familiar example of the city whose map differs by a rotation. ... The analogy is that the Pythagorean-derived distance is the invariant when ... the interval is the invariant. ...
    (sci.physics.relativity)