wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) (07/28/90)
farrell@batserver.cs.uq.oz.au (Friendless) writes: >jgk@osc.COM (Joe Keane) writes: >>Despite what some people say, i don't think strong typing is such a good deal. >>It catches obvious errors, but doesn't do you any good against less obvious >>bugs. > This is no reason to reject it! But the best thing about strong typing is >the fact that you can take advantage of it when you compile things, by knowing >for example whether they want arguments or not, and you can make assumptions >about what they return when they evaluate, etc. Types are also useful as a >framework for the programmer to think about the roles of various parts of his >program. What is strong typing? Is it just the case that every member of a sum-of-products establish some type and all together another type? Does it requires open type implementations or do you introduce abstract sort names for each member of the sum? Is the domain of a constrained object an anonymous one? Exists any standard paper about strong typing? - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Wolfgang Grieskamp wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET
farrell@batserver.cs.uq.oz.au (Friendless) (07/30/90)
wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp) writes: >farrell@batserver.cs.uq.oz.au (Friendless) writes: >>jgk@osc.COM (Joe Keane) writes: >>>Despite what some people say, i don't think strong typing is such a good deal >>>It catches obvious errors, but doesn't do you any good against less obvious >>>bugs. >What is strong typing? Is it just the case that every member of a >sum-of-products establish some type and all together another type? >Does it requires open type implementations or do you introduce >abstract sort names for each member of the sum? Is the domain of a >constrained object an anonymous one? I didn't have in mind any particular concept of strong typing, other than the idea that you have to be able to determine at compile-time what type things are. Sorry, but I'm not a type-theorist. My particular favourite is Milner polymorphism, because it's easy and it provides exactly the type information which an implementation needs and can use. That is, you need to know the information that Milner typing gives you, and you cannot take advantage of any more. Correct me if I'm wrong, please. John
tom@stl.stc.co.uk (Tom Thomson) (07/31/90)
> I didn't have in mind any particular concept of strong typing, other than >the idea that you have to be able to determine at compile-time what type >things are. Sorry, but I'm not a type-theorist. My particular favourite is >Milner polymorphism, because it's easy and it provides exactly the type >information which an implementation needs and can use. That is, you need to >know the information that Milner typing gives you, and you cannot take >advantage of any more. Correct me if I'm wrong, please. > Why should type checking be restricted to compile time? It is perfectly possible to have strong typing which is done wholely at run-time (any interpreter is going to behave like that). 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). 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. Tom Thomson [tom @ me.stl.stc.co.uk PS: No, I don't know any language implementations that let me do this, more's the pity.
farrell@batserver.cs.uq.oz.au (Friendless) (08/01/90)
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
nick@lfcs.cs.edinburgh.ac.uk (Nick Rothwell) (08/01/90)
In article <3263@stl.stc.co.uk>, tom@stl.stc.co.uk (Tom Thomson) writes: > Why should type checking be restricted to compile time? > It is perfectly possible to have strong typing which is done wholely > at run-time (any interpreter is going to behave like that). No, you can have interpreters which don't do typechecking at all. Our ML system just interprets a form of untyped language calculus. Why is typechecking an issue connected to interpretation? > 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? 0 is an integer, just like 17 is. Milner-style typechecking is structural, so it knows about, say, integers, but not about positive integers, primes, and non-structural entities of this kind. -- Nick Rothwell, Laboratory for Foundations of Computer Science, Edinburgh. nick@lfcs.ed.ac.uk <Atlantic Ocean>!mcsun!ukc!lfcs!nick ~ ~~ ~~ ~~ ~~ Hey, son, get that DeLorean off the track! And ~~ ~~ ~~ ~~ ~ what have you done with all my lovely harpsichords?
dnt@lfcs.ed.ac.uk (David N Turner) (08/01/90)
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.
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (08/04/90)
I think we need some definitions of terminaology. The word type is being
badly abused in this discussion. The two sides essentially coming at it
with two different definitions. How about we adopt the algebrist's
terminology and go from there.
Type: What you write after the colon in a variable declaration. This can
be any set valued expression.
Sort: The essential structure of an object. Essentially the largest
homogeneous set containing the object. Essentially a cludge invented
to make decidable "typing" algorithms. VERY context dependant.
For example, whether 3 is INTEGER or REAL or whatever,
depends on what you have decided as your basic sorts: an abitrary
decision.
Now having sorting information is simply not enough to ensure that
partial functions will always be safely applied.
You need to do some sort of exception handling.
The question is whether the exception handling is done within the
functional paradigm or whether you invent side-effects to handle such
problems.
To my mind the functional paradigm is either superior or it is not. If
you have to introduce side-effects to handle anything then you might as
well be programming in C from the start.
--
Brendan Mahony | brendan@batserver.cs.uq.oz
Department of Computer Science | heretic: someone who disgrees with you
University of Queensland | about something neither of you knows
Australia | anything about.tom@nw.stl.stc.co.uk (Tom Thomson) (08/06/90)
In article <5448@castle.ed.ac.uk> nick@lfcs.ed.ac.uk (Nick Rothwell) writes: >0 is an integer, just like 17 is. Milner-style typechecking is structural, >so it knows about, say, integers, but not about positive integers, primes, >and non-structural entities of this kind. > I think this misses the point completely. The reason for introducing zero-division as an example was precisely to point that Milner-style type checking doesn't cover this case - - in fact any type checking system that insists on operating at compile time and not at run time (while leaving it possible to write a reasonable range of programs) will fail to cover this case. Also, what does structural mean in this context? In terms of structural types, I can easily define positive integers as a type distinct from natural numbers including zero. I have never come across a functional language that would stop me doing this. I think it might be useful to think about why we have type systems (to limit the damage when we apply a function to arguments outside its domain) rather than what a particular type system (or class of type systems) can do. Tom Thomson [tom@nw.stl.stc.co.uk
tom@nw.stl.stc.co.uk (Tom Thomson) (08/06/90)
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
tom@nw.stl.stc.co.uk (Tom Thomson) (08/06/90)
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
dnt@lfcs.ed.ac.uk (David N Turner) (08/06/90)
In article <3283@stl.stc.co.uk>, tom@nw.stl.stc.co.uk (Tom Thomson) writes: > ... > 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? > ... That was roughly my point (I think :-). I think the problem with your idea for enhanced type checking is that it puts type checking algorithms into a completely different ballpark. There are enough problems with the time complexity etc. of current type checkers (which don't even scratch the surface of what you are suggesting). I accept your point that since we can write programs that don't terminate then perhaps we shouldn't worry too much about non-termination during compilation. However, when you say "why should I insist THEY terminate at compile time". Your argument relies on the fact that the only programs which don't terminate at compile time are the ones which don't terminate at run time. Even if you didn't mean the "THEY" to have such emphasis then I think there is still a point to be made : the kind of type checking algorithm you suggest, which is far more powerful than, for instance, Milner-style type checking is surely quite likely to fail to terminate (before you get fed up waiting :-) for valid programs as well as programs which would not terminate anyway. Hence, you cannot ignore problems with non-termination and time complexity. Dave.
sakkinen@tukki.jyu.fi (Markku Sakkinen) (08/08/90)
Note2: Third trial to post! Note1: This is the second posting of an article that apparently disappeared while the news software was out of order here for three days. Sorry if somebody receives it twice. In article <3283@stl.stc.co.uk> "Tom Thomson" <tom@stl.stc.co.uk> writes (rather as a side issue in the posting): > ... >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?) > ... Run-time termination (i.e. the termination of _your_ programme) and compile-time termination (i.e. the termination of the _compiler_ you use) are two totally independent things. Well, not totally: if the compilation never terminates, there will never _be_ an executable form of your programme to run. I estimate that 99.99999% of all programmers would consider a compiler badly broken if it did not terminate, or even if its time requirement seemed exponential w.r.t. source code size. And very few programmers would accept to use a _language_ for which it is impossible to build a terminating compiler; even though many programmers today seem to delight in horrible languages like C. (I am a complete outsider in this group. Perhaps non-imperative programmers have more patience than we others.) Markku Sakkinen Department of Computer Science University of Jyvaskyla (a's with umlauts) Seminaarinkatu 15 SF-40100 Jyvaskyla (umlauts again) Finland SAKKINEN@FINJYU.bitnet (alternative network address)
brendan@batserver.cs.uq.oz.au (Brendan Mahony) (08/09/90)
tom@nw.stl.stc.co.uk (Tom Thomson) writes:
->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.
Presumably, the requirement on f is that (f,u,T) form an abelian group.
This certainly cannot be established either at compile or run-time. It
must be established during the specification and refinement phase, since
it will be undecidable for non-finite sets T, and essentially be
somewhat unwieldy for largish sets, say of size 10 and above. I think,
in part, you are pointing out a problem with the exclusive use of
executable notations.
The typing problem occuring here lies in the fact that "reduce" will
happily go about its business regardless of the nature of the "f" and
"u" passed to it. The user may never realise that the answers being
produced are complete garbage. This example shows that the original
problem put forward goes far beyond the idiosyncracies of lazy
evaluation.
In fact it helps make it clear that the original problem was
due to a failure of type security not to the method of evaluation used.
The function in question was being used incorrectly. It is the job of
the programmer to ensure that an overall product cannot be used
incorrectly (i.e. it must at least make it clear that it is producing
garbage), and hence that all internal functions are always used correctly.
The primary tool available for ensuring this is the programmers
intellect. Compile time and run-time checks can help in discovering some
incorrect uses of functions, but as we have seen the general problem is
theoretically beyond their capacity. The only way of having reasonable
confidence that all functions will always be used correctly is to
produce rigorous logical proofs that this is the case. Lambda calculus
is not an appropriate vehicle for producing such proofs, though its
cousin natural deduction is a good candidate for such a vehicle.
Far too little effort is being made by the fp community to deal with
this problem.
--
Brendan Mahony | brendan@batserver.cs.uq.oz
Department of Computer Science | heretic: someone who disgrees with you
University of Queensland | about something neither of you knows
Australia | anything about.JWC@IDA.LiU.SE (Jonas Wallgren) (08/10/90)
In article <5448@castle.ed.ac.uk> nick@lfcs.ed.ac.uk (Nick Rothwell) writes: >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 eroor trap except a type failure indication from the hardware >0 is an integer, just like 17 is. Milner-style typechecking is structural, >so it knows about, say, integers, but not about positive integers, primes, >and non-structural entities of this kind. Then perhaps some appropriate questions are: What is a type? What are types used for? Should the type of an object exactly describe its possible values (Tom T), or should types be coarse, well-known approximations (Nick R), such as integers, thus making reasoning about the program simpler? Maybe there are as many answers to these questions as there are programmers and computer scientists...? ------------------------------------------------------------------------------- Jonas Wallgren | JWC@IDA.LiU.SE Department of Computer and Information Science | Linkoping University |------------------------------- SE-581 83 Linkoping | Sweden |(\x.xx)(\x.x):(forall a.(a->a)) -------------------------------------------------------------------------------
des@frogland.inmos.co.uk (David Shepherd) (08/21/90)
In article <1990Aug17.124142.9332@tukki.jyu.fi>, sakkinen@tukki.jyu.fi (Markku Sakkinen) writes: |> I estimate that 99.99999% of all programmers would consider |> a compiler badly broken if it did not terminate, or even if its |> time requirement seemed exponential w.r.t. source code size. |> And very few programmers would accept to use a _language_ for which |> it is impossible to build a terminating compiler; even though |> many programmers today seem to delight in horrible languages like C. try using SunOS 4.0 cc on a Sparc with -04 (or even -02 sometimes) on some files .... I've heard of one the went 24hrs and still counting :-) -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 529 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq