Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: cyclic value construction ("let rec")
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Xavier Leroy <Xavier.Leroy@i...>
Subject: Re: cyclic value construction ("let rec")
> > [Pierre Weis:]
> > This certainly suggests to allow the export of an immutable view of a
> > record type with mutable fields. This way you could do the
> > initialization in a safe way (no magic) using side effects, and still
> > export a safe immutable type to the external world.
> 
> [Markus Mottl:]
> Sounds like a good idea! Using powerful "magic" is probably too dangerous
> for "everyday"-use and definitely not in accordance with the "zero defect"
> ambitions of the type system...
> Although it would sometimes be nice to even hide specific fields of the
> record, this would probably not work well together with separate
> compilation.  However, the memory layout of the fields does not change by
> just omitting the "mutable" declaration, so this should not do any harm.

Alas, it can do a lot of harm.  For one thing, you could break type
safety this way, just like with polymorphic references:

A.ml:
        type 'a t = { mutable contents: 'a }
        let assign t v = t.contents <- v

A.mli:
        type 'a t = { contents: 'a}
        val assign: 'a t -> 'a -> unit

Client.ml:
        open A
        ...
          let x = { contents = [] } in
          assign x [1];
          x.contents = [true]

When typing Client.ml, since "contents" is assumed immutable, the
definition of x is a syntactic value, hence x receives type
        forall 'a.  'a list t
But of course this typing is invalidated by the call to "assign",
and you end up comparing an int list to a bool list -- a typing violation.

Some compiler optimisations, specific to immutable structures, could
similarly be broken.

So, no, we can't allow exporting a record with different mutability
annotations than in its definition.

- Xavier Leroy