From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA02905 for caml-red; Sun, 23 Jul 2000 17:22:59 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA10573 for ; Sun, 23 Jul 2000 15:55:29 +0200 (MET DST) Received: from mail.cs.uu.nl (sunset.cs.uu.nl [131.211.80.32]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e6NDtS909953 for ; Sun, 23 Jul 2000 15:55:28 +0200 (MET DST) Received: from silvester.cs.uu.nl.cs.uu.nl (silvester.cs.uu.nl [131.211.80.119]) by mail.cs.uu.nl (Postfix) with ESMTP id BDF09451B; Sun, 23 Jul 2000 15:55:27 +0200 (MET DST) From: Frank Atanassow MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-ID: <14714.63823.257355.941516@silvester.cs.uu.nl> Date: Sun, 23 Jul 2000 15:55:27 +0200 (MET DST) To: Markus Mottl Cc: Frank Atanassow , John Gerard Malecki , OCAML Subject: Re: [newbie] Define and use records in sum types In-Reply-To: <20000722203116.A8157@miss.wu-wien.ac.at> References: <20000717120151.A32148@miss.wu-wien.ac.at> <14709.63462.792269.194367@ish.artisan.com> <20000719221048.B23676@miss.wu-wien.ac.at> <14712.16572.925353.202223@silvester.cs.uu.nl> <20000721220058.A29053@miss.wu-wien.ac.at> <14713.41688.558933.239829@silvester.cs.uu.nl> <20000722203116.A8157@miss.wu-wien.ac.at> X-Mailer: VM 6.75 under Emacs 20.4.1 Sender: weis@pauillac.inria.fr Markus Mottl writes: > > Can you be more specific about "capturing logical invariants"? I don't > > know quite what you mean. > > If you have axioms that specify invariant properties about the types and > functions in question. E.g. that removing an element from a set results in > a set that does not contain it and that this is true for all sets. > > Exporting auxiliary functions from the module might allow the programmer to > violate this condition. The same is true for not restricting the types of > the functions. Therefore, you need both means of information hiding to > guarantee correctness (i.e. the properties in question). I don't think that has anything to do with hiding values, or if it does, it needn't. Suppose I want to define a type of sets, but I don't want to reveal the fact that I'm using lists to do it. module type SET = sig type 'a set val union : 'a set -> 'a set -> 'a set end module ListSet = struct type 'a set = 'a list let removeDup m = ... let union m n = removeDup (m @ n) end module Set = ListSet : SET (removeDup doesn't break the abstraction since it's the identity on sets, but for the sake of brevity suppose it did.) Here is my rendition of what the signature restriction to SET is doing: 1) It existentially introduces a new type 'a Set.set, whose witness is 'a list, and at the same time introduces a new value Set.union, with occurrences of 'a ListSet.list replaced by 'a Set.set in its type, whose witness is ListSet.union. 2) It hides all the names defined in ListSet. This includes ListSet.union as well as ListSet.removeDup (and ListSet.set). So the type-theoretic role of the signature restriction is to do existential quantification (or something close to it), and delimit the scope of the quantification on types and values. However, there is no reason why it needed to hide, e.g., ListSet.removeDup. It could have also added removeDup to Set also, without breaking abstraction, as long as it weren't included in the scope of the quantification. Then Set.removeDup would have type 'a list -> 'a list, so you couldn't apply it to sets, so there is no problem. I think that this is close to what Ocaml does, though I wouldn't swear to it. BTW, if you are familiar with category theory, then you will know that all this stuff, even the binding syntax for quantification and abstraction, can be translated into a purely semantic, variable-free form. Ipso facto, you don't need syntactic notions like names or name-hiding to express it. > I guess you mean that it is only the structure of the module that counts > and not the naming? But how about ambiguities then? You need a way to refer > to the right function, whatever, if it has the same signature as another > one. Nono, identity is important. I'm just saying identifier visibility and renaming should have nothing to do with semantics. (Scope is important, though. By "visibility doesn't matter", I guess I mean you should never need to _remove_ an identifier from the set of free variables in a subterm.) > > > I'd rather use different namings like "r1_name" and "r2_name" for the > > > field: although this requires me to always include the name of the > > > type, one cannot get confused either: it makes the sources easier to > > > understand. > > > > I don't find that argument very convincing; Ocaml _already_ allows type, > > value and field label definitions to shadow each other, which many people > > consider a cognitive burden. I don't have an opinion on that issue; I'm > > just trying to be consistent with the way Ocaml treats bindings > > currently, and add a little bit more flexibility. > > There's not much you can do about shadowing of value bindings unless you > prohibit it which would cause other problems: you'd have to invent a new > name each time even if you just want to "transform" a value using the same > name - this could cause horror if you wanted to add such a transformation > in the middle of a function body... Well, I disagree that nothing can be done about it. Personally, I wouldn't mind so much if shadowing were outlawed entirely, but a less drastic solution is the one adopted by Haskell and Mercury, in which one distinguishes top-level bindings from local ones, and "lazily" disallow shadowing at the top level. This means that you can import distinct values with the same name, but you only get an error if the name is actually used somewhere in the module. But that's just FYI; I'm not suggesting that Ocaml's shadowing rules be changed in any way. Frankly, I think Ocaml's perspective, that top-level value bindings are treated essentially the same way as local bindings, is nicely consistent in its own way, though. (However, it arguably causes problems too, since side-effects at the top level makes module-linking order significant.) > Now, accessing fields more flexibly is surely possible. The question is > whether adding this feature is really of so much help: the only case where > it pays off is when you have large records which share a great deal of > names. It pays off when you have records which share names, period. In that case it improves readability, in the sense that "r.label" is easier to read than "r.prefix_label". > Then it might be a bit more convenient to have an initial declaration that > tells the compiler what kind of record you are talking about instead of > inventing new names for records. A rather statistical question... What sort of declaration? > > In fact, I don't see how this makes programs any less readable. > > It adds another construct that people have to learn. Reading constructs > that you are not familiar with is confusing. I bet that there are plenty of > people who do not even know about the "with"-construct for records... But this construct is closely analogous to the existing dot-notation for modules. For all we know, it may turn out that some programmers actually mistakenly assume it already exists. However, it occurs to me now that my syntax would bring type names into the same namespace as field labels. The reason is because of the ambiguity: does "m.t.x" mean "the field x of the t-record m", or "the field x of the field t of the record m"? I guess having type names and labels in the same namespace is bad, so you would want a different syntax, maybe "m:t.x" for selection and { x = ... } : t for building. I guess that makes it essentially the same as SML's records. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791