Re: [MirageOS-devel] Whole Program Optimization in Mirage

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

On 1 Jul 2014, at 11:14, Anil Madhavapeddy <anil@xxxxxxxxxx> wrote:

> - staged programming: the Mirage tool evaluates a config.ml, and outputs
>  an OCaml main.ml which performs the functor applications into a concrete
>  module.  This gives the compiler more static knowledge than if we used
>  first-class modules.  Again, we don't have much defunctorisation in the
>  compiler right now, but Pierre's -flambda branch will help a lot (no
>  pressure, Pierre :-)

As an aside, we submitted a talk proposal to the ML workshop that just got
accepted, and I noticed this misinterpretation of the config.ml combinators
from one of the anonymous reviewers:

Reviewer #2 wrote:
> MirageOS is a very interesting project and it is nice to see an example of ML 
> module system features being put to use. At the same time, the need for a 
> customized configuration language with new functor combinators suggests that 
> the authors ran into limitations in the expressiveness of the OCaml module 
> system. Taken together, these points suggest this work should lead to 
> interesting discussions.

Our extended abstract was written in the early hours of the morning and was
no doubt slightly incoherent, but we should definitely emphasise that the
functor combinators are in fact just normal OCaml functions, with the resulting
values being GADTs that output code that is guaranteed (due to the GADT
witnesses) to not result in a type error.

This is something that will eventually disappear behind a MetaCaml-like
model, instead of concrete source code being output between stages...

-anil
_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel