From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 0A8E5BC57 for ; Sun, 29 Aug 2010 20:42:28 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsoBAB5HekzRVdY0kGdsb2JhbACfdU0IFgEBAQkJDAcRAx+fXIknghOFMS6IVAEBAwWFMgSEb4Ua X-IronPort-AV: E=Sophos;i="4.56,288,1280700000"; d="scan'208";a="57945033" Received: from mail-bw0-f52.google.com ([209.85.214.52]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Aug 2010 20:42:27 +0200 Received: by bwz5 with SMTP id 5so3970425bwz.39 for ; Sun, 29 Aug 2010 11:42:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:in-reply-to :references:date:message-id:subject:from:to:cc:content-type; bh=cZ2cnTx+BAzBnNDRCuhVd4R50o7l0Qhr8TOGMUsDEuY=; b=ndwv8gxjQSKtYO/cu2rkt1+NdDg7hqdNLbv64g716tIqMSX9bPfjbb/50dRLC6IzQN fRRaltHd1AWXrpu68m0HSpsL2Gft+jT8RRMWjok1iOwpYz6SyR9alozgG53kOKJ2UcvE XUsZiB4GDMvQoKLC9eQEtbKpD5Gw888VgIAWg= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=OnZbh4Yp5QesVZlMcwwXZ28Rm5HPfmxLX9Tsc8FyVcYde7m5SopAnQYiYKcj5My8oL bmNYQ0Q+1E0rhIbyh5rdCGlvbzX1o7mXhQ5FgvJSfvD6Xh6LL77RtZk+co46stC2Ckun QvS0VDSa+VM7L2r4nuem2nVI2y+hsRZGw9nc0= MIME-Version: 1.0 Received: by 10.204.63.9 with SMTP id z9mr2496151bkh.66.1283107345557; Sun, 29 Aug 2010 11:42:25 -0700 (PDT) Received: by 10.204.54.68 with HTTP; Sun, 29 Aug 2010 11:42:25 -0700 (PDT) In-Reply-To: References: Date: Sun, 29 Aug 2010 14:42:25 -0400 Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml From: Jeremy Bem To: bluestorm Cc: caml-list List Content-Type: multipart/alternative; boundary=001636c5b9e38a69c8048efab5e3 X-Spam: no; 0.00; bugfix:01 polymorphism:01 foo:01 foo:01 scanf:01 higher-order:01 non-ocaml:01 ocaml:01 bug:01 toplevel:01 bug:01 last-minute:01 makefile:01 bugfix:01 polymorphism:01 --001636c5b9e38a69c8048efab5e3 Content-Type: text/plain; charset=ISO-8859-1 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 --001636c5b9e38a69c8048efab5e3 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
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.
<= div>
An easily overlooked feature of Llama Light is that it i= s written in Llama Light. =A0The fact that this substantial codebase can be= written without let-generalization (and hardly any changes) supports the t= hesis of that paper and , in my opinion, further demonstrates that explicit= polymorphism (which has its own complexities) is not even necessary to red= eem anything.

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

I confess however that the "Scanf" module has= not been ported due to a complex use of let-generalization which I have no= t yet managed to pull apart (anyone want to contribute? ;-).
=A0
And yes, this is relevant to my (more theoretical) work (alth= ough I could certainly live with a system that had let-generalization). =A0= In particular HOL, higher-order logic, does not have it, and because of thi= s, HOL can be interpreted in weak versions of set theory that are easily tr= usted.

As for the location in the documentation, I'll cons= ider changing it...but the basic idea was to write a page that would make s= ense for non-OCaml users. For comparison, the OCaml manual mentions *nowher= e* that let *is* generalized :)

Please keep the bug reports (and non-bug reports) comin= g! =A0The 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

--001636c5b9e38a69c8048efab5e3--