Python from Wise Guy's Viewpoint

[Jon S. Anthony]

(e-mail address removed) (Jon S. Anthony) once said:

I'm not sure I understand you, but if I do, then "templates" take care
of this. That is, we'd write (e.g. for the 3-arg case):

template <class A, class B, class C>
Result someFunc( A a, B b, C c ); // fudging "Result" for simplicity

which means that someFunc works "forall" types A, B, and C.

No, it means for any _instantiations_ of types A, B, and C, this will
(probably) give a runable function back.

/Jon

 

[Marshall Spight]

For your
average Joe (or Jane), having at least the option to freely play with
mutable values, and imperative flow, makes programming a WHOLE LOT
easier to reason about.

I used to think that, but I'm not so sure anymore. Oh, I
suppose it's true for Joe or Jane where they're already
used to variables and imperative flow, but if they're not?
How would we know whether recursion or loops are
easier to learn? I don't think we would know anything
unless we did a big test on naive subjects.


Marshall

 

[james anderson]

(e-mail address removed) once said:
...

There are two ways to go. If it's reasonable to know statically about
this attribute, then you could encode it in the type system (e.g. a type
like DOMWithDocumentElement). My hunch (based on my very limited
knowledge of the domain) is that this is a dynamic attribute. So
instead you'd 'fail' if the attribute didn't match at run-time. Note
that my Haskell code returned "Maybe XMLRep"s, so the corresponding code
would look something like

-- has type Maybe XMLRep
if (hasAttr domObj "documentElement")
then Just ... -- do the conversion of the domObj
else Nothing

The same strategy would be used to cope with other 'dynamic failures'
in the other branches, such as a malformed XML string, or a
non-existent file when converting from a filename.

one favor which clos brings to the party is a fairly direct means to express
type constraints with arbitrary valence. generic functions turn the original
__init__ sort of "inside-out" and suggest an expression more like:

(defclass XML_Objectify () ())

(defgeneric __init__ (what from)
method ((instance XML_Objectify) (source string))
(case (char source 0)
(#\< (with-input-from-string (stream source)
(__init__ instance stream)))
(t (__init__ instance (intern-uri source)))))
method ((instance XML_Objectify) (source http-uri))
(with-open-uri (stream source :method :get)
(__init__ instance stream)))
method ((instance XML_Objectify) (source pathname))
(with-open-file (stream source :direction :input)
(__init__ instance stream)))
method ((instance XML_Objectify) (source stream))
(__init__ instance (parse-document source)))
method ((instance XML_Objectify) (source xml-document))
(dolist (element (children (root source)))
(setf (slot-value instance (name-symbol (name element)))
(read-from-string (value element))))))

if one needed additional specialization, one could add additional parameters,
as in

(defgeneric __init__ (what from how) ...)

from some perspectives this is "easy". from others perhaps not.
....

 

[prunesquallor]

I think I have a stumper. I'll be impressed if a type checker can
validate this. The same-fringe function takes a pair of arbitrary
trees and lazily determines if they have the same leaf elements in the
same order. Computation stops as soon as a difference is found so
that if one of the trees is infinite, it won't cause divergence.

(defun lazy-sequence (x y)
(if (null x)
(funcall y)
(funcall x
(lambda (xh xt)
(lambda (z)
(funcall z xh
(lambda ()
(lazy-sequence
(funcall xt)
y))))))))

(defun lazy-fringe (x)
(cond ((null x) '())
((consp x) (lazy-sequence (lazy-fringe (car x))
(lambda () (lazy-fringe (cdr x)))))
(t (lambda (z)
(funcall z x (lambda () ()))))))

(defun lazy-same (s1 s2)
(cond ((null s1) (null s2))
((null s2) nil)
(t (funcall s1
(lambda (h1 t1)
(funcall s2
(lambda (h2 t2)
(if (eql h1 h2)
(lazy-same (funcall t1) (funcall t2))
nil))))))))

(defun same-fringe (l1 l2)
(lazy-same (lazy-fringe l1) (lazy-fringe l2)))

(defun testit ()
(assert (same-fringe '((1 2) (3 (4))) '(1 (2 3) (4))))
(let ((circular-list (list 3)))
(setf (cdr circular-list) circular-list)
(assert (not (same-fringe `((1 2) (3 ,circular-list)) `(1 (2 3) (3 4)))))))

 

[Brian McNamara!]

(e-mail address removed) once said:

I think I have a stumper. I'll be impressed if a type checker can
validate this. The same-fringe function takes a pair of arbitrary
trees and lazily determines if they have the same leaf elements in the
same order. Computation stops as soon as a difference is found so
that if one of the trees is infinite, it won't cause divergence.

Laziness is pretty orthogonal to static typing.

This one is so easy, we do it in C++ just for spite.
I'm using the FC++ library as a helper.

----------------------------------------------------------------------
#include <iostream>
using std:stream;
using std::cout;
using std::endl;

#include "prelude.hpp"
using namespace boost::fcpp;

struct LispCons;
typedef either<int,LispCons*> LispValue;

struct LispCons {
LispValue car;
LispValue cdr;
LispCons( LispValue x, LispValue y ) : car(x), cdr(y) {}
};

LispValue make( int x ) { return inl(x); }
LispValue make( LispCons* x ) { return inr(x); }

// "l" prefix for "Lisp"
LispValue lnil = make( (LispCons*)0 );
LispValue lcons( LispValue x, LispValue y ) {
return make( new LispCons( x, y ) );
}

ostream& operator<<( ostream& o, LispValue l ) {
if( l.is_left() )
o << l.left();
else {
LispCons* p = l.right();
if( !p )
o << "()";
else
o << "(" << p->car << "." << p->cdr << ")";
}
return o;
}

struct Fringe : public c_fun_type<LispValue,list<int> > {
list<int> operator()( LispValue lv ) const {
if( lv.is_left() )
return cons( lv.left(), NIL );
else {
LispCons* lc = lv.right();
if( lc==0 )
return NIL;
else
return cat( Fringe()(lc->car),
thunk1(Fringe(),lc->cdr) );
}
}
} fringe;

int main() {
LispValue one = make(1), two = make(2),
three = make(3), four = make(4);
// tree1 = '((1 2) (3 (4)))
LispValue tree1 = lcons(lcons(one,lcons(two,lnil)),
lcons(three,lcons(lcons(four,lnil),lnil)));
cout << "tree1 is " << tree1 << endl;

// tree2 = '(1 (2 3) (4))))
LispValue tree2 = lcons(one,lcons(lcons(two,lcons(three,lnil)),
lcons(lcons(four,lnil),lnil)));
cout << "tree2 is " << tree2 << endl;

cout << "fringe(tree1) is " << fringe(tree1) << endl;
cout << "fringe(tree2) is " << fringe(tree2) << endl;

LispCons* tmp = new LispCons(three,lnil);
tmp->cdr = make(tmp);
LispValue circle = make(tmp);
cout << "first 10 of fringe(circle) is "
<< take(10,fringe(circle)) << endl;

// tree3 = '(1 (2 3) (<circle>))))
LispValue tree3 = lcons(one,lcons(lcons(two,lcons(three,lnil)),
lcons(lcons(circle,lnil),lnil)));
cout << "first 10 of fringe(tree3) is "
<< take(10,fringe(tree3)) << endl;
cout << "tree2 = tree3? " << (fringe(tree2) == fringe(tree3)) << endl;

return 0;
}
----------------------------------------------------------------------

The output:
----------------------------------------------------------------------
tree1 is ((1.(2.())).(3.((4.()).())))
tree2 is (1.((2.(3.())).((4.()).())))
fringe(tree1) is [1,2,3,4]
fringe(tree2) is [1,2,3,4]
first 10 of fringe(circle) is [3,3,3,3,3,3,3,3,3,3]
first 10 of fringe(tree3) is [1,2,3,3,3,3,3,3,3,3]
tree2 = tree3? 0

 

[Pascal Costanza]

Ha!

Although this doesn't get me any closer to my goal of
simple, useful, correct program that cannot be proven
typesafe.

OK, here we go!



(defvar *default-company* 'costanza-inc)

(defclass employed ()
((original-class :initarg riginal-class)
(company :accessor company :initarg :company)
(salary :accessor salary :initarg :salary)))

(defun hire (someone salary &key (company *default-company*))
(let* ((original-class (class-name (class-of someone)))
(employed-class
(intern (format nil "~A-~A" 'employed original-class))))
(eval `(defclass ,employed-class (employed ,original-class) ()))
(change-class someone employed-class
riginal-class original-class
:company company
:salary salary)))

(defun fire (someone)
(when (member
(find-class 'employed)
(class-precedence-list (class-of someone)))
(change-class someone (slot-value someone 'original-class))))


(defun test-employed ()
(let ((person (make-symbol "PERSON")))
(eval `(defclass ,person ()
((name :accessor name :initarg :name))))
(let ((joe (make-instance person :name "joe")))
(format t "-> hire joe~%")
(hire joe 60000)
(format t "name: ~A~%" (name joe))
(format t "current class: ~A~%" (class-name (class-of joe)))
(format t "original class: ~A~%" (slot-value joe 'original-class))
(format t "company: ~A~%" (company joe))
(format t "salary: ~A~%" (salary joe))
(format t "-> fire joe~%")
(fire joe)
(if (member (find-class 'employed)
(class-precedence-list (class-of joe)))
(format t "joe is still employed.~%")
(format t "joe is not employed anymore.~%")))))



And here is a sample session:

CL-USER 1 > (test-employed)
-> hire joe
name: joe
current class: EMPLOYED-PERSON
original class: PERSON
company: COSTANZA-INC
salary: 60000
-> fire joe
joe is not employed anymore.
NIL



Some minor comments:

- This is all standard ANSI Common Lisp, except for
CLASS-PRECEDENCE-LIST which is part of the semi-standard MOP.

- This codes runs without any changes and without any additional
libraries on both LispWorks 4.3 and Macintosh Common Lisp 5.0, and
probably also on many other Common Lisp implementations. (This fulfils
the requirement that this is indeed a relatively short example.)

- I have used EVAL to define classes at runtime, because although the
MOP defines ENSURE-CLASS for that purpose the latter is not defined in
Macintosh Common Lisp. The use of EVAL is not the reason for this code
not being acceptable for a static type checker.

- The important thing here is that the EMLOYED mixin works on any class,
even one that is added later on to a running program. So even if you
want to hire martians some time in the future you can still do this.

- As an interesting sidenote, both Common Lisp compilers I have used
emit a warning that there is no definition for the function NAME that is
called in TEST-EMPLOYED. I don't care - the code is elegant, relatively
straightforward to understand, useful and correct. And I can safely
ignore the warning - it works as expected.



Pascal


P.S., to Joe Marshall: I hope you don't mind that I hire and fire you
within a split second. ;-)

 

[Darius]

On Sat, 25 Oct 2003 23:27:46 GMT

I think I have a stumper. I'll be impressed if a type checker can
validate this. The same-fringe function takes a pair of arbitrary
trees and lazily determines if they have the same leaf elements in the
same order. Computation stops as soon as a difference is found so
that if one of the trees is infinite, it won't cause divergence.

-- this is all sooo pointless in Haskell
data LazyList a
= Nil
| Cons (forall r. ((a,() -> LazyList a) -> r) -> r)

data Tree a = Empty | Leaf a | Fork (Tree a) (Tree a)

-- lazySequence :: LazyList a -> (() -> LazyList a) -> LazyList a
lazySequence Nil y = y ()
lazySequence (Cons x) y
= x (\(xh,xt) ->
Cons (\k -> k (xh,(\() -> lazySequence (xt ()) y))))

-- lazyFringe :: Tree a -> LazyList a
lazyFringe Empty = Nil
lazyFringe (Leaf a) = Cons (\k -> k (a,\() -> Nil))
lazyFringe (Fork l r) = lazySequence (lazyFringe l)
(\() -> lazyFringe r)

-- lazySame :: Eq a => LazyList a -> LazyList a -> Bool
lazySame Nil Nil = True
lazySame Nil _ = False
lazySame (Cons s1) (Cons s2)
= s1 (\(h1,t1) ->
s2 (\(h2,t2) -> h1 == h2 && lazySame (t1 ()) (t2 ())))

-- sameFringe :: Eq a => Tree a -> Tree a -> Bool
sameFringe t1 t2 = lazySame (lazyFringe t1) (lazyFringe t2)

testit = test1 && not test2
where test1 = sameFringe (Fork (Fork (Leaf 1) (Leaf 2))
(Fork (Leaf 3) (Fork (Leaf 4)
Empty)))
(Fork (Leaf 1)
(Fork (Fork (Leaf 2) (Leaf 3))
(Fork (Leaf 4) Empty)))
test2 = sameFringe (Fork (Fork (Leaf 1) (Leaf 2))
(Fork (Leaf 3) cl))
(Fork (Leaf 1)
(Fork (Fork (Leaf 2) (Leaf 3))
(Fork (Leaf 3) (Leaf 4))))
cl = Fork (Leaf 3) cl

testit == True quite unsurprisingly, the example trees aren't -exactly-
the same as the ones in the Lisp version. This requires one popular
extension to Haskell 98 (rank-2 types). Of course, all these
shenanigans are unnecessary in Haskell.

I already have a bunch of Church encoded data structures as well if
that's next.

 

[prunesquallor]

P.S., to Joe Marshall: I hope you don't mind that I hire and fire you
within a split second. ;-)

I'm getting used to it.

 

[prunesquallor]

On Sat, 25 Oct 2003 23:27:46 GMT


-- this is all sooo pointless in Haskell

Well, yeah.

data LazyList a
= Nil
| Cons (forall r. ((a,() -> LazyList a) -> r) -> r)

I specifically didn't define the LazyList type. I don't want to write
type annotations. I want the type inference engine to deduce them.

I should have been more specific: I *know* that all these things can
be done in a statically typed language. What I don't know is whether
these can be done as *easily*. Will this type check without giving
the type checker hints about the type of
(lambda (x y) (lambda (z) (z x y)))? Will it type check if you
don't tell it that the `cons' in lazySequence is the same `cons'
in lazySame and lazyFringe?

I already have a bunch of Church encoded data structures as well if
that's next.

I'm not just trying to come up with convoluted examples for the sake
of quizzing you. I'm trying to find the point where the type checker
gets confused. I'm not writing it in Haskell because I don't know
Haskell, so I'm writing in Lisp. It will always be possible to
*recast* the problem in your favorite language, but can you
transliterate it and let the type checker infer that the program is
correct?

 

[prunesquallor]

(e-mail address removed) once said:

Laziness is pretty orthogonal to static typing.

This one is so easy, we do it in C++ just for spite.
I'm using the FC++ library as a helper.

[snip]

Yuck! Type declarations *everywhere*. Where's this famous inference?

What's this LispCons type? I don't have that in my source. My code
is built of lambda abstractions. I don't have a lispvalue type either.
And it isn't limited to integers in the list. Where did my functions go?

And how can you compare a LispCons to an integer?

This works, but it doesn't faithfully represent what I wrote.
In addition, with all the type decorations, it only serves to reinforce
the idea the static type checking means a lot of extra keystrokes.

 

[Darius]

data LazyList a
= Nil
| Cons (forall r. ((a,() -> LazyList a) -> r) -> r)

I specifically didn't define the LazyList type. I don't want to write
type annotations. I want the type inference engine to deduce them.[/QUOTE]

This is a data declaration, -not- a type declaration. For example,
Bool is data Bool = True | False and lists would be data [a] = [] | a
:[a]. If I were to use Java would I not be allowed to use 'class'?
class introduces a type too.

Furthermore, 'data' doesn't just give you a type. It also gives you
constructors, destructors (kind of), and recognition.

data Either a b = Left a | Right b
The idiomatic Lisp functions that would correspond to what this
declaration provides would be something like: left, right, leftp,
rightp, eitherp, get-left, get-right.

Also, that type distinction let's me add LazyList to typeclasses like
Show, Read, Eq, Ord, Monad, Num, etc. Perhaps, I don't like my lazy
lists displaying as #<closure> or my trees as ((3 2) (4)) when what I'd
want is((3 . (2 . ()) . (4 . ())). Perhaps, I don't want
(equal<the lazy list 1 2 3> <the lazy list 1 2 3>) to return nil because
they aren't the same procedure.

Also, ignoring the testit function, my code with those four laborious
"type annotations" is 16 lines compared to 29 lines of lisp. (Including
it, it's still shorter.)

If all you want to do is show an example in Lisp that won't type check
in most statically typed language without any alterations you could
simply write,(list t 3) or (if t 'a 10).

Finally, I don't want to write some insane continuation passing
sequence. I want the language to not overevaluate. I guess lazy Lisp or
dynamic Haskell beats us both.

 

[Dirk Thierbach]

(e-mail address removed) once said:

Finally, an example that I don't think you can type in Haskell.

It's a bit tricky. As Remi has shown, you need recursive types.
Recursive types in Haskell always need an intervening data type
constructor. That's a conscious design decision, because recursive
types are very often a result of a real typing error. (IIRC, that's
why OCaml added an option to enable recursive typing after having it
enabled as default for some time, but Remi should know that better
than I do.)

We also need an existential type in this constructor, because the
argument can be of different type for each application of the black hole.

data BlackHole = BH (forall a. a -> BlackHole)

Now we can write the black hole function itself:

black_hole :: BlackHole
black_hole = BH (\_ -> black_hole)

That's it. However, we cannot apply it directly. We have to "unfold"
it explicitely by taking it out of the data constructor. We define an
auxiliary infix function to take care of that.

infixl 0 $$

($$) :: BlackHole -> a -> BlackHole
(BH f) $$ x = f x

Now we can write a function like

f = black_hole $$ "12" $$ 5 $$ True

which will nicely typecheck.

That's the first time one actually has to add non-obvious stuff to
"please" the type checker. OTOH, the black hole function is pretty
bogus, so one can argue that this is a realistic price to pay to say
that you really really want this strange function. I would be very
surprised if this function is of any use in a real-world program.

And there is nothing else you can do with arguments of arbitary type
but silently discard them, so I guess there are not many other examples
like this.

- Dirk

 

[Dirk Thierbach]

(e-mail address removed) (Brian McNamara!) writes:

Yuck! Type declarations *everywhere*. Where's this famous inference?

You *did* notice that it is C++, which hasn't type inference (and
a lousy typesystem? So what Brian is saying that this is so easy
he can even to it with hands tied on his back and standing on his
head.

In addition, with all the type decorations, it only serves to reinforce
the idea the static type checking means a lot of extra keystrokes.

Yes. C++ and Java are to blame for that, and it's a completely
justified obverservation. Static typechecking in C++ and Java just
sucks, and gets in the way all the time. If I had the choice between one
of them and a dynamically typed language, I would of course use the
dynamically typed one.

But there are other statically typechecked languages where you don't
have this kind of trouble. I don't know if this thread turns out do to
something useful for anyone, but if it does, I would hope it gets at
least this idea across.

- Dirk

 

[Dirk Thierbach]

But I suppose you really want this example

statically typed, huh?

After quite some time, I think I have finally figured out what Pascal
meant with

I have the impression that he is confusing dynamic type errors and
runtime errors. In Lisp and Smalltalk they are more or less the same,
and since dynamic type errors map to static type errors, he may think
by analogy that other runtime errors must necessarily also map to
compile errors somehow involved with static typing. Of course this is
nonsense; those two are completely different things. The "too many
cases" referred to some cases of runtime errors he didn't want to be
checked at compile time. As you cannot get "too many test cases" by
type annotations static typing (which was the context where he made
this comment), like you cannot get "too many test cases" by writing too
many of them by hand, I really had a hard time figuring this out.

To sum it up: Unit tests (some, not all!) correspond to type
annotations, static type checking is the same as running the test
suite, dynamic types correspond to data types, runtime errors
correspond to runtime errors (surprise .

Ok, I'll try. If I come up short, I expect it's because I'm fluent
in neither Haskell nor Lisp, not because it can't be done.

You don't really need runtime errors for the above example,
but here's a similar version to yours that throws an error in
'cerror' to return to the toplevel. No Maybe types.

cerror :: String -> String -> IO a -> IO a
cerror optmsg errmsg cont = do
print errmsg
print ("1: " ++ optmsg)
print ("2: Fail")
s <- getLine
x <- readIO s
let choice 1 = cont
choice 2 = ioError (userError errmsg)
choice x

f :: Integer -> IO (Integer)
f x =
if (x < 200)
then return (x * 2)
else cerror
"Type another number"
"You have typed a wrong number"
(getLine >>= readIO >>= f)

And you got it, exactly as you wanted. Perfectly typeable.
(Please don't say now "but I want to use the Lisp code, and
it should run exactly as it is, without any changes in syntax").
You could even assign the very same types in Lisp if any of the
extensions of Lisp support that. (I didn't try.)

- Dirk

 

[Andreas Rossberg]

Tell that to the hackers who worked on the "Python" compiler found in
CMUCL, SBCL, and some others. It does extensive type inference for both
efficiency and correctness. But it doesn't get in the way (except in
certain rare cases), it just (noisely) informs you what it thinks.

Clarification: I was talking about strong typing, i.e. full and precise
inference. As I wrote in another posting, I don't believe in soft typing,
since it has exactly the weaknesses that seems to make proponents of dynamic
typing judge type systems having marginal utility: its only use is to flag
more or less trivial errors, and unreliable so.

I would be very, very surprised to see a strong type system put on top of an
untyped language successfully, i.e. without changing or restricting the
language severely.

Correction: it could not work without typing--dynamic typing does not
imply a lack of typing. I could be wrong, but it seems you would rule
out generic functions in the CLOS (and dynamic dispatch in general) with
the above statement.

See my example below.

power.

This doesn't sound right: erasing type information should not invalidate
the post conditions; it should simply make it more difficult
(impossible?) to check the validity of the post conditions.

It does, because it also invalidates the pre conditions, on which the post
conditions depend.

This program should still work, even if you fail to type-check it, if
said type-checking would have passed successfully.

This is only a meaningful observation if you look at a closed program. If
you simply erase types from some given piece of code it may or may not
continue to work, depending on how friendly client code will act. In that
sense it definitely changes meaning. You had to protect against that using
other, incomparable features. So there is a difference in expressiveness.

And making modular composition more reliable is exactly the main point about
the expressiveness types add!

This statement is irrelevant because dynamic typing does not eliminate
type information.

Yes it does. With "dynamic typing" in all its incarnations I'm aware of type
infromation is always bound to values. Proper type systems are not
restricted to this, they can express free-standing or relational type
information.

As an example of the kind of "overloading" (or type dispatch, if you want)
you cannot express in dynamically typed lagnuages: in Haskell, you can
naturally define functions which are overloaded on their return type, i.e.
you don't need any value at all at runtime to do the "dispatch". For
example, consider an overloaded function fromString, that produces values of
potentially arbitrary types from strings.

- Andreas

 

[Lex Spoon]

Clarification: I was talking about strong typing, i.e. full and precise
inference.

Please let us be careful with the terminology. Strong typing means
that type checking happens at some point, and that a type error is
never allowed to complete (and thus do something non-sensical).
Inference is a completely independent axis -- any type system may or
may not have type inference. If you happen to like strong
*dynamically* typed languages then it is extremely irritating when
people assume strong typing can only happen at compile time.

I don't know the exact word you are looking for, unfortunately.
"complete" doesn't seem right, because that seems to be a property of
an inferencer: an inferencer is complete if it finds a type assignment
for any program that can be type checked. "sound" doesn't seem right,
either. A sound type system produces *correct* types, but those types
may not be tight enough to predict an absence of type errors.

Maybe you should just say "static checking". People will assume you
probably mean that programs get rejected if they have type errors.

As an example of the kind of "overloading" (or type dispatch, if you want)
you cannot express in dynamically typed lagnuages: in Haskell, you can
naturally define functions which are overloaded on their return type, i.e.
you don't need any value at all at runtime to do the "dispatch". For
example, consider an overloaded function fromString, that produces values of
potentially arbitrary types from strings.

You can do this kind of thing in dynamically typed languages, too,
though unfortunately it is not very common. Do a web search on
"object-oriented" and "roles" and a lot comes up. This is the same
thing: depending on the role that a requestor sees an object under,
the object can respond differently even to the same messages. For
example, someone may respond to #requestPurchase differently depending
on whether the request treats them like a father or treats them like
the president of a company. And it works for functional languages,
too, as is clearly exhibited by your fromString() overloaded function.
It could be viewed as acting differently depending on whether it is in
an int-producer role or a float-producer role.


(Incidentally, a lot of the results that turn up regard languages for
databases. I was surprised at how much interesting language research
happens in the database world. They take the view that long-lived
data is important. This is common to Smalltalk people, and perhaps to
people who like Lisp machines, but even Scheme and Lisp people don't
seem to think a whole lot about this idea. Database people certainly
do, however. You can't just repopulate a database all the time!)

Anyway, depending on the role that the requestor is talking to, a
responder (be it a function or an object) can act differently. In
some cases, the expected role can be figured out automatically,
instead of needing to be written explicitly. This is somewhat similar
to the behavior of C++ when you invoke a non-virtual method: the type
of the *variable* decides what will happen.


Getting aside from theory and research, Matlab and Perl both allow
this kind of context sensitivity. When you call a Matlab function,
the function knows how many return values you are expecting. If you
call a function in Perl, it can tell whether you want a scalar or a
vector back, and it can act accordingly. (At least, the built-in Perl
functions can do this.)



-Lex

 

[Joachim Durchholz]

Yuck! Type declarations *everywhere*. Where's this famous inference?

Hey, what do you expect of C++ code?

No type declarations in Haskell.

Regards,
Jo

 

[Joachim Durchholz]

I would challenge any enthusiast of Haskell, SML, Mozart, Clean, or the
like to come up with something similarly direct.

Take Mozart out: it uses run-time typing.

Regards,
Jo

 

[Pascal Costanza]

Sidenote: The code above has a bug. Here is the correct version:

(defun f (x)
(if (< x 200)
(* x 2)
(progn
(cerror "Type another number"
"You have typed a wrong number")
(print '>)
(f (read)))))

(Noone spotted this bug before. All transliterations I have seen so far
have silently corrected this bug. It is interesting to note that it
probably weren't the type systems that corrected it.)

After quite some time, I think I have finally figured out what Pascal
meant with




I have the impression that he is confusing dynamic type errors and
runtime errors. In Lisp and Smalltalk they are more or less the same,
and since dynamic type errors map to static type errors, he may think
by analogy that other runtime errors must necessarily also map to
compile errors somehow involved with static typing. Of course this is
nonsense; those two are completely different things. The "too many
cases" referred to some cases of runtime errors he didn't want to be
checked at compile time. As you cannot get "too many test cases" by
type annotations static typing (which was the context where he made
this comment), like you cannot get "too many test cases" by writing too
many of them by hand, I really had a hard time figuring this out.

I think you have a restricted view of what "type" means. Here is the
same program written in a "type-friendly" way. (Again, in standard ANSI
Common Lisp. Note that the type is defined inside of f and not visible
to the outside.)

(defun f (x)
(check-type x (real * 200))
(* x 2))

CL-USER 1 > (f 5)
10

CL-USER 2 > (f 666)

Error: The value 666 of X is not of type (REAL * 200).
1 (continue) Supply a new value of X.
2 (abort) Return to level 0.
3 Return to top loop level 0.

Type :b for backtrace, :c <option number> to proceed, or :? for other
options

CL-USER 3 : 1 > :c 1

Enter a form to be evaluated: 66
132

You don't really need runtime errors for the above example,
but here's a similar version to yours that throws an error in
'cerror' to return to the toplevel. No Maybe types.

cerror :: String -> String -> IO a -> IO a
cerror optmsg errmsg cont = do
print errmsg
print ("1: " ++ optmsg)
print ("2: Fail")
s <- getLine
x <- readIO s
let choice 1 = cont
choice 2 = ioError (userError errmsg)
choice x

f :: Integer -> IO (Integer)
f x =
if (x < 200)
then return (x * 2)
else cerror
"Type another number"
"You have typed a wrong number"
(getLine >>= readIO >>= f)




And you got it, exactly as you wanted. Perfectly typeable.
Nice.

(Please don't say now "but I want to use the Lisp code, and
it should run exactly as it is, without any changes in syntax").

No, I don't care about syntax.

You have used CPS - that's a nice solution. However, you obviously
needed to make the type declaration for f :: Integer -> IO (Integer)

Note that my code is not restricted to integers. (But I don't know
whether this is actually a serious restriction in Haskell. I am not a
Haskell programmer.)

You could even assign the very same types in Lisp if any of the
extensions of Lisp support that. (I didn't try.)

What you actually did is: you have assigned a "broad" type statically,
and then you revert to a manual dynamic check to make the fine-grained
distinction.

In both Lisp versions, you have exactly one place where you check the
(single) type. A static type system cannot provide this kind of
granularity. It has to make more or less distinctions.


I regard the distinction between dynamic type errors and runtime errors
to be an artificial one, and in fact a red herring. I would rather call
the former type _exceptions_. Exceptions are situations that occur at
runtime and that I have a chance to control and correct in one way or
the other. Errors are beyond control.

This might be terminological nitpicking, but I think it is a serious
confusion, and it probably stems from weakly typed languages that allow
for arbitrary memory access and jumps to arbitrary machine addresses.
The niche in which such languages are still useful is getting smaller by
the time. (Languages like Java, Python, Ruby, etc., did a fine job in
this regard, i.e. to promote writing safe programs, rather than using
languages for high-level purposes that are actually designed for writing
hardware drivers.)

Anything below real runtime errors (core dumps) has the chance to be
controlled and corrected at runtime. (Including endless loops - they
should never be unbreakable in the first place.)

This can give you a real advantage for long-running systems or for very
large applications that you don't want to, or cannot stop and restart on
a regular basis.

Both (correct) code snippets I have provided are considerably smaller
than your solution and both are more general. And my second solution
still provides a way to correct a wrong parameter at runtime at no
additional cost. I regard this a feature, not a problem.

Assume that you need to write a program that has only vague
specifications and requires a high level of such flexibility in its
specs. _I_ would fire the programmer who would insist to use a language
that requires him to program all this flexibility by hand, and
especially wants to see a specification for "unforeseen problems",
whether formal or not.

See http://www.dilbert.com/comics/dilbert/archive/dilbert-20031025.html


Pascal

P.S.: Please always remember the original setting of this thread. The
original original questions was something along the lines of "why on
earth would one not want a static type system?" I don't want to prove
the general superiority of dynamic type checking over static type
checking. Heck, there isn't even a general superiority of typing over
no-typing-at-all. All these approaches have their respective advantages
and disadvantages, and should be used in the right circumstances.

Yes, you can clearly tell from my postings that I prefer dynamic typing
over static typing. This in turn means that I am probbaly not a good fit
for projects that require a strong static approach. And everyone who
prefers static typing is probably not a good fit for projects that
require a strong dynamic approach. So what? All of us who participate in
this discussion are probably not good fits for writing hardware drivers.


Everyone should do what they are best at, and everyone should use the
tools that fit their style most.

But why on earth should anyone want to prove that their own preferred
_personal_ style is generally superior to all others?



"If I have seen farther than others, it is because I was
standing on the shoulder of giants."

--- Isaac Newton


"In computer science, we stand on each other's feet."

--- Brian K. Reed


P.P.S.: And I still think that soft typing is the best compromise. It's
the only approach I know of that has the potential to switch styles
during the course without the need to completely start from scratch.

 

[Don Geddis]

(e-mail address removed) reasonably noted:

Hindley-Milner type inference always terminates. The result is either
a provable mismatch, or a provable-non-mismatch.

You're completely wrong, which can be easily demonstrated.

The fact that it terminates isn't the interesting part. Any inference
procedure can also "always terminate" simply by having a timeout, and reporting
"no proof" if it can't find one in time.

So what's interesting is whether the conclusions are correct.

Let's take as our ideal what a dynamic type system (say, a program in Lisp)
would report upon executing the program. The question is, can your type
inference system make exactly the same conclusions at compile time, and predict
all (and only!) the type errors that the dynamic type system would report at
run time?

The answer is no.

A provable mismatch means that there is an execution branch that will crash
if you ever get there. If for some reason this branch will never get
executed, either because it's (non-provably) dead code

That's one obvious case, so even you know that your claim of a "provable
mismatch" is incorrect. There are programs that will never have run-time
errors, but your static type inference will claim a type error.

or because you have an implicit restriction for possible arguments to this
expression the type system doesn't know about, than you could call it a
"valid program", but it will still be rejected, yes.

So haven't you just contradicted yourself? Perhaps you think this "implicit
restriction" is unfair, because you've kept information from the system.
But the real problem is that all the information might be there, but the
system isn't capable of making sufficient inferences to figure it out.

For example:
(defun foo (x)
(check-type x (integer 0 10))
(+ 1 x) )
(defun fib (n)
(check-type n (integer 0 *))
(if (< n 2)
1
(+ (fib (- n 1)) (fib (- n 2))) ))
(print (foo (fib 5)))

This program prints "9", and causes no run-time type errors. Will it be
successfully type-checked at compile time by a static system? Almost certainly
the answer is no.

In case the code isn't clear; FOO is a function that increments a number by
one. Its domain is [0,10], and its range is [1,11]. FIB is the Fibonacci
sequence, with domain [0,infinity] and range [1,infinity].

Are you allowed to call FOO with the output of FIB? In general, no, because
the range of FIB is much greater than the domain of FOO.

However, in the particular case of the particular code in this program, it
turns out that only (FIB 5) is called, which happens to compute to 8, well
within the domain of FOO. Hence, no run-time type error. Unfortunately, the
only way to figure this out is to actually compute the fifth Fibonacci number,
which surely no static type inference system is going to do. (And if you do
happen to find one, I'm sure I can come up with a version of the halting
problem that will break that system too.)

Do you now accept that your static type inference systems do NOT partition
all programs into "either a provable [type] mismatch, or a provable [type]
non-mismatch"?

Finally, to get back to the point of the dynamic typing fans: realizing that
type inference is not perfect, we're annoyed to be restricted to writing only
programs that can be successfully type checked at compile time. Nobody
objects to doing compile-time type inference (e.g. as the CMUCL compiler for
Common Lisp does) -- especially just to generate warnings -- but many people
object to refusing to compile programs that can not be proven type-safe at
compile time (by your limited type inference systems).

-- Don
_______________________________________________________________________________
Don Geddis http://don.geddis.org/ (e-mail address removed)