Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!lewis!dnt
From: dnt@lfcs.ed.ac.uk (David N Turner)
Newsgroups: comp.lang.functional
Subject: Re: What is strong typing? (Was: I like strong typing)
Message-ID: <5450@castle.ed.ac.uk>
Date: 1 Aug 90 10:58:59 GMT
References: <4387@uqcspe.cs.uq.oz.au> <1689@opal.tubopal.UUCP> <4424@uqcspe.cs.uq.oz.au> <3263@stl.stc.co.uk>
Reply-To: dnt@lfcs.ed.ac.uk (David N Turner)
Organization: Computer Science, Edinburgh University
Lines: 34

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.