🚀 go-pugleaf

In article <3263@stl.stc.co.uk>, tom@stl.stc.co.uk (Tom Thomson) writes:

> ...
> Currently most systems do some type checking at run time: what is a
> divide-by-zero error trap except a type failure indication from the hardware?
> If you believe that Milner-style type checking is adequate, would you
be happy
> to modify your hardware to not cause this trap but deliver some result of the
> operation instead? 
>
> Is "tail" defined on lists or on non-nil lists? If the latter, how do
you cope
> with this in a Milner-style system (pretty clumsily, if at all, I
would guess).
> ...
> Tom Thomson  [tom @ me.stl.stc.co.uk
> ...

I think you are confusing type checking, which gives information about the type
of a value at run time (shockingly enough), and a system which gives
information
about the actual value returned at run time. With reference to your
"tail" example,
Milner-style type checking will guarantee that you never apply "tail" to
anything
other than a list. It does not say anything, however, about whether
"tail" is applied
to a nil list.

The kind of information you are asking for is slightly more ambitious I think,
bearing in mind that we cannot write a program to determine whether a function
halts or not.

Dave.