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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 0EB19BC57 for ; Sun, 29 Aug 2010 18:37:52 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0CAJQpekzRVdY0kGdsb2JhbACYPQGIBAgWAQEBCQkMBxEDH58eiSeCE4UoLohUAQEDBYUyBIRvhRo X-IronPort-AV: E=Sophos;i="4.56,288,1280700000"; d="scan'208";a="56148312" Received: from mail-bw0-f52.google.com ([209.85.214.52]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Aug 2010 18:37:51 +0200 Received: by bwz5 with SMTP id 5so3914373bwz.39 for ; Sun, 29 Aug 2010 09:37:51 -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=PAs7fyj3sX9E4sQO236j4JIAY54aPTkOsjzBTddm/Xs=; b=RcJObACsSHhysyXy/Vju0sILBTZdkpB2GaohY0zBK6XYH52xzcrkfSFHl+tQB44NH0 x4PrhNUpDnSECPUcIc2nlRUIZwEVqWVXHG12Rmt4siju7bNTG23IM+8IZB15zTCK6ysu 5PU3C08949OmSASmKSkvlSgtbEY89VRcQQCSE= 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=CetFRgwdE5NMqQUnIEHl8f22YfMo1bdPRCTZ62pGsDhR137/ferfukI2XrEhNcfFPy Q3a7lhYOIR1zP/Zn4EExCaQJGo9MLaFwLG9R2oFAh35P+/BfP7VXv76z0nHzA953d+Rr XNX7tmqgvcKWuCnWmRKPzX6AYPCnaL4uRypv4= MIME-Version: 1.0 Received: by 10.204.11.13 with SMTP id r13mr2392438bkr.96.1283099868214; Sun, 29 Aug 2010 09:37:48 -0700 (PDT) Received: by 10.204.54.68 with HTTP; Sun, 29 Aug 2010 09:37:48 -0700 (PDT) In-Reply-To: References: Date: Sun, 29 Aug 2010 12:37:48 -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=00032555539edb344f048ef8f7d7 X-Spam: no; 0.00; bug:01 toplevel:01 ocaml:01 typechecker:01 compiler:01 ocaml's:01 typechecker:01 runtime:01 ocaml's:01 toplevel:01 foo:01 foo:01 typecheck:01 annotations:01 typer:01 --00032555539edb344f048ef8f7d7 Content-Type: text/plain; charset=ISO-8859-1 bluestorm: Thank you for the bug report. The toplevel issue has been fixed in the version now posted. Do you see a nice way to add let-generalization without reintroducing "type levels"? I was pleased to remove those. Ivan: It was originally forked from Caml Light but now includes more code from OCaml. The typechecker is mostly original code at this point; the compiler is OCaml's with minimal changes to accommodate the new typechecker; the runtime is almost identical to OCaml's. -Jeremy On Sun, Aug 29, 2010 at 6:52 AM, bluestorm wrote: > When using the toplevel, declaration phrases fail (looks like a linking > problem), but expressions work as intented : > >> $ llama > > Llama Light version 0.0828 > > # 1 + 1;; > > - : int = 2 > > # let x = 1 + 1;; > > Error: Reference to undefined global `Toploop' > > > I made my tests using "llamac -i foo.ml". > > > I found it startling that the most important difference to my eyes are > buried, on the web page, under lines of relatively boring documentation : > > In Llama Light (and in contrast to other Caml implementations): > > >> - let does not generalize. > > - Phrases are generalized immediately. In particular, "let foo = ref []" >> does not typecheck. > > - The value restriction is not relaxed. (This is similar to Caml Light.) > > >> These choices simplify the implementation while having relatively little >> impact on the user. > > > You cite the "Let Should Not Be Generalised" paper. There is however a > difference in your application of the maxim : in the paper, local let that > have polymorphic type annotations are generalised, while in your system it > is not possible to force generalisation. > > I had a look at the typer, and it's indeed rather simple; it seems it would > be quite simple to implement generalized let (when encountering annotations > or with a different syntaxic construct : "letg .. = .. in ..."), but the > added complexity is equivalent to adding let generalization by default. > > Is the presence of let-generalization a real issue in your work ? > --00032555539edb344f048ef8f7d7 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
bluestorm:

Thank you for the bug report. =A0The to= plevel issue has been fixed in the version now posted.

Do you see a nice way to add let-generalization without reintroducing &q= uot;type levels"? =A0I was pleased to remove those.

Ivan:

It was originally forked= from Caml Light but now includes more code from OCaml. =A0The typechecker = is mostly original code at this point; the compiler is OCaml's with min= imal changes to accommodate the new typechecker; the runtime is almost iden= tical to OCaml's.

-Jeremy

On Sun= , Aug 29, 2010 at 6:52 AM, bluestorm <bluestorm.dylc@gmail.com> wrote:<= br>
When using the toplevel, declaration p= hrases fail (looks like a linking problem), but expressions work as intente= d :
$ llama
=A0=A0 =A0 =A0 =A0Llama Light version 0.0828
# 1 + 1;;
- : int =3D 2
# let x =3D 1 + 1;;
Error: Reference to undefined global `Toploop'

I m= ade my tests using "llamac -i foo.ml".


I found it startling tha= t the most important difference to my eyes are buried, on the web page, und= er lines of relatively boring documentation :

In Llama Light (and in contrast to other Caml implementations):

- let=A0does not generalize.
- Phrases are generalized immediately. In particular, "let foo =3D ref= []" does not typecheck.
- The value restriction is not=A0relaxed. (This is similar to Caml Light.)<= /blockquote>

These choices simplify the implementation while having relatively little im= pact on the user.

You cite the "Let Sh= ould Not Be Generalised" paper. There is however a difference in your = application of the maxim : in the paper, local let that have polymorphic ty= pe annotations are generalised, while in your system it is not possible to = force generalisation.

I had a look at the typer, and it's indeed rather s= imple; it seems it would be quite simple to implement generalized let (when= encountering annotations or with a different syntaxic construct : "le= tg .. =3D .. in ..."), but the added complexity is equivalent to addin= g let generalization by default.

Is the presence of let-generalization a real issue in y= our work ?

--00032555539edb344f048ef8f7d7--