Llama Light: a simple implementation of Caml

Llama Light: a simple implementation of Caml

[Jeremy Bem]

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

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

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

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

[bluestorm]

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

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 ?

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

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

[Jeremy Bem]

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

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

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

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

[Jeremy Bem]

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

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

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

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

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

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

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

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

Thanks,
-Jeremy

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

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

[ivan chollet]

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

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

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

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

[Jon Harrop]

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

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

 


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

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

[ivan chollet]

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

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

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

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

[Jon Harrop]

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

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@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'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 = 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

 

 


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

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

[ivan chollet]

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

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.
>
>
>
> 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@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’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 = 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
>
>
>
>
>

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

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

[Jeremy Bem]

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

[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 <bluestorm.dylc@gmail.com> wrote:

> On Mon, Aug 30, 2010 at 7:03 PM, Jeremy Bem <jeremy1@gmail.com> 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.
>

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

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

[ivan chollet]

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

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 <jeremy1@gmail.com> 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
>
>

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