Re: [Caml-list] Type safe affectation ?

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

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

Gregory Morrisett wrote:
>>The problem is that holes at the type level are a difficult feature to
>>offer: they require linear types in the compiler. As an 
>>optimization, it is a rather high-level one, and maybe not so 
>>easy to know when it will apply.
> 
> 
> Perhaps, but it's easy for a compiler to offer support
> for "tail-allocation" (i.e., a tail-call except for a
> constructor application) which is what you need for
> a tail-recursive append or map.  Perry Cheng implemented it in
> the TIL compiler in about a week if memory serves and
> it was a tremendous improvement in performance without
> any magic.  
> 
> Yasuhiko Minamide wrote a paper on how to model this
> well (I think it appeared in ICFP).  The approach used
> in our Typed Assembly Language paper is yet another
> approach based on a simple subtyping trick with initialization
> flags.  It didn't require linear types at all and 
> instead of implicit subtyping, you could accomplish
> the same thing with an explicit (type-safe) up-cast.
> 
> So, all in all, it's quite possible to have the compiler
> implement this optimization for the common case of
> tail-allocation, and if you think it's more generally
> applicable, then you could move to something like TAL's
> initialization flags (though I would prefer the former
> option.)  

Does this also solve the construction of structure with loop ? (the 
other case were affectation is needed ? I say that because it is a 
similar problem and can be seen as a failuer of the compiler to type 
some expressions like this (the compiler says :

This kind of expression is not allowed as right-hand side of `let rec'
for add_Greater and add_Less

module Var = struct
   type t = var
   let compare = (-)
end

module MapVar = Map.Make(Var)

type env = value MapVar.t

and value =
   | Def of closure
   | Less of closure
   | Greater of closure

and closure = typ * env

let add_Greater v t e =
   let rec va = Greater(t, e')
   and e' = MapVar.add v va e in
   e'

let add_Less v t e =
   let rec va = Greater(t, e')
   and e' = MapVar.add v va e in
   e'

The same fonction is easy to write with affectation ... so it should be 
possible to compile it ?


-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

[-- Attachment #2: Type: application/pgp-signature, Size: 252 bytes --]