Re: cyclic value construction ("let rec")

From: Xavier Leroy (Xavier.Leroy@inria.fr)
Date: Thu Apr 06 2000 - 16:25:52 MET DST

  • Next message: Markus Mottl: "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



    This archive was generated by hypermail 2b29 : Mon Apr 10 2000 - 01:31:18 MET DST