Path: utzoo!utgpu!news-server.csri.toronto.edu!clyde.concordia.ca!uunet!mcsun!ukc!stl!tom@nw.stl.stc.co.uk From: tom@nw.stl.stc.co.uk (Tom Thomson) Newsgroups: comp.lang.functional Subject: Re: What is strong typing? (Was: I like strong typing) Message-ID: <3284@stl.stc.co.uk> Date: 6 Aug 90 02:00:04 GMT References: <4387@uqcspe.cs.uq.oz.au> <1689@opal.tubopal.UUCP> <4424@uqcspe.cs.uq.oz.au> <3263@stl.stc.co.uk> <4461@uqcspe.cs.uq.oz.au> Sender: news@stl.stc.co.uk Reply-To: "Tom Thomson" Organization: STC Technology Limited, London Road, Harlow, Essex, UK Lines: 65 In article <4461@uqcspe.cs.uq.oz.au> farrell@batserver.cs.uq.oz.au writes: >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. Yes, we should tell the compiler as much as possible and let it do as much work as possible at compile time. After all, we are going to run most programs more often than we compile them. But this doesn't mean that we should not allow our machine to check for inappropriate arguments to functions at run time - - no compiler is that clever (maybe some programmers are, but then presumably they don't need a compile-time type checker either? I know I'm not that clever). > 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. > I think we agree on everything except terminology. Certain errors I would call type errors, and expect "the system" to detect for me and raise an exception; you've chosen not to call them type errors. I would, however, point that type resolution (and in particular resolution of overloading) can occur at run time (as well as error detection); most object-oriented languages seem to have this capability; when one wants a module capability, so that one ends up with different implementations of the same abstract type and transfer functions to convert between them, some run-time resolution seems inevitable. >>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 > > I have got no idea what you mean by "reduce a function over a set". More >information please? > This is pretty straightforward. If I have a set of numbers, I can talk about their sum and their product; these two things are described by a "reduction" function: one reduces binary addition (or binary nultiplication) over the set with respect to an unit value of zero (or one). It's not possible to talk about the difference or quotient of a set, because subtraction and division do not have the right properties. Think of it as starting from a function on lists: reduce :: ((alpha * beta) -> beta) * beta * list alpha -> beta; reduce f u (cons a l) = reduce f (f a u) l; reduce f u nil = u; Then impose the requirement that it's meaningful for sets, rather than just for lists: ie you have to get the same result for the same set of list elements, regardless of the order they occur in. You can see how this requirement to be relevant to sets imposes restrictions on the function "f" in the above definition; and today's type systems do not allow me to specify these restrictions. Tom Thomson [tom@nw.stl.stc.co.uk