David Teller a écrit :
>    Hi everyone,
>  I'm currently in the very first stages of writing down a prototype
> implementation of a type checker. At the moment, I'm looking for "the
> nicest" way of labelling my abstract syntax tree with type annotations
> -- without corrupting the AST at all, if possible.
>
>
> Say I have
>
> type my_expression = ESomeConstructor  of ...
>                    | ESomeConstructor2 of ...
>                    | ESomeConstructor3 of my_function
> and  my_function   = FSomeConstructor ...
>
>
> A first idea would be to replace this structures with
>
> type 'a my_expression = ESomeConstructor  of ...
>                       | ESomeConstructor2 of ...
>                       | ESomeConstructor3 of 'a my_function
> and  'a my_function   = FSomeConstructor ...
>
> That would let me annotate instances of my_expression or my_function
> with informations of type 'a. However, this won't scale in case I decide
> that my static checker will need annotations of different types for
> my_expression and my_function. Of course, my AST is actually a tad more
> complex and would require about 15 type arguments, which I don't
> consider very nice. 
>
> Intuitively, using functors will yield the same kind of half-satisfying
> results.
>
> Any suggestions ?
>
>   
I can't ressit ... use pml 
(http://www.lama.univ-savoie.fr/~raffalli/repos/pml) in one week from 
now (I am currently implementing what you need,
this is why I am answering).

You will be able to write things like :

type AST =
  Nope[]
| App[AST,AST]

val rec decorate_with_size  ast =
  Nope[] -> 
    { Nope[] with val size = 0 } (* Here I am lying pml does not support 
native int yet, nor it will in one week *)
| App[u,v] ->
    let u' = decorate_with_size u and v' = decorate_with_size v in
    { App[decorate u, decorate v] with val size = 1 + u'.size  +  v'.size }

Moreover, the result type of decorate_with_size (which is {AST with val 
size : int }) is a subtype of AST
and this subtyping is completely implicit (no typecast needed) ...

OK, pml does not have native int (it has multiprecision nat) and no IO 
yet, it is interpreted (but not that slow),
probably buggy ... But you will soon be able to specify and prove your 
code too ...

Cheers,
Christophe