Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!sdd.hp.com!elroy.jpl.nasa.gov!ames!uhccux!munnari.oz.au!bunyip!brolga!uqcspe!batserver.cs.uq.oz.au!farrell
From: farrell@batserver.cs.uq.oz.au (Friendless)
Newsgroups: comp.lang.functional
Subject: Re: What is strong typing? (Was: I like strong typing)
Message-ID: <4461@uqcspe.cs.uq.oz.au>
Date: 1 Aug 90 07:59:14 GMT
References: <4387@uqcspe.cs.uq.oz.au> <1689@opal.tubopal.UUCP> <4424@uqcspe.cs.uq.oz.au> <3263@stl.stc.co.uk>
Sender: news@uqcspe.cs.uq.oz.au
Reply-To: farrell@batserver.cs.uq.oz.au
Lines: 48

tom@stl.stc.co.uk (Tom Thomson) writes:
>Why should type checking be restricted to compile time?

  Because it makes the implementation faster. I consider this to be enough
reason, others may not. In any case, I like to know the types of things when
I write the program, and therefore there's no reason the compiler shouldn't.

>It is perfectly possible to have strong typing which is done wholely
>at run-time (any interpreter is going to behave like that).

  Not true. An interpreter can do a type checking phase before it runs the
program. I know one which does. But this is just splitting hairs.

>Currently most systems do some type checking at run time: what is a
>divide-by-zero eroor 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).

  Sure, tail can be defined on nil lists. In Miranda, I can say

tail [] = error "Tail applied to nil"

In this case, error has type list char -> list alpha. It's a hack, but
exception handling always is. But I get your point, you can change the type
system to be really clever and then not be able to do typing at compile time.
But since I am not even one little bit interested in doing run-time type
checking, I use Milner types and figure them out at compile-time. Everything
which doesn't work is an error rather than a typing failure, and I raise an
exception.
  
>Personally I would like the type system to ensure, when I reduce a function 
>over a set, that that function is commutative and associative (since the
>reduction operation is otherwise undefined).  I would also like it to check
>that the unit used in the reduction has the right properties.  I can't imagine
>doing this in a type system that doesn't allow me to make assertions that it is
>unable to check (actually I can, but doing the operation 2**n times and making
>sure all the results are the same is not what I want it to do); do Milner style
>systems give this sort of information? I guess not, but I'm absolutely
>certain you can take advvantage of it.

  I have got no idea what you mean by "reduce a function over a set". More
information please?


								John