Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

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

34 views
Skip to first unread message

Jeremy Bem

unread,
Aug 29, 2010, 1:42:21 AM8/29/10
to caml-list List
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

bluestorm

unread,
Aug 29, 2010, 6:52:54 AM8/29/10
to Jeremy Bem, caml-list List
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 ?

ivan chollet

unread,
Aug 29, 2010, 9:01:09 AM8/29/10
to Jeremy Bem, caml-list List
Hi,

Is it just a fork on Caml light or a new implementation and runtime?

Regards

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

Jeremy Bem

unread,
Aug 29, 2010, 12:37:59 PM8/29/10
to bluestorm, caml-list List
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

Jeremy Bem

unread,
Aug 29, 2010, 2:42:35 PM8/29/10
to bluestorm, caml-list List
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

ivan chollet

unread,
Aug 30, 2010, 6:57:32 AM8/30/10
to Jeremy Bem, caml-list List
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!

Jon Harrop

unread,
Aug 30, 2010, 11:57:39 AM8/30/10
to ivan chollet, Jeremy Bem, caml-list List
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.

ivan chollet

unread,
Aug 30, 2010, 1:09:46 PM8/30/10
to Jon Harrop, Jeremy Bem, caml-list List
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 <
jonathand...@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-lis...@yquem.inria.fr [mailto:
> caml-lis...@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

Jon Harrop

unread,
Aug 30, 2010, 1:39:54 PM8/30/10
to ivan chollet, Jon Harrop, Jeremy Bem, caml-list List
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.c...@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
<jonathand...@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-lis...@yquem.inria.fr
[mailto:caml-lis...@yquem.inria.fr] On Behalf Of ivan chollet
Sent: 30 August 2010 11:57
To: Jeremy Bem
Cc: caml-list List

Jeremy Bem

unread,
Aug 30, 2010, 4:49:57 PM8/30/10
to bluestorm, caml-list List
[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 <bluesto...@gmail.com> wrote:

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

ivan chollet

unread,
Sep 1, 2010, 2:21:45 AM9/1/10
to Jon Harrop, Jeremy Bem, caml-list List
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 <
jonathand...@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.c...@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 <
> jonathand...@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-lis...@yquem.inria.fr [mailto:
> caml-lis...@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

0 new messages