🚀 go-pugleaf

In article <5450@castle.ed.ac.uk> dnt@lfcs.ed.ac.uk (David N Turner) writes:
>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.


No, I'm not confused, you are.

Even if I restrict myself to compile-time type checking, there doesn't
appear to be any reason to restrict myself to type checking which is 
guaranteed to terminate (since I can probably write programs which won't
terminate at run time, why should I insist they terminate at compile time?)
 - but maybe that wasn't your point?

When I'm trying to point out deficiencies in compile-time-only type
checking in general, you don't advance the discussion any by pointing
out that one particular style of compile-time type system has the very
deficiencies I'm drawing attention to - - at least not if you think
you are disagreeing with me!

Type checking is about one very simple semantic issue: is the argument
I'm using in the domain of the function I'm applying (in the sense of
it making sense to try to apply the function; the result may be bottom,
or not, that's irrelevant, we just want to be sure that we're not asking
our program to eat a chair or sit on a cream bun).  We need to look at 
how well the type system characterises the domains of the functions we
want to use. Then we need to look at how well the functions we want to use
map these domains onto each-other.  This will throw up a variety of problems,
some of which can be handled by a Milner type system and some of which cannot,
and some of which are best handled during transformation from one
representation (ML, say) to another (PDP8 machine code say) and some of which
are best handled during evaluation of the program (ok, so the distinction
between evaluation and transformation is theoretically unsound, because
evaluation is simply transformation of representations of values; despite
that I'll stick with it, because I have to deal with practical engineering).

I think your article is trying to claim that the two occurences of "some 
of which" in the preceding paragraph refer to the same subset of the
problems at issue.  Where's your evidence for that?  If you weren't claiming
that, what DID you mean to say?

Tom Thomson  [tom@nw.stl.stc.co.uk