head as a total function

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

head as a total function

oleg-7

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: head as a total function

Bulat Ziganshin-2
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,
 Bulat                            mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: head as a total function

Bill Wood-3
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: head as a total function

Jon Fairbairn
In reply to this post by oleg-7
[hidden email] writes:

> Jo'n Fairbairn wrote in response to Neil Mitchell:
> > 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:

Oh, indeed. Come to think of it, in Ponder the list type was
something like (to translate into invalid Haskell)

   type List t = Maybe (NonEmptyList t)
   type NonEmptyList t = (t, List t)

but while I did some little experiments that took advantage
of that, I wasn't quite avant-garde enough to leave head and
tail out of the language (back then it was hard enough to
get people to try functional programming at all, and leaving
out the friendly-seeming functions would have made it just
too strange)

> P.S. Algol68 was my favorite language too.

I wrote the Ponder compiler in A68C...


--
Jón Fairbairn                                 [hidden email]
http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html  (updated 2006-07-14)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: head as a total function

Jared Updike
In reply to this post by Bill Wood-3
> > 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re[2]: head as a total function

Bulat Ziganshin-2
In reply to this post by Bill Wood-3
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,
 Bulat                            mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe