From:  Robin Popplestone
Subject: Re: Static Typing
Date: 
Message-ID: <65ctqs$kag$1@goldenapple.srv.cs.cmu.edu>
 Juliusz Chroboczek wrote:

> Can one /conceive/ of failed search as an exception, justifying ML's
> approach? Sure. I once had to live with a library routine that treated
> /successful/ search as an exception! The programmer's reasoning: if you
> are adding something to a collection, and checking first to see if it
> already exists, then successful search is bad. <sigh>

You are certainly not constrained to do that! Indeed exceptions -should- be
used primarily for  error reporting,  where they  provide flexibility  (for
example in writing a  package which uses a library of functions that create
exceptions that need to be explained to the  package users, who may be
naive). If  you want to return an answer or a failure, try something like:

    datatype 'a Maybe = OK of 'a | NotSo;

Then the LISP assoc function is rendered:

fun assoc x [] = NotSo
  | assoc x ((p as (x1,y1))::l) =
        if x=x1 then OK p else assoc x l

[obtaining
 val assoc = fn : ''a -> (''a * 'b) list -> (''a * 'b) Maybe
]

I think the LISP community  has a BAD tendency to  turn its back upon  what
the LISP pioneers were trying to  do, namely realise some excellent  formal
ideas on small machines and with  imperfect understanding. I have the  same
tendency (of turning my back on progress)  but try not to proclaim it  as a
virtue...

In particular, LISP pioneered  the implementation of symbolic  mathematical
reasoning - what better  subject of such  reasoning than computer  programs
themselves.

Now one could damn static typing as a weak logic, so argue for HOL etc..
(or Boyer-Moore). But this requires a certain discipline in writing one's
object code.

Robin Popplestone.