Re: [Caml-list] Llama Light: a simple implementation of Caml

[Jeremy Bem <jeremy1@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1691 bytes --]

Now that I'm not in a hurry to get a bugfix out, I thought I'd reflect at
greater length on the question about let-generalization.

An easily overlooked feature of Llama Light is that it is written in Llama
Light.  The fact that this substantial codebase can be written without
let-generalization (and hardly any changes) supports the thesis of that
paper and , in my opinion, further demonstrates that explicit polymorphism
(which has its own complexities) is not even necessary to redeem anything.

The most intrusive changes were to the following not-that-common idiom: "let
raise_foo x y = raise (Foo (x, y)) in ..." which is then used in multiple,
incompatible locations. The workaround is simply "let make_foo x y = Foo (x,
y) in ..." which is then raised explicitly.

I confess however that the "Scanf" module has not been ported due to a
complex use of let-generalization which I have not yet managed to pull apart
(anyone want to contribute? ;-).

And yes, this is relevant to my (more theoretical) work (although I could
certainly live with a system that had let-generalization).  In particular
HOL, higher-order logic, does not have it, and because of this, HOL can be
interpreted in weak versions of set theory that are easily trusted.

As for the location in the documentation, I'll consider changing it...but
the basic idea was to write a page that would make sense for non-OCaml
users. For comparison, the OCaml manual mentions *nowhere* that let *is*
generalized :)

Please keep the bug reports (and non-bug reports) coming!  The toplevel bug
was due to overzealous last-minute Makefile pruning...but that's no excuse,
I ought to have a real testing system.

Thanks,
-Jeremy

[-- Attachment #2: Type: text/html, Size: 1951 bytes --]