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