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 4DC82BC57 for ; Sun, 29 Aug 2010 07:42:14 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkMCAAaQeUzRVdY0kGdsb2JhbACTOIUYiAUIFQEBAQEJCQwHEQMfnnuJJ4IThQ4uiFQBAQMFhTIEigk X-IronPort-AV: E=Sophos;i="4.56,286,1280700000"; d="scan'208";a="56139063" Received: from mail-bw0-f52.google.com ([209.85.214.52]) by mail3-smtp-sop.national.inria.fr with ESMTP; 29 Aug 2010 07:42:13 +0200 Received: by bwz5 with SMTP id 5so3644506bwz.39 for ; Sat, 28 Aug 2010 22:42:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:received:date:message-id :subject:from:to:content-type; bh=g+sp9w+E2OY/kLGtVrkMHyRKBGfcG86yZWtDgfdyURI=; b=bzcUIWDpKxv+CJKnZzE685oDO1S9N037XFOFyzql6kUtCiRo9DpCmqfsp3n+U32B5k MPwH/dmbOuOW6LRuR4bo90slJ9woBSZJhVIv3mUq+ffpVx6hcmwKoj8MpxLV6RNCfYRq xRBO3f/GLG7TeNokOUfuhc2nQOolT46gxYP+E= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=KU7Vt2cpYs6KRJva8QIk4b7gSosA0l2aCcPd3PIehRfb28ouMcmXpJ+tWdYHUz6dzx fOI7CyDEGb3MX7J7vZemRIypwpQDfcI23vEIZMxLpwayt6uooLG2fUitfjAOOhe55Wra VaLY66Q8erQtDrYD12BMLLrTKQJyo/w+F4Y7A= MIME-Version: 1.0 Received: by 10.204.6.75 with SMTP id 11mr2008417bky.95.1283060532910; Sat, 28 Aug 2010 22:42:12 -0700 (PDT) Received: by 10.204.54.68 with HTTP; Sat, 28 Aug 2010 22:42:12 -0700 (PDT) Date: Sun, 29 Aug 2010 01:42:12 -0400 Message-ID: Subject: Llama Light: a simple implementation of Caml From: Jeremy Bem To: caml-list List Content-Type: multipart/alternative; boundary=000e0cd1d1244a1aa2048eefcfec X-Spam: no; 0.00; typechecker:01 ocaml:01 typechecker:01 ocaml:01 caml-list:01 caml-list:01 caml:02 caml:02 let:03 let:03 modify:05 modify:05 derived:05 derived:05 inria:06 --000e0cd1d1244a1aa2048eefcfec Content-Type: text/plain; charset=ISO-8859-1 Dear caml-list, I'm pleased to announce Llama Light, an implementation of the core Caml language. It features a typechecker that is small enough to read through and grasp as a whole, thereby making it easy to modify and extend. Llama Light is derived from Caml Light and OCaml. I'm grateful to the developers at INRIA for allowing derivative works to be created. The system is available for download at http://llamalabs.org/light.html. All feedback is greatly appreciated (even if it's just to let me know that you tried it out). Thanks! -Jeremy --000e0cd1d1244a1aa2048eefcfec Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Dear caml-list,

I'm pleased to announce L= lama Light, an implementation of the core Caml language. =A0It features a t= ypechecker that is small enough to read through and grasp as a whole, there= by making it easy to modify and extend.

Llama Light is derived from Caml Light and OCaml. =A0I&= #39;m grateful to the developers at INRIA for allowing derivative works to = be created.

The system is available for download a= t http://llam= alabs.org/light.html. =A0All feedback is greatly appreciated (even if i= t's just to let me know that you tried it out).

Thanks!
-Jeremy
--000e0cd1d1244a1aa2048eefcfec-- 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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id BD1C7BC57 for ; Sun, 29 Aug 2010 12:52:47 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AggCADbYeUzRVditkGdsb2JhbACYPQGIBAgVAQEBAQkJDAcRAx+dZ4knghOFHC6IVAEBAwWFMgSEb4UaiE8 X-IronPort-AV: E=Sophos;i="4.56,286,1280700000"; d="scan'208";a="68331997" Received: from mail-qy0-f173.google.com ([209.85.216.173]) by mail4-smtp-sop.national.inria.fr with ESMTP; 29 Aug 2010 12:52:47 +0200 Received: by qyk5 with SMTP id 5so2511099qyk.18 for ; Sun, 29 Aug 2010 03:52:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:mime-version:sender:received :in-reply-to:references:from:date:x-google-sender-auth:message-id :subject:to:cc:content-type; bh=2HAolr9X7nig9a9LaEvzS9SQu5/13Bh7ba3MKGG98YI=; b=nqFz/pku7grmbrrUMEBU0UQlEX9xIdWiLuUwAvQJugrbRZXUeqrGQ9ve/wmrif9OaX Ji9GduoL5wtDGA4qp0RqqZYJ3dKGJ6PLE0U6oPxtZ0fSAvpwTvVe0lQxAHkTE56QYyDR 5A7z7kX2F0uuindVYUz4TUlhwJrRJGpX7ta8s= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=medhroKTg18TyjWQ/M4Gf5kHGjODsHZyTvbXmnf/+qFmO0pwSxSNQgzOoZwaZugOme ICfdhB3tBZ1dVSM80elQpmbTO3yqQ4eth1fnXtk+Tdggii1J619Dt88RBFW/8ozsyeef TJDgtwAJqcq3gYzsAis90rJwgaQcdyMaDp2s8= Received: by 10.229.213.131 with SMTP id gw3mr849526qcb.9.1283079162159; Sun, 29 Aug 2010 03:52:42 -0700 (PDT) MIME-Version: 1.0 Sender: gabriel.scherer@gmail.com Received: by 10.229.185.206 with HTTP; Sun, 29 Aug 2010 03:52:22 -0700 (PDT) In-Reply-To: References: From: bluestorm Date: Sun, 29 Aug 2010 12:52:22 +0200 X-Google-Sender-Auth: N_6XUaxfevQrG8jxDv-nZKu835g Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml To: Jeremy Bem Cc: caml-list List Content-Type: multipart/alternative; boundary=0016361e8270adeaae048ef425a5 X-Spam: no; 0.00; toplevel:01 foo:01 foo:01 typecheck:01 annotations:01 typer:01 annotations:01 toplevel:01 typecheck:01 typer:01 maxim:98 maxim:98 polymorphic:01 polymorphic:01 caml-list:01 --0016361e8270adeaae048ef425a5 Content-Type: text/plain; charset=ISO-8859-1 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 ? --0016361e8270adeaae048ef425a5 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
When using the toplevel, declaration phrases fail (looks like a linkin= g problem), but expressions work as intented :
$ 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&quo= t;.


I found it startling that the most importa= nt difference to my eyes are buried, on the web page, under lines of relati= vely 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 ?
--0016361e8270adeaae048ef425a5-- 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 B6C50BC58 for ; Sun, 29 Aug 2010 15:01:03 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhICAGT3eUzRVda0kGdsb2JhbACSczKFGAGIBAgVAQEBAQkJDAcRAx+eD4knghOFJC6IVAEBAwWFMgSBV4gy X-IronPort-AV: E=Sophos;i="4.56,287,1280700000"; d="scan'208";a="57939121" Received: from mail-iw0-f180.google.com ([209.85.214.180]) by mail2-smtp-roc.national.inria.fr with ESMTP; 29 Aug 2010 15:00:57 +0200 Received: by iwn6 with SMTP id 6so5519757iwn.39 for ; Sun, 29 Aug 2010 06:00:54 -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=UCyO9+QSJD/+B3htSSkM6uX7WU8S9wkv9QTlR8cGpR0=; b=L1JLAzwiNi5yw1rJFJr/ZwjeL3AyWaMh+pPr3mJoURfQoZjWHLEOmTWtZ9WtVvixmR rSQQHcFQb1ugWP8TyOvTO3wecmy3iIE/Goxci08cE5Dsmz0sERtOpXbA5608A4LD++Wd 9wHVKO+lYPVTqSNV1C6XSxOBbxsw7vDp9+/oo= 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=opZ/mr3eoE79mEYepgxjLv3pSRfphC9qBwOVcIMFXZ3Fy2JBiJmJC6dydsnNjd097D kaY554YYER8hVYb2SprGrDIIlXXUmeZdy9NDi/Va813QhEVIfPhioshZJrvKCEnSQrIi m9B0RP2ED3EGkh8yYbQCdM/dt7bXD2liX4utE= MIME-Version: 1.0 Received: by 10.231.146.134 with SMTP id h6mr3758655ibv.170.1283086853429; Sun, 29 Aug 2010 06:00:53 -0700 (PDT) Received: by 10.231.153.147 with HTTP; Sun, 29 Aug 2010 06:00:53 -0700 (PDT) In-Reply-To: References: Date: Sun, 29 Aug 2010 23:00:53 +1000 Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml From: ivan chollet To: Jeremy Bem Cc: caml-list List Content-Type: multipart/alternative; boundary=0016e64806781d5d59048ef5f09e X-Spam: no; 0.00; runtime:01 typechecker:01 ocaml:01 beginner's:01 ocaml:01 bug:01 runtime:01 typechecker:01 beginner's:01 bug:01 beginners:01 beginners:01 wrote:01 wrote:01 caml-list:01 --0016e64806781d5d59048ef5f09e Content-Type: text/plain; charset=ISO-8859-1 Hi, Is it just a fork on Caml light or a new implementation and runtime? Regards On Sun, Aug 29, 2010 at 3:42 PM, Jeremy Bem wrote: > Dear caml-list, > > I'm pleased to announce Llama Light, an implementation of the core Caml > language. It features a typechecker that is small enough to read through > and grasp as a whole, thereby making it easy to modify and extend. > > Llama Light is derived from Caml Light and OCaml. I'm grateful to the > developers at INRIA for allowing derivative works to be created. > > The system is available for download at http://llamalabs.org/light.html. > All feedback is greatly appreciated (even if it's just to let me know that > you tried it out). > > Thanks! > -Jeremy > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --0016e64806781d5d59048ef5f09e Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hi,

Is it just a fork on Caml light or a new implementation and runt= ime?

Regards



On Sun, Aug 2= 9, 2010 at 3:42 PM, Jeremy Bem <jeremy1@gmail.com> wrote:
Dear caml-li= st,

I'm pleased to announce Llama Light, an im= plementation of the core Caml language. =A0It features a typechecker that i= s small enough to read through and grasp as a whole, thereby making it easy= to modify and extend.

Llama Light is derived from Caml Light and OCaml. =A0I&= #39;m grateful to the developers at INRIA for allowing derivative works to = be created.

The system is available for download a= t http://llam= alabs.org/light.html. =A0All feedback is greatly appreciated (even if i= t's just to let me know that you tried it out).

Thanks!
-Jeremy

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.in= ria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--0016e64806781d5d59048ef5f09e-- 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-- 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-- 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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 55875BC57 for ; Mon, 30 Aug 2010 12:57:26 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai8CAB4re0zRVditkGdsb2JhbACScoVKAYd6CBUBAQEBCQkMBxEDH559iSeCE4VHLohUAQEDBYUyBIFXgxiFGg X-IronPort-AV: E=Sophos;i="4.56,292,1280700000"; d="scan'208";a="68362041" Received: from mail-qy0-f173.google.com ([209.85.216.173]) by mail4-smtp-sop.national.inria.fr with ESMTP; 30 Aug 2010 12:57:25 +0200 Received: by qyk5 with SMTP id 5so3356932qyk.18 for ; Mon, 30 Aug 2010 03:57:24 -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=1aPv9PitwFJVj9Z07Ulp9fI84RriSY55KAgxGBku9SE=; b=WrY92/qNheHzE59ddGL7biGgtBCzB7JpNNX7vzq74bpE0J8xNM/LZU63bsn4TfqhxF QhqM5RqaCCrfVLxBdUFtvIu6ELVOMMXXgfh7tV/nztj5VKs/+VC99tIKp84aAK3Q4IuL XxRGoLy/L9HoktrqAZDeanxeeuaXgN9/zTxQY= 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=OwIf6Y/nBi1c77kIQ2QS9EPGOpaESzOdLxv17re32Qcdducyf6ovh4+iShyXsIIu8F hNnwWqxwTYbr9f3+jV8NHj4uAbdzHIHSqx0ejL14gdtuQ0l4eEowp1qKWfEotgkyYwea RXf5j5xrD974uI5cnOnUIUV79mqBMsjhFbSs4= MIME-Version: 1.0 Received: by 10.229.251.210 with SMTP id mt18mr2949524qcb.151.1283165844039; Mon, 30 Aug 2010 03:57:24 -0700 (PDT) Received: by 10.229.218.19 with HTTP; Mon, 30 Aug 2010 03:57:23 -0700 (PDT) In-Reply-To: References: Date: Mon, 30 Aug 2010 20:57:23 +1000 Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml From: ivan chollet To: Jeremy Bem Cc: bluestorm , caml-list List Content-Type: multipart/alternative; boundary=00163631036f526806048f0854db X-Spam: no; 0.00; pointers:01 typechecker:01 ocaml:01 typechecker:01 runtime:01 bytecode:01 compiler:01 bug:01 toplevel:01 ocaml:01 compiler:01 ocaml's:01 runtime:01 ocaml's:01 toplevel:01 --00163631036f526806048f0854db Content-Type: text/plain; charset=ISO-8859-1 OK. This looks nice and I would be pleased if you could put a few pointers or explanations on your webpage about your typechecker implementation and how it differs with OCaml typechecker. I will get some free time this week and to implement yet another runtime and bytecode compiler from scratch. Not sure if it will be completed at the end of the week, but i'll be definitely interested to know more about the theoretical motivations of works like yours! On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem wrote: > 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 ? >> > > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --00163631036f526806048f0854db Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable OK.

This looks nice and I would be pleased if you could put a few po= inters or explanations on your webpage about your typechecker implementatio= n and how it differs with OCaml typechecker.
I will get some free time = this week and to implement yet another runtime and bytecode compiler from s= cratch. Not sure if it will be completed at the end of the week, but i'= ll be definitely interested to know more about the theoretical motivations = of works like yours!



On Mon, Aug 30, 2010 at 2:37 AM, Jer= emy Bem <jeremy1@= gmail.com> wrote:
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
<= /div>

On Sun, Aug 29, = 2010 at 6:52 AM, bluestorm <bluestorm.dylc@gmail.com>= wrote:
When using t= he toplevel, declaration phrases fail (looks like a linking problem), but e= xpressions work as intented :
$ 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 ?


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.in= ria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--00163631036f526806048f0854db-- 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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C5EE4BC57 for ; Mon, 30 Aug 2010 17:57:29 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmcCAG5xe0xKfVIuimdsb2JhbACBQ5EygU6DfAGHeggVAQEBCgkMBw8FH6InizoBBY5cAQSFN4Fbgxg X-IronPort-AV: E=Sophos;i="4.56,293,1280700000"; d="scan'208,217";a="68378444" Received: from mail-ww0-f46.google.com ([74.125.82.46]) by mail4-smtp-sop.national.inria.fr with ESMTP; 30 Aug 2010 17:57:29 +0200 Received: by wwb18 with SMTP id 18so2924634wwb.3 for ; Mon, 30 Aug 2010 08:57:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=gamma; h=domainkey-signature:received:received:from:to:cc:references :in-reply-to:subject:date:organization:message-id:mime-version :content-type:x-mailer:thread-index:content-language; bh=2GtzX9/O9T7pp6hNZ2TCfOmUtVBv+IsUkTWXDHLlaGA=; b=cB2LtGa7hN13XeCwZ+leCczuk2U4mcg2uamfjGd8ctunU5slWIFfUKCNx9PdpoGjXq oRgMcsfWmwE8EPBbeLgBEqNoWpDG3J/r4IvCkh8ry80fDtRRQQjAydb3CGSw/7Xp5rx1 XY4cTTjBDZZlCwlcOW/CQuIoIbe6aYZGiSnTc= DomainKey-Signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=from:to:cc:references:in-reply-to:subject:date:organization :message-id:mime-version:content-type:x-mailer:thread-index :content-language; b=MFRpPXeEtHdXGFdSJRTGgMsnOtqUSctd3nZx3Sp+dCFnz+huXA1LI32JZf+c2FQ+7I wWl/8zc9fUvTisw/kcIp6+ugvl5cGklK/evvwVSQ/lLDt6nUCKXBV6vcoiLbUiORLD6F j0wBsnOrOf74zhhauD/wC0duZfSe4t7eMH8nA= Received: by 10.227.208.85 with SMTP id gb21mr4544302wbb.167.1283183847172; Mon, 30 Aug 2010 08:57:27 -0700 (PDT) Received: from WinEight ([87.113.136.121]) by mx.google.com with ESMTPS id w1sm4549152weq.1.2010.08.30.08.57.23 (version=SSLv3 cipher=RC4-MD5); Mon, 30 Aug 2010 08:57:24 -0700 (PDT) From: Jon Harrop To: "'ivan chollet'" , "'Jeremy Bem'" Cc: "'caml-list List'" References: In-Reply-To: Subject: RE: [Caml-list] Llama Light: a simple implementation of Caml Date: Mon, 30 Aug 2010 16:57:04 +0100 Organization: Flying Frog Consultancy Message-ID: <026901cb485b$ff1b8ad0$fd52a070$@com> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_NextPart_000_026A_01CB4864.60DFF2D0" X-Mailer: Microsoft Office Outlook 12.0 Thread-Index: ActIMjODNbUYxsFRRf2gzu8KyGQrCQAKOQVg Content-Language: en-gb X-Spam: no; 0.00; run-time:01 compiler:01 recursion:01 cheers:01 pointers:01 typechecker:01 ocaml:01 typechecker:01 runtime:01 bytecode:01 compiler:01 bug:01 toplevel:01 ocaml:01 ocaml's:01 This is a multi-part message in MIME format. ------=_NextPart_000_026A_01CB4864.60DFF2D0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Try to remove all assumptions of uniform run-time representation from the compiler because avoiding boxing gives huge performance gains and makes it much easier to write a performant garbage collector. You'll need to sacrifice polymorphic recursion though, which you probably already have anyway. Cheers, Jon. From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan chollet Sent: 30 August 2010 11:57 To: Jeremy Bem Cc: caml-list List Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml OK. This looks nice and I would be pleased if you could put a few pointers or explanations on your webpage about your typechecker implementation and how it differs with OCaml typechecker. I will get some free time this week and to implement yet another runtime and bytecode compiler from scratch. Not sure if it will be completed at the end of the week, but i'll be definitely interested to know more about the theoretical motivations of works like yours! On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem wrote: 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 ? _______________________________________________ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs ------=_NextPart_000_026A_01CB4864.60DFF2D0 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

Try to remove all assumptions of uniform run-time = representation from the compiler because avoiding boxing gives huge performance gains = and makes it much easier to write a performant garbage collector. = You’ll need to sacrifice polymorphic recursion though, which you probably already = have anyway…

 

Cheers,

Jon.

 

From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan = chollet
Sent: 30 August 2010 11:57
To: Jeremy Bem
Cc: caml-list List
Subject: Re: [Caml-list] Llama Light: a simple implementation of = Caml

 

OK.

This looks nice and I would be pleased if you could put a few pointers = or explanations on your webpage about your typechecker implementation and = how it differs with OCaml typechecker.
I will get some free time this week and to implement yet another runtime = and bytecode compiler from scratch. Not sure if it will be completed at the = end of the week, but i'll be definitely interested to know more about the = theoretical motivations of works like yours!


On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem <jeremy1@gmail.com> = wrote:

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 <bluestorm.dylc@gmail.com> 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 =3D 2

# let x =3D 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 =3D 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 .. =3D = .. 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 ?

 


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-lis= t
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

 

------=_NextPart_000_026A_01CB4864.60DFF2D0-- 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 9116EBC57 for ; Mon, 30 Aug 2010 19:09:39 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkoCAFKCe0zRVdi0kGdsb2JhbACBRJExhUoBhzdDCBUBAQEBCQkMBxEDH6J/iSeCE4V5LohUAQEDBYUyBIFXgxiFGg X-IronPort-AV: E=Sophos;i="4.56,293,1280700000"; d="scan'208";a="57993694" Received: from mail-qy0-f180.google.com ([209.85.216.180]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Aug 2010 19:09:38 +0200 Received: by qyk31 with SMTP id 31so6658344qyk.18 for ; Mon, 30 Aug 2010 10:09:38 -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=kjidYJztplh7r4xAiLAqvfug3gliX6LHeImLTJZ3cbY=; b=K1P9S83lZq4Fy5z6y3CKl03iNGgM9jHJPg3yLlzAOrX4c00OYQkcuFHYe0Hq9CvLGx +1AIir0gj3ANWkAg75NlP3GswMLpjyWgdP2yqkUsXCOc5OmZwjVVNSTRlK/l9ZWZQdXN L6DLX9P90E/y+LGwyLBsAflcNpPBw7DhGKLZ8= 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=nPfy9Y/RK/CDTIF0l5V+J5xKSikykb3jdOlt6Vog8kssBqQ/3FLCHUvkNFBVHU6v1H WElfJR23hJ/Ru0f40KCgPuWtDCsolPv10495BHTMHYGOVAsAmU5T04jVc4IvLvVJNs65 mySBzg5Uu8Yrv0s5YO/1Z/ycJ2hYYDx84M6AY= MIME-Version: 1.0 Received: by 10.229.52.32 with SMTP id f32mr3217797qcg.265.1283188177646; Mon, 30 Aug 2010 10:09:37 -0700 (PDT) Received: by 10.229.218.19 with HTTP; Mon, 30 Aug 2010 10:09:37 -0700 (PDT) In-Reply-To: <026901cb485b$ff1b8ad0$fd52a070$@com> References: <026901cb485b$ff1b8ad0$fd52a070$@com> Date: Tue, 31 Aug 2010 03:09:37 +1000 Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml From: ivan chollet To: Jon Harrop Cc: Jeremy Bem , caml-list List Content-Type: multipart/alternative; boundary=0016367d5ba882673f048f0d872d X-Spam: no; 0.00; recursion:01 pointers:01 run-time:01 compiler:01 recursion:01 cheers:01 pointers:01 typechecker:01 ocaml:01 typechecker:01 runtime:01 bytecode:01 compiler:01 bug:01 toplevel:01 --0016367d5ba882673f048f0d872d Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable clearly didn't plan to support polymorphic recursion in any way. I don't even plan to support lexical scoping... As for data representation I'm actually boxing everything except ints and function pointers. I found out that it leads to the simplest design, which is appropriate for a project that I don't want to take me more than a few days. On Tue, Aug 31, 2010 at 1:57 AM, Jon Harrop < jonathandeanharrop@googlemail.com> wrote: > Try to remove all assumptions of uniform run-time representation from th= e > compiler because avoiding boxing gives huge performance gains and makes i= t > much easier to write a performant garbage collector. You=92ll need to > sacrifice polymorphic recursion though, which you probably already have > anyway=85 > > > > Cheers, > > Jon. > > > > *From:* caml-list-bounces@yquem.inria.fr [mailto: > caml-list-bounces@yquem.inria.fr] *On Behalf Of *ivan chollet > *Sent:* 30 August 2010 11:57 > *To:* Jeremy Bem > *Cc:* caml-list List > *Subject:* Re: [Caml-list] Llama Light: a simple implementation of Caml > > > > OK. > > This looks nice and I would be pleased if you could put a few pointers or > explanations on your webpage about your typechecker implementation and ho= w > it differs with OCaml typechecker. > I will get some free time this week and to implement yet another runtime > and bytecode compiler from scratch. Not sure if it will be completed at t= he > end of the week, but i'll be definitely interested to know more about the > theoretical motivations of works like yours! > > > On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem wrote: > > 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 "ty= pe > 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 compil= er > 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 =3D 2 > > # let x =3D 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 =3D 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 tha= t > have polymorphic type annotations are generalised, while in your system i= t > is not possible to force generalisation. > > > > I had a look at the typer, and it's indeed rather simple; it seems it wou= ld > be quite simple to implement generalized let (when encountering annotatio= ns > or with a different syntaxic construct : "letg .. =3D .. in ..."), but th= e > added complexity is equivalent to adding let generalization by default. > > > > Is the presence of let-generalization a real issue in your work ? > > > > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > > --0016367d5ba882673f048f0d872d Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: quoted-printable clearly didn't plan to support polymorphic recursion in any way. I don&= #39;t even plan to support lexical scoping...
As for data representation= I'm actually boxing everything except ints and function pointers. I fo= und out that it leads to the simplest design, which is appropriate for a pr= oject that I don't want to take me more than a few days.


On Tue, Aug 31, 2010 at 1:57 AM, Jon Har= rop <jonathandeanharrop@googlemail.com> wrote:

Try to remove all assumptions of uniform run-time representation from the compiler because avoiding boxing gives huge performance gains and makes it much easier to write a performant garbage collector. You=92ll need to sacrifice polymorphic recursion though, which you probably already have anyway=85

=A0

Cheers,

Jon.

=A0

F= rom: caml-list-bounce= s@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan chollet Sent: 30 August 2010 11:57
To: Jeremy Bem
Cc: caml-list List
Subject: Re: [Caml-list] Llama Light: a simple implementation of Cam= l

=A0

OK.

This looks nice and I would be pleased if you could put a few pointers or explanations on your webpage about your typechecker implementation and how = it differs with OCaml typechecker.
I will get some free time this week and to implement yet another runtime an= d bytecode compiler from scratch. Not sure if it will be completed at the end= of the week, but i'll be definitely interested to know more about the theo= retical motivations of works like yours!


On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem <jeremy1@gmail.com>= ; wrote:

bluestorm:

=A0

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

=A0

Do you see a nice way to add let-generalization with= out reintroducing "type levels"? =A0I was pleased to remove those.

=A0

Ivan:

=A0

It was originally forked from Caml Light but now inc= ludes more code from OCaml. =A0The 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.

=A0

-Jeremy

=A0

On Sun, Aug 29, 2010 at 6:52 AM, bluestorm <bluestorm.dylc@gma= il.com> wrote:

When using the toplevel, declaration phrases fail (l= ooks like a linking problem), but expressions work as intented :

$ 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'

=A0

I made my tests using "llamac -i foo.ml".

=A0


I found it startling that the most important difference to my eyes are buri= ed, on the web page, under lines of relatively boring documentation :

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

=A0

- 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.)

=A0

These choices simplify the implementation while havi= ng relatively little impact on the user.

=A0

You cite the "Let Should Not Be Generalised&quo= t; paper. There is however a difference in your application of the maxim : in = the paper, local let that have polymorphic type annotations are generalised, wh= ile in your system it is not possible to force generalisation.

=A0

I had a look at the typer, and it's indeed rathe= r simple; it seems it would be quite simple to implement generalized let (when encounter= ing annotations or with a different syntaxic construct : "letg .. =3D .. i= n ..."), but the added complexity is equivalent to adding let generaliza= tion by default.

=A0

Is the presence of let-generalization a real issue i= n your work ?

=A0


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.in= ria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

=A0


--0016367d5ba882673f048f0d872d-- 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 E780EBC57 for ; Mon, 30 Aug 2010 19:39:44 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgQCAFuJe0zRVde0mWdsb2JhbACBRJEzgU6DfAGHeggVAQEBAQEICwoHESKjPos6AQWPAAEEhTeBW4MY X-IronPort-AV: E=Sophos;i="4.56,294,1280700000"; d="scan'208,217";a="57994826" Received: from mail-ey0-f180.google.com ([209.85.215.180]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Aug 2010 19:39:44 +0200 Received: by eya25 with SMTP id 25so4131948eya.39 for ; Mon, 30 Aug 2010 10:39:43 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=gamma; h=domainkey-signature:received:received:from:to:cc:references :in-reply-to:subject:date:organization:message-id:mime-version :content-type:x-mailer:thread-index:content-language; bh=H5umcyfu3gGw1TAGruzGzEmPhsbbXGxTNeLQvYw76pg=; b=ha1SN0KCiPDitkeTG/msNNtfOfxydRicxQ7BtnKXBUVPWH2YzLtJ6AyjNnOw8wKdcr n1lIzUGBFNquE3S1aZU7xdwKAHsdToxlttRAzr4wu0ZiwM09SDCKV+uyR5N9BrsjOek4 XxD9qHhrvsdOTTTLQtBaMN29FJY4FudsEN+nw= DomainKey-Signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=from:to:cc:references:in-reply-to:subject:date:organization :message-id:mime-version:content-type:x-mailer:thread-index :content-language; b=LhGqnqc9fH3whcd8d/tUcDsxb9FB6u8GzFqrwpFhtt18yVhqjVTwkWTDWBGhOTaDqb /hMmnPoigKILHK1p1vwvPhOGh63qvEIWUjHvfWu2wvKvWo2MzVXAnJd7A88+U3/3+iJ2 94C21zgD+DW+VPqtGeCqoF0SrxwxKni3djyB4= Received: by 10.216.188.81 with SMTP id z59mr5180607wem.106.1283189982370; Mon, 30 Aug 2010 10:39:42 -0700 (PDT) Received: from WinEight ([87.113.136.121]) by mx.google.com with ESMTPS id n40sm4621787weq.29.2010.08.30.10.39.39 (version=SSLv3 cipher=RC4-MD5); Mon, 30 Aug 2010 10:39:41 -0700 (PDT) From: Jon Harrop To: "'ivan chollet'" , "'Jon Harrop'" Cc: "'Jeremy Bem'" , "'caml-list List'" References: <026901cb485b$ff1b8ad0$fd52a070$@com> In-Reply-To: Subject: RE: [Caml-list] Llama Light: a simple implementation of Caml Date: Mon, 30 Aug 2010 18:39:20 +0100 Organization: Flying Frog Consultancy Message-ID: <027401cb486a$48511e00$d8f35a00$@com> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_NextPart_000_0275_01CB4872.AA158600" X-Mailer: Microsoft Office Outlook 12.0 Thread-Index: ActIZiCKqvJUmmSVSaG6vG4Vv2+0WwAAzKcA Content-Language: en-gb X-Spam: no; 0.00; parallelism:01 cheers:01 recursion:01 pointers:01 run-time:01 compiler:01 recursion:01 cheers:01 pointers:01 typechecker:01 ocaml:01 typechecker:01 runtime:01 bytecode:01 compiler:01 This is a multi-part message in MIME format. ------=_NextPart_000_0275_01CB4872.AA158600 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit If you can keep it agnostic wrt boxing then you should be able to plug it into HLVM easily for much faster numerics and parallelism. Cheers, Jon. From: ivan chollet [mailto:ivan.chollet@gmail.com] Sent: 30 August 2010 18:10 To: Jon Harrop Cc: Jeremy Bem; caml-list List Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml clearly didn't plan to support polymorphic recursion in any way. I don't even plan to support lexical scoping... As for data representation I'm actually boxing everything except ints and function pointers. I found out that it leads to the simplest design, which is appropriate for a project that I don't want to take me more than a few days. On Tue, Aug 31, 2010 at 1:57 AM, Jon Harrop wrote: Try to remove all assumptions of uniform run-time representation from the compiler because avoiding boxing gives huge performance gains and makes it much easier to write a performant garbage collector. You'll need to sacrifice polymorphic recursion though, which you probably already have anyway. Cheers, Jon. From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan chollet Sent: 30 August 2010 11:57 To: Jeremy Bem Cc: caml-list List Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml OK. This looks nice and I would be pleased if you could put a few pointers or explanations on your webpage about your typechecker implementation and how it differs with OCaml typechecker. I will get some free time this week and to implement yet another runtime and bytecode compiler from scratch. Not sure if it will be completed at the end of the week, but i'll be definitely interested to know more about the theoretical motivations of works like yours! On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem wrote: 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 ? _______________________________________________ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs ------=_NextPart_000_0275_01CB4872.AA158600 Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

If you can keep it agnostic wrt boxing then you should be = able to plug it into HLVM easily for much faster numerics and = parallelism.

 

Cheers,

Jon.

 

From: ivan chollet [mailto:ivan.chollet@gmail.com]
Sent: 30 August 2010 18:10
To: Jon Harrop
Cc: Jeremy Bem; caml-list List
Subject: Re: [Caml-list] Llama Light: a simple implementation of = Caml

 

clearly didn't plan = to support polymorphic recursion in any way. I don't even plan to support lexical scoping...
As for data representation I'm actually boxing everything except ints = and function pointers. I found out that it leads to the simplest design, = which is appropriate for a project that I don't want to take me more than a few = days.

On Tue, Aug 31, 2010 at 1:57 AM, Jon Harrop <jonathandeanharrop@goog= lemail.com> wrote:

Try to remove all assumptions = of uniform run-time representation from the compiler because avoiding boxing gives = huge performance gains and makes it much easier to write a performant garbage = collector. You’ll need to sacrifice polymorphic recursion though, which you = probably already have anyway…

 

Cheers,

Jon.

 

From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan chollet
Sent: 30 August 2010 11:57
To: Jeremy Bem
Cc: caml-list List
Subject: Re: [Caml-list] Llama Light: a simple implementation of = Caml

 <= /o:p>

OK.

This looks nice and I would be pleased if you could put a few pointers = or explanations on your webpage about your typechecker implementation and = how it differs with OCaml typechecker.
I will get some free time this week and to implement yet another runtime = and bytecode compiler from scratch. Not sure if it will be completed at the = end of the week, but i'll be definitely interested to know more about the = theoretical motivations of works like yours!

On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem <jeremy1@gmail.com> wrote:

bluestorm:

 <= /o:p>

Thank you for the bug report.  The toplevel issue has been fixed in the = version now posted.

 <= /o:p>

Do you see a nice way to add let-generalization without reintroducing = "type levels"?  I was pleased to remove those.

 <= /o:p>

Ivan:

 <= /o:p>

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.

 <= /o:p>

-Jeremy

 <= /o:p>

On Sun, Aug 29, 2010 at 6:52 AM, bluestorm <bluestorm.dylc@gmail.com> 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 =3D 2

# let x =3D 1 + 1;;

Error: Reference to undefined global `Toploop'

 <= /o:p>

I made my tests using "llamac -i foo.ml".

 <= /o:p>


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):

 <= /o:p>

- let does not generalize.

- Phrases are generalized immediately. In particular, "let foo =3D = ref []" does not typecheck.

- The value restriction is not relaxed. (This is similar to Caml = Light.)

 <= /o:p>

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

 <= /o:p>

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.

 <= /o:p>

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 .. =3D .. in = ..."), but the added complexity is equivalent to adding let generalization by = default.

 <= /o:p>

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

 <= /o:p>


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-lis= t
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

 <= /o:p>

 

------=_NextPart_000_0275_01CB4872.AA158600-- 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 5EBADBC57 for ; Mon, 30 Aug 2010 22:49:52 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqABAN+1e0zRVdY0kGdsb2JhbACgYQgVAQEBAQkJDAcRAx+kRoknghOGJy6IVAEBAwWFMgSKCQ X-IronPort-AV: E=Sophos;i="4.56,294,1280700000"; d="scan'208";a="58000218" Received: from mail-bw0-f52.google.com ([209.85.214.52]) by mail2-smtp-roc.national.inria.fr with ESMTP; 30 Aug 2010 22:49:51 +0200 Received: by bwz5 with SMTP id 5so4978572bwz.39 for ; Mon, 30 Aug 2010 13:49: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=da0CrUEQIqutKd43D5yXpXUdtDe4hw74f6jY5QIRzmg=; b=ry4ohiEEb8LZ0WAKmK/HArTPCcBSbRYC4a1MZjiD2vJGnXCAHPKxnj8myHa27aZxu/ TMyL9RkweMm+0sYgZDXhYjy9m6NvgTd7Uv8pSwxv0jXiALCQTP5cYaG1FJbD2j0TbRQW /SduPgJ288Glk4ffU8k478pVMjrPHAfNXbc0c= 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=pB4mZjO0ulLDZ/jMv090TZSu0bTG9q6FRDTPQHJvfPbhyxtdEUXbEdcPj+CIZ/Ue8m CfNG/oX3xcJ0qlCb21/jIqjCwmbgAjINE2baKrg2prbpR2B9vdhBIog+NRgPnI0angzP 2QflHEMq1FXvnQPsoS3e2wwu7Gy1RPpJ39BfU= MIME-Version: 1.0 Received: by 10.204.104.5 with SMTP id m5mr3805372bko.73.1283201391051; Mon, 30 Aug 2010 13:49:51 -0700 (PDT) Received: by 10.204.128.213 with HTTP; Mon, 30 Aug 2010 13:49:50 -0700 (PDT) In-Reply-To: References: Date: Mon, 30 Aug 2010 16:49:50 -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=0016e6d7e13d16ce32048f109bfd X-Spam: no; 0.00; lambda:01 occurences:01 polymorphism:01 haskell:01 polymorphism:01 ocaml:01 binders:01 lambda:01 binders:01 functors:01 occurences:01 haskell:01 ocaml:01 functors:01 rung:98 --0016e6d7e13d16ce32048f109bfd Content-Type: text/plain; charset=ISO-8859-1 [Re-adding caml-list: I thought this conversation about let-polymorphism might be of wider interest.] The "stability" property you mention is nice, but of course if you don't have let-polymorphism then you get a different handy rewrite, namely the equivalence of let x = e1 in e2 and (fun x -> e2) e1 no? I was surprised when I first realized this didn't hold in ML. In your last paragraph, you seem to elide the distinction between monomorphic and polymorphic let, implying that both are the bottom rung of the type hierarchy...but I'm proposing that polymorphic let is already an extension of a simpler system. Does polymorphic let not seem "richer" than lambda to you? It certainly seems to me to affect the metatheory (although recently I've been thinking more about set-theoretic sematics than the usual type-theoretic properties). Maybe I'm splitting hairs...overall it still seems reasonable to me to exclude let-polymorphism from Llama Light, considering that the goal is be a minimal base system, and this one appears to be perfectly practical. I can't tell whether you disagree with this. -Jeremy On Mon, Aug 30, 2010 at 4:06 PM, bluestorm wrote: > On Mon, Aug 30, 2010 at 7:03 PM, Jeremy Bem wrote: > > Right...thanks for the refresher. I suppose I should implement this, as > > technically it is not "ML" until I do. I'm still wondering why this is > > considered an essential and desirable feature. > > One reason it is interesting is that it gives you the following > stability property, > wich is good for refactoring (both by humans and by copmuters) for example > : > > let x = e1 in e2 is equivalent to e2{x <- e1} (e2 in wich > all free occurences of x are replaced by e1) > > If let isn't polymorphic, then for example let id x = x in (id 1, id > 2) doesn't work out. > > There are other cases where polymorphism may be useful locally. For > example in Haskell, the ST monad use polymorphism to encode an > information about the use of effects in your code : if all effect are > used locally (so the function is "observationally pure", or > "referentially transparent", while still using side effects inside), > the result will be polymorphic in the state parameter of the ST monad. > If it's not, we know a side effect has escaped, and the type system > forbids you from "running" the monad. > > > > If one can make local polymorphic definitions, why > > not local types and local exceptions? > > In OCaml you can have local types and exceptions through the "let > module = .. in .." construct. > > Note however that, on a "richness of the type system" scale, they're > much higher in the hierarchy. Binders on value (lambda and let) are > features of the simple lambda-calculus. Binding on types is a much > more advanced feature, as it belongs to System F. Binders on module > and functors (let module = ... in ..) is even richer, as it translates > in system Fomega. It may not make a lot of difference to the > programmer, but the metatheory needed to support each of these > extension is quite different. Let-binding is the simpler of those. > --0016e6d7e13d16ce32048f109bfd Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
[Re-adding caml-list: I thought this conversation about let-polymorphi= sm might be of wider interest.]

The "stabilit= y" property you mention is nice, but of course if you don't have l= et-polymorphism then you get a different handy rewrite, namely the equivale= nce of
=A0=A0let x =3D e1 in e2 =A0and =A0 (fun x -> e2) e1
no? =A0I = was surprised when I first realized this didn't hold in ML.
<= br>
In your last paragraph, you seem to elide the distinction bet= ween monomorphic and polymorphic let, implying that both are the bottom run= g of the type hierarchy...but I'm proposing that polymorphic let is alr= eady an extension of a simpler system. =A0Does polymorphic let not seem &qu= ot;richer" than lambda to you? =A0It certainly seems to me to affect t= he metatheory (although recently I've been thinking more about set-theo= retic sematics than the usual type-theoretic properties).

Maybe I'm splitting hairs...overall it still seems = reasonable to me to exclude let-polymorphism from Llama Light, considering = that the goal is be a minimal base system, and this one appears to be perfe= ctly practical. =A0I can't tell whether you disagree with this.

-Jeremy

On Mon, Aug 30, 2010 at 4:06 PM, bluestorm <bluestorm.dylc@gmail.com> wrote:
On Mon, Aug 30, 2010 at 7= :03 PM, Jeremy Bem <jeremy1@gmail.c= om> wrote:
> Right...thanks for the refresher. =A0I suppose I should implement this= , as
> technically it is not "ML" until I do. =A0I'm still wond= ering why this is
> considered an essential and desirable feature.

One reason it is interesting is that it gives you the following
stability property,
wich is good for refactoring (both by humans and by copmuters) for example = :

=A0let x =3D e1 in e2 =A0 =A0 is equivalent to =A0 =A0e2{x <- e1} =A0(e= 2 in wich
all free occurences of x are replaced by e1)

If let isn't polymorphic, then for example =A0 let id x =3D x in (id 1,= id
2) =A0doesn't work out.

There are other cases where polymorphism may be useful locally. For
example in Haskell, the ST monad use polymorphism to encode an
information about the use of effects in your code : if all effect are
used locally (so the function is "observationally pure", or
"referentially transparent", while still using side effects insid= e),
the result will be polymorphic in the state parameter of the ST monad.
If it's not, we know a side effect has escaped, and the type system
forbids you from "running" the monad.


> If one can make local polymorphic definitions, why
> not local types and local exceptions?

In OCaml you can have local types and exceptions through the "le= t
module =3D .. in .." construct.

Note however that, on a "richness of the type system" scale, they= 're
much higher in the hierarchy. Binders on value (lambda and let) are
features of the simple lambda-calculus. Binding on types is a much
more advanced feature, as it belongs to System F. Binders on module
and functors (let module =3D ... in ..) is even richer, as it translates in system Fomega. It may not make a lot of difference to the
programmer, but the metatheory needed to support each of these
extension is quite different. Let-binding is the simpler of those.

--0016e6d7e13d16ce32048f109bfd-- 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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 75325BC57 for ; Wed, 1 Sep 2010 08:21:37 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArICAKqNfUzRVdg0kGdsb2JhbACBQ5FKhVABh3kIFQEBAQEJCQwHEQMfo2mJLoIVhlIuiFQBAQMFhTQEgVeDG4Uf X-IronPort-AV: E=Sophos;i="4.56,302,1280700000"; d="scan'208";a="66488368" Received: from mail-qw0-f52.google.com ([209.85.216.52]) by mail1-smtp-roc.national.inria.fr with ESMTP; 01 Sep 2010 08:21:36 +0200 Received: by qwi4 with SMTP id 4so87558qwi.39 for ; Tue, 31 Aug 2010 23:21:36 -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=joGwhzjFKmJ9NbuZKJpQrwM1HIgzj9cEAbjrYXmmQnk=; b=oMFbg7t0lPVjrHfxDc8dnfWJujToSMFBAKEeABPiRYuOm1XrTGtuUsDHf4JSrAurMl V7enX2UywrOtJ9r+iusU99Y1NPHIucW/x2eELFhhBaZqaheqPs7NpuYMbpnMYIXkVtqH iorMycA25BhTbffQo9hDq4QvTqTtKcm1wqOo8= 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=uVRgcycSzSdVwRhCz65Ff376dYCS3DH73DdkgACELPgh3b+CNcQc705oJ2MM3uGfCk eJQeTsbhUPBFVIUEbvdMIdyMIs763kKnOXhcuH7OSrgMIEkh3uGnvyyB7UWPPxJltc5w I8Ps0+fztzElfhtQ8GK2HJ4WXMYUhx/yz2AoA= MIME-Version: 1.0 Received: by 10.229.214.210 with SMTP id hb18mr5049422qcb.68.1283322094631; Tue, 31 Aug 2010 23:21:34 -0700 (PDT) Received: by 10.229.218.19 with HTTP; Tue, 31 Aug 2010 23:21:34 -0700 (PDT) In-Reply-To: <027401cb486a$48511e00$d8f35a00$@com> References: <026901cb485b$ff1b8ad0$fd52a070$@com> <027401cb486a$48511e00$d8f35a00$@com> Date: Wed, 1 Sep 2010 16:21:34 +1000 Message-ID: Subject: Re: [Caml-list] Llama Light: a simple implementation of Caml From: ivan chollet To: Jon Harrop Cc: Jeremy Bem , caml-list List Content-Type: multipart/alternative; boundary=0016361e83ba953c7a048f2cb515 X-Spam: no; 0.00; parallelism:01 cheers:01 recursion:01 pointers:01 run-time:01 compiler:01 recursion:01 cheers:01 pointers:01 typechecker:01 ocaml:01 typechecker:01 runtime:01 bytecode:01 compiler:01 --0016361e83ba953c7a048f2cb515 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable Thanks. I will keep that it mind and might look into it one day or another. Ivan On Tue, Aug 31, 2010 at 3:39 AM, Jon Harrop < jonathandeanharrop@googlemail.com> wrote: > If you can keep it agnostic wrt boxing then you should be able to plug i= t > into HLVM easily for much faster numerics and parallelism. > > > > Cheers, > > Jon. > > > > *From:* ivan chollet [mailto:ivan.chollet@gmail.com] > *Sent:* 30 August 2010 18:10 > *To:* Jon Harrop > *Cc:* Jeremy Bem; caml-list List > > *Subject:* Re: [Caml-list] Llama Light: a simple implementation of Caml > > > > clearly didn't plan to support polymorphic recursion in any way. I don't > even plan to support lexical scoping... > As for data representation I'm actually boxing everything except ints and > function pointers. I found out that it leads to the simplest design, whic= h > is appropriate for a project that I don't want to take me more than a few > days. > > On Tue, Aug 31, 2010 at 1:57 AM, Jon Harrop < > jonathandeanharrop@googlemail.com> wrote: > > Try to remove all assumptions of uniform run-time representation from the > compiler because avoiding boxing gives huge performance gains and makes i= t > much easier to write a performant garbage collector. You=92ll need to > sacrifice polymorphic recursion though, which you probably already have > anyway=85 > > > > Cheers, > > Jon. > > > > *From:* caml-list-bounces@yquem.inria.fr [mailto: > caml-list-bounces@yquem.inria.fr] *On Behalf Of *ivan chollet > *Sent:* 30 August 2010 11:57 > *To:* Jeremy Bem > *Cc:* caml-list List > *Subject:* Re: [Caml-list] Llama Light: a simple implementation of Caml > > > > OK. > > This looks nice and I would be pleased if you could put a few pointers or > explanations on your webpage about your typechecker implementation and ho= w > it differs with OCaml typechecker. > I will get some free time this week and to implement yet another runtime > and bytecode compiler from scratch. Not sure if it will be completed at t= he > end of the week, but i'll be definitely interested to know more about the > theoretical motivations of works like yours! > > On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem wrote: > > 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 "ty= pe > 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 compil= er > 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 =3D 2 > > # let x =3D 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 =3D 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 tha= t > have polymorphic type annotations are generalised, while in your system i= t > is not possible to force generalisation. > > > > I had a look at the typer, and it's indeed rather simple; it seems it wou= ld > be quite simple to implement generalized let (when encountering annotatio= ns > or with a different syntaxic construct : "letg .. =3D .. in ..."), but th= e > added complexity is equivalent to adding let generalization by default. > > > > Is the presence of let-generalization a real issue in your work ? > > > > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > > > > --0016361e83ba953c7a048f2cb515 Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: quoted-printable Thanks. I will keep that it mind and might look into it one day or another.=

Ivan


On Tue, Aug 31, 2010 at = 3:39 AM, Jon Harrop <jonathandeanharrop@googlemail.com> wrote:=

If you can keep it agnostic wrt boxing then you should be able to plug it into HLVM easily for much faster numerics and parallelism.

=A0

Cheers,

Jon.

=A0

F= rom: ivan cholle= t [mailto:ivan.ch= ollet@gmail.com]
Sent: 30 August 2010 18:10
To: Jon Harrop
Cc: Jeremy Bem; caml-list List


Subject: Re: [Caml-list] Llama Light: a simple implementation of Cam= l

=A0

clearly didn't pl= an to support polymorphic recursion in any way. I don't even plan to support lexical scoping...
As for data representation I'm actually boxing everything except ints a= nd function pointers. I found out that it leads to the simplest design, which = is appropriate for a project that I don't want to take me more than a few = days.

On Tue, Aug 31, 2010 at 1:57 AM, Jon Harrop <jonathan= deanharrop@googlemail.com> wrote:

Try to remove all assumptions of uniform run-time representation from the compiler because avoiding boxing gives hug= e performance gains and makes it much easier to write a performant garbage co= llector. You=92ll need to sacrifice polymorphic recursion though, which you probably already have anyway=85

=A0

Cheers,

Jon.

=A0

F= rom: caml-list-bounce= s@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] On Behalf Of ivan chollet
Sent: 30 August 2010 11:57
To: Jeremy Bem
Cc: caml-list List
Subject: Re: [Caml-list] Llama Light: a simple implementation of Cam= l

=A0

OK.

This looks nice and I would be pleased if you could put a few pointers or explanations on your webpage about your typechecker implementation and how = it differs with OCaml typechecker.
I will get some free time this week and to implement yet another runtime an= d bytecode compiler from scratch. Not sure if it will be completed at the end= of the week, but i'll be definitely interested to know more about the theo= retical motivations of works like yours!

On Mon, Aug 30, 2010 at 2:37 AM, Jeremy Bem <jeremy1@gmail.com> wrote:

bluestorm:

=A0

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

=A0

Do you see a nice way to add let-generalization without reintroducing "ty= pe levels"? =A0I was pleased to remove those.

=A0

Ivan:

=A0

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 minimal changes to accommodate the new typechecker; the ru= ntime is almost identical to OCaml's.

=A0

-Jeremy

=A0

On Sun, Aug 29, 2010 at 6:52 AM, bluestorm <bluestorm.dylc@gmail.com> wrote:

When using the toplevel, declaration phrases fail (looks like a linking problem)= , but expressions work as intented :

$ 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'

=A0

I made my tests using "llamac -i foo.ml".

=A0


I found it startling that the most important difference to my eyes are buri= ed, on the web page, under lines of relatively boring documentation :

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

=A0

- 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.)

=A0

These choices simplify the implementation while having relatively little impact o= n the user.

=A0

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 no= t possible to force generalisation.

=A0

I had a look at the typer, and it's indeed rather simple; it seems it wou= ld be quite simple to implement generalized let (when encountering annotations or with a different syntaxic construct : "letg .. =3D .. in ..."), b= ut the added complexity is equivalent to adding let generalization by default.

=A0

Is the presence of let-generalization a real issue in your work ?

=A0


_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.in= ria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

=A0

=A0


--0016361e83ba953c7a048f2cb515--