Questions about Equality of Code, CSP and State

[Martin Berger-3]

Hello, I have a few simple question about MetaOCaml.  The first is
about equality of code. I get:

    # let x = .<2>. in x = x;;
    - : bool = true
    # .<2>. = .<2>.;;
    - : bool = false

Why? For similar equation at function type MetaOCaml answers:

    # let f = (fun x -> x ) in f = f;;
    Exception: Invalid_argument "equal: functional value".
    # (fun x -> x ) = (fun x -> x );;
    Exception: Invalid_argument "equal: functional value".

My second question concerns staging correctness and typing. The page

    http://okmij.org/ftp/Computation/Generative.html

lists the following example:

     let code =
        let x = ref .<1>. in
        let _ = .<fun v -> .~(x := .<v>.; .<()>.)>. in
        !x;;

It evaluates to:

     val code : ('a, int) code = .<v_1>.
     # .!code;;
     Unbound value v_1
     Exception: Trx.TypeCheckingError.

Why is this program allowed to typeckeck? Clearly CSP (cross-stage
persistence) and state don't make easy bedfellows. Would ruling it out
through some suitable restriction (along the lines of making state and
polymorphism compatible) be too restrictive?

Martin
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Walid Taha-3]

Dear Martin,

Thank you for these questions.  They are quite timely.

I'm CC'ing the mailing list so that others can chime in as needed.

On Thu, Jun 4, 2009 at 4:08 AM, Martin Berger <M.F.Berger@...> wrote:

Hello, I have a few simple question about MetaOCaml.  The first is
about equality of code. I get:

  # let x = .<2>. in x = x;;
  - : bool = true
  # .<2>. = .<2>.;;
  - : bool = false

Why? For similar equation at function type MetaOCaml answers:

Technically, code is an abstract type and so the equality test is of OCaml
should not be defined.  What you see above is exposing the underlying
implementation (AST's) and testing equality on that.

Ideally, it would be better if we can change the implementation so that it
returns an error message if this type is compared for equality, in a way
similar to what you illustrate below.

  # let f = (fun x -> x ) in f = f;;
  Exception: Invalid_argument "equal: functional value".
  # (fun x -> x ) = (fun x -> x );;
  Exception: Invalid_argument "equal: functional value".

Cristiano/Ron:  Would this change be easy enough for us to impelemnt?

My second question concerns staging correctness and typing. The page

  http://okmij.org/ftp/Computation/Generative.html

lists the following example:

   let code =
      let x = ref .<1>. in
      let _ = .<fun v -> .~(x := .<v>.; .<()>.)>. in
      !x;;

It evaluates to:

   val code : ('a, int) code = .<v_1>.
   # .!code;;
   Unbound value v_1
   Exception: Trx.TypeCheckingError.

Yes, this is the classic scope extrusion example, and it does behave
this way in MetaOCaml.  The classifier system, which is what MetaOCaml
uses, is sound only in the purely functional setting.

 

Why is this program allowed to typeckeck?

Only because all alternatives were too heavy wait, and seemed impractical.
Classifiers are very lightweight, but only ensure static type safety for the
purely functional subset.
 

Clearly CSP (cross-stage
persistence) and state don't make easy bedfellows.

I don't see how CSP is implicated in this example.
 

Would ruling it out
through some suitable restriction (along the lines of making state and
polymorphism compatible) be too restrictive?

This looks like it could be a new idea.  Can you say a bit more about
what you have in mind?

Walid.

Martin
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

--
Walid Taha, Assistant Professor,
Department of Computer Science and Department of Electrical and Computer Engineering
Rice University, MS-1302, Duncan Hall 3103, Houston, TX 77025
Tel:  [phone].  Fax:  [phone]

---

CONFIDENTIALITY NOTICE

The information in this email may be confidential and/or privileged. This
email is intended to be reviewed by only the individual or organization
named above. If you are not the intended recipient or an authorized
representative of the intended recipient, you are hereby notified that any
review, dissemination or copying of this email and its attachments, if any,
or the information contained herein is prohibited. If you have received this
email in error, please immediately notify the sender by return email and
delete this email from your system.

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Walid Taha-3]

Hi Martin

Incidentally a roughly equivalent program in the (dynamically typed)
Converge metaprogramming language (http://convergepl.org) does catch
this error at compile time:

That is a good point.  Because MetaOCaml is an extension of OCaml,
we are restricted to how OCaml does things.  If I remember correctly,
OCaml pretends that equality is polymorphic (in that it gives it a polymorphic
type), but then checks unusual cases like functions at runtime (I may
be misremembering on this).  If that's the case, it becomes hard for
us to do such test statically, and it is easy to do dynamically.

If OCmal had either weak type variables or type classes, doing such
a check statically would be easier.

I don't see how CSP is implicated in this example.

The variable v is defined at metalevel 1, but is then used at
level 0. OK, that's maybe not what we usually call CSP.

Actually, it is used at level 1 (it's in brackets).
 

This looks like it could be a new idea.  Can you say a bit more about what you have in mind?

I have not though about it deeply. I'm new to metaprogramming.

 
We just submitted a paper on a new approach to imperative MSP (developed
by Edwin, Jun, and Mathias).  This approach is based on restricting computations
that can be done under escapes.  If you'd like, Edwin can provide you with
a copy of the submitted draft.  I would be very interested in your feedback.

Martin

--
Walid Taha, Assistant Professor,
Department of Computer Science and Department of Electrical and Computer Engineering
Rice University, MS-1302, Duncan Hall 3103, Houston, TX 77025
Tel:  [phone].  Fax:  [phone]

---

CONFIDENTIALITY NOTICE

The information in this email may be confidential and/or privileged. This
email is intended to be reviewed by only the individual or organization
named above. If you are not the intended recipient or an authorized
representative of the intended recipient, you are hereby notified that any
review, dissemination or copying of this email and its attachments, if any,
or the information contained herein is prohibited. If you have received this
email in error, please immediately notify the sender by return email and
delete this email from your system.

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

> There has been some research on this matter; Walid and Cristiano wrote
> a paper proposing one restriction (permitting only closed values to be
> stored in reference cells). Alas, it it too restrictive for Gibonacci
> example. Peter Thiemann proposed restrictions in his old paper on
> partial evaluation. I've been involved in such research too. I can't
> say we found the final solution and we can't typecheck all interesting
> programs (we can't lift common sub-expressions out of the loops, for
> example). We can typecheck Gibonacci (with mutable memo table) and
> similar problems though...

I have a question about the relationship between these typing systems
and the mechanisms Converge (http://convergepl.org) and Template Haskell
use to avoid such scope extrusion. It appears to me that these languages
do essentially the same thing in regard to avoiding inappropriate scope
extrusion, namely a program analysis on (essentially) the whole
program after parsing. (The TH paper [2] by Sheard and Peyton Jones is
unclear on this issue; a description of the Converge mechanism
can be found in [1]). This seems to be much more expressive than
using types (or at least the types that have been proposed) and
less intrusive.

Martin

[1] Laurence Tratt, Compile-time meta-programming in a dynamically
typed OO language.

[2] Tim Sheard, Simon Peyton Jones, Template meta-programming for
Haskell.
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Walid Taha-3]

Dear Martin,

The type of scope extrusion that we have addressed in the recent Mint work
arises when you have statically scoped next-stage code and imperative
effects in the *current* stage.  Any language that tries to guarantee static
scoping for next-stage (and inevitably uses a kind of gensym to achieve
static scoping) will suffer from that problem.  Oleg is more familiar with TH
than I, and can assert whether it uses gensym and allows state in the current
(or first) stage.  Whether or not you statically type the second stage is
independent of the presence of the scope extrusion problem.

As for expressivity, yes, a simple type discipline can limit what you can generate
from *one* generator.  However, if you have slightly more expressive types,
such as indexed types, then you can write one generator that can generate all
simply typed terms.  Thus, you can have very expressive statically typed
generators.  This is the subject of both our Concoqtion paper and our "Tagless
Staged Interpreters" paper.  Now, if you really don't like types, then yes, any
statically typed approach will not seem convenient.  But if you want to be
untyped (or dynamically typed as some people prefer to call such languages)
and to avoid scope extrusion, you need to use something along the lines
proposed in the mint paper.

With respect to Converge, it really depends.  If you are only allows to write
DSL programs that contain no escapes (no possibility for static computation)
then you are OK.  And if you are only allowed to have escaped computation
that is purely function, you should still be OK.  But if you have escaped
computation (and specifically, under binders), then I would expect that you
can construct examples that would lead to scope extrusion.

Walid.

On Mon, Jun 8, 2009 at 8:33 AM, Martin Berger <M.F.Berger@...> wrote:

There has been some research on this matter; Walid and Cristiano wrote
a paper proposing one restriction (permitting only closed values to be
stored in reference cells). Alas, it it too restrictive for Gibonacci
example. Peter Thiemann proposed restrictions in his old paper on
partial evaluation. I've been involved in such research too. I can't
say we found the final solution and we can't typecheck all interesting
programs (we can't lift common sub-expressions out of the loops, for
example). We can typecheck Gibonacci (with mutable memo table) and
similar problems though...

I have a question about the relationship between these typing systems
and the mechanisms Converge (http://convergepl.org) and Template Haskell
use to avoid such scope extrusion. It appears to me that these languages
do essentially the same thing in regard to avoiding inappropriate scope
extrusion, namely a program analysis on (essentially) the whole
program after parsing. (The TH paper [2] by Sheard and Peyton Jones is unclear on this issue; a description of the Converge mechanism
can be found in [1]). This seems to be much more expressive than
using types (or at least the types that have been proposed) and
less intrusive.

Martin

[1] Laurence Tratt, Compile-time meta-programming in a dynamically
typed OO language.

[2] Tim Sheard, Simon Peyton Jones, Template meta-programming for
Haskell.

--
Walid Taha, Assistant Professor,
Department of Computer Science and Department of Electrical and Computer Engineering
Rice University, MS-1302, Duncan Hall 3103, Houston, TX 77025
Tel:  [phone].  Fax:  [phone]

---

CONFIDENTIALITY NOTICE

The information in this email may be confidential and/or privileged. This
email is intended to be reviewed by only the individual or organization
named above. If you are not the intended recipient or an authorized
representative of the intended recipient, you are hereby notified that any
review, dissemination or copying of this email and its attachments, if any,
or the information contained herein is prohibited. If you have received this
email in error, please immediately notify the sender by return email and
delete this email from your system.

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Chung-chieh Shan-3]

Martin Berger <M.F.Berger@...> wrote in article <4A2D1322.5030809@...> in gmane.comp.lang.ocaml.meta.user:

> I have a question about the relationship between these typing systems
> and the mechanisms Converge (http://convergepl.org) and Template Haskell
> use to avoid such scope extrusion. It appears to me that these languages
> do essentially the same thing in regard to avoiding inappropriate scope
> extrusion, namely a program analysis on (essentially) the whole
> program after parsing. (The TH paper [2] by Sheard and Peyton Jones is
> unclear on this issue; a description of the Converge mechanism
> can be found in [1]). This seems to be much more expressive than
> using types (or at least the types that have been proposed) and
> less intrusive.

To echo what Walid said: it depends on what you mean by "expressive".
If you measure expressivity by how many programs can be generated and
how short their correct generators can be, then nothing beats good old
printf.  Another notion of expressivity (followed more by, e.g., Dussart
& Thiemann, Calcagno, Moggi, Nielsen & Taha, and Kameyama, Kiselyov
& Shan) is to balance what programs you can generate and how short
their correct generators are against what safety properties can be
guaranteed for the generated code before running the generator.  For
example, I am not familiar with Converge, but Template Haskell does
not guarantee before running a generator that the generator will only
generate well-formed code.

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
We want our revolution, and we want it now! -- Marat/Sade
We want our revolution, and we'll take it at such time as  
 you've gotten around to delivering it      -- Haskell programmer

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Chung-chieh!

 > To echo what Walid said: it depends on what you mean by "expressive".
 > As far as I can see, neither Converge nor Template Haskell [...]
 > instead they are much more limited in the kinds of staging they
 > support with static scoping.

You rise a very interesting question, that of expressivity
in metaprogramming languages. In what sense precisely are some
metaprogramming languages more expressive than others?  Has the
question of metaprogramming expressivity been studied formally?

 > but Template Haskell does not guarantee before running a generator
 > that the generator will only generate well-formed code.

That's right, but since generated code will have to be
compiled before execution, only well-typed code will ever
be executed. (The scope-extrusion problem discussed
in previous mails suggests that MetaOCaml's typing system
cannot guarantee to generate only well-formed code either.)

The TH approach (also found in C++ and Converge)
where splicing in code happens at compile time, and the
approach of the MetaML family of languages, where this
is under program control, are two seemingly fundamentally
different approaches with -- presumably -- different strengths
and weaknesses.

It would be interesting to have clearcut formal results on the
expressive power of these approaches.

Martin


_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Rowan!

 > Also, I don't agree that the types involved are intrusive - they
 > just capture the reasons why the generated code is valid, and
 > provide a natural framework for programmers to reason about this
 > validity - something that a programmer must do anyway, just that
 > without types the reasoning isn't checked.

I disagree with the last sentence. My understanding of Converge (as I
said the Template Haskell paper is very sketchy on this) is that a
whole-program static analysis does reject all programs that do leak
staged-scope (and some that don't but look like they do). So Converge
does make the same guarantee, it's just not expressed in types.

 > Outside of meta programming, personally I regularly program using
 > both statically and dynamically typed languages, and I find the
 > *lack* of types quite intrusive to the way I program - basically I
 > find I have to be much more careful and go more slowly without
 > static types otherwise I end up spending nearly all the time doing
 > run-time debugging.  Meta-programming adds considerable complexity,
 > and is tough to get right, so static types help here even more.

I'm not arguing against using types. Other than being a big fan of
languages with weakly expressive type systems + type inference (like
Ocaml), which seem to have better software engineering qualities than
other forms of language, I'm quite agnostic on this issue. Typed and
untyped languages have their uses, and complementary strength and
weaknesses, and there's a huge discussion going on regarding the
large-scale software engineering properties of either approach. My
point was different:

1. The MetaOCaml typing system does not guarantee the absence of
    staged-scoping errors (it does only for the functional fragment).

2. I conjecture that any typing system that does make such a guarantee
    for all of MetaOCaml is either too restrictive or very complicated
    (e.g. no type-inference).

3. Static analysis based approaches to avoiding scope extrusion can
    guarantee the absence of staged-scoping errors without complicating
    programs.

I may be wrong on some or all of these points. In particular, the Mint
paper argues quite cogently, that only fairly minor restrictions
will have to be imposed to avoid staged scope extrusion. I'm also
unsure about (3), since -- as far as I can see -- the exact static
analysis mechanism that prevent staged-scope extrusion are unknown to
me, as they are not documented.

 > Rowan

Are you Rowan Davies who did pioneering work with Frank Pfenning in
the 1990s on typing metaprogramming?

Martin



_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Oleg!

> Template Haskell does nothing at all to avoid scope extrusion! Sadly,
> Template Haskell does nothing to prevent building of any ill-typed
> code:

That's true, but a deliberate design choice. Since splices are
executed at compile-time, the resulting code will have to be
compiled and no ill-typed generated code will be executed.

> Meta-Haskell is typed and it does not let the programmer create names
> at wish.

Sounds very interesting. Does Meta-Haskell have an interface to
the ADT representation of code like Template Haskell has?

Martin

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Rowan!

 > Ah, I think we mean different things when we say static scoping.

The term "Scope" in MP-languages often causes confusion, because
staging introduces a new form of scoping. Maybe we need a
terminological distinction between conventional scope and the new
kind of scoping introduced by staging (in what stage a variable is
defined)? I tend to call it spatial/ temporal scope, but that
terminology doesn't seem to generate much enthusiasm.

 > But, I think when it is not valid it cannot give nearly as good
 > feedback as a type checker

The question of error messages in MP-languages is a very interesting
one. Laurence probably has much more to say on this than I do.

 > Just checking the generated code is not checking the programmers
 > reasoning - it is more like a runtime error since you have already
 > started executing the code for the generators.

As far as I understand the innards of the Converge compiler, this
check happens before code generation.

 > The work of Nanevski and Pfenning seems the natural approach to me.
 > In some cases the types of generators might have to be specified
 > explicitly to make this work, but personally I don't see this as a
 > big deal

I agree that having a few annotations to ensure type-inference is
not a big deal. My question is more that I don't expect these
typing systems to scale when more involved forms of metaprogramming
are needed (like where you can splice in declarations, which you can
do in Converge).

 > For 3, this is true for compile-time metaprogramming, I guess.

 From the discussion here it seems to me now that there are two forms
of metaprogramming, which are (or appear to be) quite different. As
I'm new to the field of metaprogramming, it may appear naive to you,
or it might be wrong, in which case please correct my misconceptions.

- Dynamic metaprogramming (DMP) happens when a program P inputs some
   data x, and contingent upon that data, P constructs a program P'(x)
   which is then executed. This staging (first input data, then
   constructing a new program, then executing the new program) is done
   for efficiency purposes. A key characteristic of DMP languages is a
   run operator which executes a constructed program.  Since the
   primary objective of DMP is to increase performance, it makes sense
   to have stringent typing systems which index the type of code with
   another type representing the type of the code when run. This avoids
   type-checking at run-time.

   The MetaML family of languages is a good example of languages
   optimised for dynamic metaprogramming.

- Static metaprogramming (SMP), also known as compile-time
   metaprogramming. Here it is not the computation that is staged, but
   the compilation process: the first step in the compilation (after
   lexing and parsing) is to interpret the metaprogramming constructs,
   which typically means rewriting splices into programs free from
   metaprogramming constructs. Then normal compilation (including
   type-checking) commences. The main purpose of SMP is to increase
   language expressivity. SMP languages don't have a run operator.
   Instead they have splices. Since any generated program will have to
   pass the type-checker in the eventual 'normal' compilation it is not
   required to index the type of code as in DMP languages with the type
   that the code will evaluate to after splicing.  Moreover, since the
   performance of the (meta)compilation process is not critical (it
   will be compiled only once), type-checking splices at splice-time is
   acceptable. This means typing systems for SMP languages can be
   simpler and more expressive.

   Converge, Template Haskell and C++ are examples of SMP languages, as
   a languages with preprocessor like cpp or CamlP4.

Please note that I'm not saying that this is the only distinction one
can make in metaprogramming languages, merely a dimension in the
design space.

 > Note that if you use MetaOCaml to emulate compile-time
 > metaprogramming,

If this distinction between SMPs and DMPs is appropriate, then
defining what it means for a SMP to emulate a DMP or vice versa might
be subtle. Which notion of translation have you got in mind?


Martin

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Chung-chieh Shan-4]

On 2009-06-13T13:39:56+0100, Martin Berger wrote:
> I agree that having a few annotations to ensure type-inference is
> not a big deal. My question is more that I don't expect these
> typing systems to scale when more involved forms of metaprogramming
> are needed (like where you can splice in declarations, which you can
> do in Converge).

MetaOCaml (even just its functional fragment) can already splice in
declarations of values (using let).

> From the discussion here it seems to me now that there are two forms
> of metaprogramming, which are (or appear to be) quite different. As
> I'm new to the field of metaprogramming, it may appear naive to you,
> or it might be wrong, in which case please correct my misconceptions.

I don't understand the difference between the two forms because, for
example, MetaOCaml can perfectly well be used to increase expressivity
by splicing (a metaprogramming construct).  Your description of the two
forms mentions "a program P" and a distinction between "compile time"
and "run time".  Can P be a compiler, which takes a program x as input?
What is the difference between compile time and run time (especially in
the setting of Futamura projections)?  I don't know how to tell "normal
compilation" from abnormal compilation.

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
We want our revolution, and we want it now! -- Marat/Sade
We want our revolution, and we'll take it at such time as  
 you've gotten around to delivering it      -- Haskell programmer


_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello!

> MetaOCaml (even just its functional fragment) can already splice in
> declarations of values (using let).

Sorry, I meant type declarations, as in:

    let t = <int -> int> in
    let x = <lambda x : ~t. x3> in ...

I'll answer to the rest of your mail when I get some time to think
about it.

Martin
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Jacques Carette]

Martin Berger wrote:
> Sorry, I meant type declarations, as in:
>
>    let t = <int -> int> in
>    let x = <lambda x : ~t. x3> in ...
I (in conjunction with others) have written some large and complicated
MetaOCaml code, and I have not really needed that [although I did
naively wish for it several times].  Using Functors properly, you can
indeed 'generate' most of the dynamic types you need in practice.  The
only types you cannot generate this way are truly "computed" types,
which are quite naturally outside the scope of the present MetaOCaml.

True, to get what you need inside the strict type discipline of
MetaOCaml you need to think a lot harder than what you can get away with
in other, unsafe languages.  Once I trained myself out of my bad habits
garnered from my days of undisciplined meta-programming, I came to
really appreciate this ``better'' way of doing things.

I am not saying you never need to generate types computationally, but it
turns out to be fairly rare.  The kinds of types that MetaOCaml lets you
generate *via OCaml* are quite generous already!  The error of a lot of
programmers here seems to be that they use very little of O'Caml's power
when structuring and building their code generators.

Jacques
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Jacques!

 > I (in conjunction with others) have written some large and
 > complicated MetaOCaml code, and I have not really needed that
 > [although I did naively wish for it several times].  Using Functors
 > properly, you can indeed 'generate' most of the dynamic types you
 > need in practice.  The only types you cannot generate this way are
 > truly "computed" types, which are quite naturally outside the scope
 > of the present MetaOCaml.

That's interesting. Can you generate types for n-ary selectors (for
arbitrary n)? What I mean by this something like

    fun (x1, x2, ..., xn ) -> xi

using functors? Is it possible to generate types for printf-like
constants where the types of the remaining arguments depend on the
value of the first argument?

Martin

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Chung-chieh!

> I don't understand the difference between the two forms because, for
> example, MetaOCaml can perfectly well be used to increase expressivity
> by splicing (a metaprogramming construct).

Consider the following example: you have 100 computers and on
each you want to run a program P. Assume you use MetaOCaml to
write P, because you find Ocaml lacks in expressivity. Maybe
you need some try ... with ... finally construct. If you construct
and embed such an extension statically (e.g. with OcamlP4), you
will pay the price of reducing the extended language to Ocaml
once, at compile-time.

If you make this extension using MetaOCaml, you will pay for this
100 times.

To be sure, semantically (assuming conventional lambda-theories),
the two approaches are the same.

> Your description of the two
> forms mentions "a program P" and a distinction between "compile time"
> and "run time".  Can P be a compiler, which takes a program x as input?
> What is the difference between compile time and run time (especially in
> the setting of Futamura projections)?  I don't know how to tell "normal
> compilation" from abnormal compilation.

My understanding of the partial evaluation in general, and the
relationship between MetaML-like metaprogramming and the
Futamura projections is immature, so I'm not sure about the
answer to this question. I hope I will be able to answer in the
future.

Martin


_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Jacques Carette]

Martin Berger wrote:

> Hello Jacques!
>
> > I (in conjunction with others) have written some large and
> > complicated MetaOCaml code, and I have not really needed that
> > [although I did naively wish for it several times].  Using Functors
> > properly, you can indeed 'generate' most of the dynamic types you
> > need in practice.  The only types you cannot generate this way are
> > truly "computed" types, which are quite naturally outside the scope
> > of the present MetaOCaml.
>
> That's interesting. Can you generate types for n-ary selectors (for
> arbitrary n)? What I mean by this something like
>
>    fun (x1, x2, ..., xn ) -> xi
>
> using functors? Is it possible to generate types for printf-like
> constants where the types of the remaining arguments depend on the
> value of the first argument?

I do not know how to do the n-ary selector (and I doubt that it is
possible).  I can do it for the Church encoding of that function though,
which is just as good, since in a code generation setting you don't want
needless boxing/unboxing.

As for printf-like, yes, you can do that - you just need to write things
in CPS.  See Oleg's recent post in haskell-cafe for the core ideas
(based on ideas of Olivier Danvy from a long time ago).  Lifting that to
a code generator is relatively straightforward.  Of course, you need the
first argument to be a compile-time constant to do that, but that's the
case for almost all uses of printing.

Jacques
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Jacques!

 > I do not know how to do the n-ary selector (and I doubt that it is
 > possible).  I can do it for the Church encoding of that function
 > though, [...] As for printf-like, yes, you can do that - you just
 > need to write things in CPS.

Aha, thanks, it's good to know that it can be done if necessary.

I'm not sure I want normal programmers to use Church numberals or
CPS though. I don't expect such complicated encodings in
metaprogramming, which is already more complicated than normal
programming, to have good large-scale software engineering properties.

There is a reason why mainstream languages have a built-in type
for numbers, rather than relying on Church numerals, and why
CPS is not the default way of returning a result from a function.

Martin
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Chung-chieh Shan-4]

On 2009-06-16T11:23:28+0100, Martin Berger wrote:
> I'm not sure I want normal programmers to use Church numberals or
> CPS though. I don't expect such complicated encodings in
> metaprogramming, which is already more complicated than normal
> programming, to have good large-scale software engineering properties.
>
> There is a reason why mainstream languages have a built-in type
> for numbers, rather than relying on Church numerals, and why
> CPS is not the default way of returning a result from a function.

Our PEPM 2009 paper addresses exactly this issue!
http://www.cs.rutgers.edu/~ccshan/metafx/circle-shift.pdf

By the way, out of curiosity -- may I ask what motivates your interest
in code generation (especially imperative code generation)?

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
We want our revolution, and we want it now! -- Marat/Sade
We want our revolution, and we'll take it at such time as  
 you've gotten around to delivering it      -- Haskell programmer


_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Chung-chieh Shan-4]

On 2009-06-15T13:44:26+0100, Martin Berger wrote:
> If you make this extension using MetaOCaml, you will pay for this
> 100 times.
>
> To be sure, semantically (assuming conventional lambda-theories),
> the two approaches are the same.

Are you somehow ruling out the following way to use MetaOCaml?  Print
out a generated code value, then compile the printout ("offshore the
generated code") and run the result on 100 computers.

--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
We want our revolution, and we want it now! -- Marat/Sade
We want our revolution, and we'll take it at such time as  
 you've gotten around to delivering it      -- Haskell programmer


_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

[Martin Berger-3]

Hello Chung-chieh!

> Are you somehow ruling out the following way to use MetaOCaml?  Print
> out a generated code value, then compile the printout ("offshore the
> generated code") and run the result on 100 computers.

That's a very interesting question. If it was possible to print
out (or convert into a string) generated code, then indeed what
you suggest would be possible. But I am under the impression that
that MetaOCaml does not offer this conversion (please correct me
if I'm wrong). Moreover, if it is possible, would not the equational
theory of MetaOCaml be trivial, since we could now for example
distinguish alpha-convertible terms.

Martin

_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@...
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l