Re[2]: [Haskell-cafe] head as a total function
Hello Bill, Thursday, September 7, 2006, 8:24:53 PM, you wrote: >> it was the first imperative language supporting closures, after all > Uh, what about lisp? Lots of Idiotic Silly Parentheses? :) well, i say about more or less well-known non-FP languages. actually, i'm sure that some FBCPL supports closures (or at least anonymous functions) several years before Algol-68 :) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] head as a total function
> it was the first imperative language supporting closures, after all Uh, what about lisp? For those who read the "Foozles" slides posted earlier [0], I must say he nailed this one, on slide 2. The (MIT) lisp 1.4 manual (ca. 1965) refers to FUNCTION differing from QUOTE in that it handled free variables "correctly"; I take this to mean that at least a primitive form of closure was provided. Steele's work on Scheme helped Lisp programmers take lexical scoping seriously [1]; these ideas and a method for efficient implementation were attributed to Algol [2]. That lexical scope was available in some dialect of Lisp, even very early on, doesn't surprise me (and according to [3] is the case). But I do think dynamic scoping took a while to "die out" as generally accepted Lisp practice (it does still exist in Common LISP, with a special keyword, IIRC) and that Scheme (late 1970s) helped to effect that. Moreover, a language that provides SET/SETQ, RPLACA/RPLACD and the PROG feature (including labels and a goto) surely qualifies as imperative? Haskell has been called the best imperative programming language ever. :-) I mean, Haskell has IORef and friends, right? Jared. [0] http://hope.cs.rice.edu/twiki/pub/WG211/M3Schedule/foozles.pdf [1] Tenth paragraph, this page: http://www.lisp.org/table/Lisp-History.html [2] Steele's Rabbit compiler paper, p.13. See also Steele's Lambda papers [3] Steele and Gabriel, Evolution of Lisp. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] head as a total function
On Thu, 2006-09-07 at 11:03 +0400, Bulat Ziganshin wrote: . . . > it was the first imperative language supporting closures, after all Uh, what about lisp? The (MIT) lisp 1.4 manual (ca. 1965) refers to FUNCTION differing from QUOTE in that it handled free variables "correctly"; I take this to mean that at least a primitive form of closure was provided. Moreover, a language that provides SET/SETQ, RPLACA/RPLACD and the PROG feature (including labels and a goto) surely qualifies as imperative? -- Bill Wood ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] head as a total function
Hello oleg, Thursday, September 7, 2006, 10:28:00 AM, you wrote: > P.S. Algol68 was my favorite language too. +1 :) it was the first imperative language supporting closures, after all -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] head as a total function
Jo'n Fairbairn wrote in response to Neil Mitchell: > > And as you go on to say, if you apply it to the infinite > > list, who cares if you used head. Head is only unsafe on > > an empty list. So the problem then becomes can you detect > > unsafe calls to head and let the programmer know. > No, that's the wrong approach because it relies on detecting > something that (a) the programmer probably knows already and > (b) is undecidable in general. It would be far better for > the programmer to express this knowledge in the > programme. It is indeed possible -- and quite easy -- to write programs where head and tail are total functions. That issue was discussed, for example, at the end of an old message: Exceptions in types and exception-free programming http://www.haskell.org/pipermail/haskell/2004-June/014271.html The first two thirds of the message showed how to make exceptions apparent in the signature of a function, so we can see if a function could potentially raise the `head of an empty list' exception just by looking at its (inferred) type. The exception-free programming is far more rewarding, and practical as well. We don't actually need to introduce subtyping; explicit injection/projections don't seem to be as much of (syntactic) overhead. There is absolutely no runtime overhead! The non-empty lists have exactly the same run-time representation as the regular lists. The technique generalizes to arrays, even numbers, sorted lists (and, seemingly, to strings that are safe to include into HTML/SQL documents). That technique has been mentioned several times recently (perhaps not on this forum). Quite complex algorithms like Knuth-Morris-Pratt string search (with mutable arrays, packed strings, general recursion and creative index expressions) can be handled. Again, without introducing any runtime overhead: http://pobox.com/~oleg/ftp/Haskell/KMP-deptype.hs The approach is formalizable; the recent PLPV talk by Chung-chieh Shan presented the types systems and the proof techniques. Some of the proofs have been formalized in Twelf: http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html#Formalization In short, the safety property (absence of `head of an empty list' exception) is a corollary to the Progress theorem, for a type system with dependent-type flavor. The type system doesn't actually have dependent types. Furthermore, whatever dependent-type flavor there is, it can be erased while maintaining the safety guarantees, given some precisely stated conditions on the safety kernel. P.S. Algol68 was my favorite language too. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
