caml-list - the Caml user's mailing list
 help / color / mirror / Atom feed
From: Xavier Leroy <xavier.leroy@inria.fr>
To: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Type safe affectation ?
Date: Sat, 14 Jun 2003 15:35:23 +0200	[thread overview]
Message-ID: <20030614153523.A21942@pauillac.inria.fr> (raw)
In-Reply-To: <3EE9A15D.7080403@univ-savoie.fr>; from Christophe.Raffalli@univ-savoie.fr on Fri, Jun 13, 2003 at 12:03:09PM +0200

> Using the Obj module you can do affectation of cons cell of a list (or 
> any onther data type), which is usefull for instance to write a tail 
> recursive Map funtion ... (see a previous thread)
> But this is not typesafe !

Like all uses of module Obj, you can make this type-safe via proper
type constraints:

let set_cdr (l: 'a list) (x: 'a list) =
  match l with
    [] -> invalid_arg "set_cdr"
  | _::_ -> Obj.set_field (Obj.repr l) 1 (Obj.repr x)

> Why not allow a typesafe way to mute immutable data (sum, products, 
> immutable records and so on) ?

Because that would make this data mutable :-)  Immutability isn't there
just to annoy the programmer: it's a major improvement for software
reliability and quality.  Proving the correctness of functions that
manipulate lists or trees is feasible if the data is immutable, but
becomes essentially impossible if arbitrary in-place modifications are
allowed anywhere in the program.

Even if you're not interested in proofs of programs, I'm ready to bet
that there aren't 1 programmer in 100 who can write *fully correct*
code that manipulate mutable balanced trees, for instance.  (I think I
can't.)

Also, keep in mind that the compiler can optimize based on
immutability assumptions.  For instance, the OCaml compiler performs
propagation of structured constants and code motion for accesses
inside data structures that are immutable.  You might very well break
something by using the set_cdr function above.

> By the way, another step would be to infer for each function if it mutes 
> its arguments instead of annoting record with "mutable" indication.
> 
> This is better because the same data may be considered as mutable by 
> some functions (for instance when you construct the data) but then be 
> used only by immutable functions and this way the type inference can 
> help you insure that you do not mute the data anymore.
> 
> But this is research topic ?

This sounds reminiscent of effect systems.

- Xavier Leroy

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners


  reply	other threads:[~2003-06-14 13:35 UTC|newest]

Thread overview: 20+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2003-06-13  6:44 [Caml-list] FP's and HyperThreading Processors David McClain
2003-06-13  8:06 ` John Max Skaller
2003-06-13 10:03   ` [Caml-list] Type safe affectation ? Christophe Raffalli
2003-06-14 13:35     ` Xavier Leroy [this message]
2003-06-15 18:53       ` brogoff
2003-06-15 19:49         ` Brian Hurt
2003-06-16  1:38           ` Jacques Garrigue
2003-06-13 18:38 ` [Caml-list] FP's and HyperThreading Processors Kip Macy
2003-06-13 21:23   ` David McClain
2003-06-13 21:39     ` Kip Macy
2003-06-13 21:56       ` David McClain
2003-06-14 22:08         ` John Max Skaller
2003-06-14  6:11     ` Ville-Pertti Keinonen
2003-06-13 19:07 ` Xavier Leroy
2003-06-13 21:33   ` Jim Farrand
2003-06-13 21:39     ` David McClain
2003-07-02 10:26   ` David Monniaux
2003-06-17  0:59 [Caml-list] Type safe affectation ? Gregory Morrisett
2003-06-17 11:10 ` Christophe Raffalli
2003-06-17 14:07 Gregory Morrisett

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20030614153523.A21942@pauillac.inria.fr \
    --to=xavier.leroy@inria.fr \
    --cc=Christophe.Raffalli@univ-savoie.fr \
    --cc=caml-list@inria.fr \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).