* [newbie] Define and use records in sum types @ 2000-07-11 11:32 David Mentré 2000-07-17 10:01 ` Markus Mottl 2000-07-19 19:21 ` Jean-Christophe Filliatre 0 siblings, 2 replies; 13+ messages in thread From: David Mentré @ 2000-07-11 11:32 UTC (permalink / raw) To: caml-list Hello dear camlists, I have problems with basic record and sum types use. I would like to define a sum type with records as constructor parameters, records with the same field names. I have tried the follwing definition: <ocaml> # type asp = A of { name : string } | B of { name : string ; ext : int };; - Syntax error </ocaml> However, I can use intermediate names: <ocaml> # type a_rec = { name : string };; type a_rec = { name : string; } # type b_rec = { name : string ; ext : int };; type b_rec = { name : string; ext : int; } # type asp = A of a_rec | B of b_rec ;; type asp = A of a_rec | B of b_rec </ocaml> It *seems* to work but, in fact, the a_rec definition is masked by b_rec definition: <ocaml> # let a_b = B({name = "n" ; ext=3 }) ;; val a_b : asp = B {name="n"; ext=3} # let an_a = A({name="n"});; ---------- Some record field labels are undefined </ocaml> So my question is: is it possible to define a sum of records with the same field names? The rationale behind this question: I find records more clear that tuples in source code. Best regards, david -- David.Mentre@irisa.fr -- http://www.irisa.fr/prive/dmentre/ Opinions expressed here are only mine. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-11 11:32 [newbie] Define and use records in sum types David Mentré @ 2000-07-17 10:01 ` Markus Mottl [not found] ` <14709.63462.792269.194367@ish.artisan.com> 2000-07-19 19:21 ` Jean-Christophe Filliatre 1 sibling, 1 reply; 13+ messages in thread From: Markus Mottl @ 2000-07-17 10:01 UTC (permalink / raw) To: David Mentré; +Cc: caml-list On Tue, 11 Jul 2000, David Mentré wrote: > I would like to define a sum type with records as constructor > parameters, records with the same field names. It is unfortunately not possible to use records with the same names at the same time without putting them into separate modules. > It *seems* to work but, in fact, the a_rec definition is masked by b_rec > definition: Exactly: names of record fields get overridden by subsequent definitions. There is no way to get the "old" meaning back without the use of modules. > The rationale behind this question: I find records more clear that > tuples in source code. Using records makes sources more readable and also easier to maintain. For example, the "with" statement as in { some_record with some_field = some_value; ... } allows adding fields to records without breaking code. Best regards, Markus Mottl -- Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl ^ permalink raw reply [flat|nested] 13+ messages in thread
[parent not found: <14709.63462.792269.194367@ish.artisan.com>]
* Re: [newbie] Define and use records in sum types [not found] ` <14709.63462.792269.194367@ish.artisan.com> @ 2000-07-19 20:10 ` Markus Mottl 2000-07-21 12:23 ` Frank Atanassow 0 siblings, 1 reply; 13+ messages in thread From: Markus Mottl @ 2000-07-19 20:10 UTC (permalink / raw) To: John Gerard Malecki; +Cc: OCAML On Wed, 19 Jul 2000, John Gerard Malecki wrote: > Many of the professional programmers I show ocaml to like it very much > but are annoyed by this behavior. Maybe there is a reasonable work > around? The normal solution for the behavior of ocaml records is to > prepend the record name to the field name. For example, > > type male = { male_name : string; male_salary : int } > type female = { female_name : string; female_salary : float } Ahem, do you want to express with this example that women earn so little in your company as compared to men that you need floats to express their salary? ;-) (only joking!) Well, anyway, modules solve the problem quite well - why not use them? The effort is hardly worth mentioning. E.g.: module Male = struct type t = { name : string; salary : int } let raise_salary p n = { p with salary = p.salary + n } end module Female = struct type t = { name : string; salary : float } let raise_salary p n = { p with salary = p.salary +. n } end let _ = let male = { Male.name = "Albert"; Male.salary = 1000 } and female = { Female.name = "Berta"; Female.salary = 1000.0 } in let happy_male = Male.raise_salary male 100 and happy_female = Female.raise_salary female 100.0 and other_female = { female with Female.name = "Caroline" } in () > but then reference > > { male:salary = x } The module version nearly looks the same ("." instead of ":" and capital letter). Additionally, it forces people to introduce some modularity into the program, which is hardly a drawback. > The idea is to allow the disambiguation to be optional. It may > confuse novices but ... I'd opt against this: to me, modules already provide a regular way to organize namespaces - no need to add even further constructs to the language... Best regards, Markus Mottl -- Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-19 20:10 ` Markus Mottl @ 2000-07-21 12:23 ` Frank Atanassow 2000-07-21 20:00 ` Markus Mottl 0 siblings, 1 reply; 13+ messages in thread From: Frank Atanassow @ 2000-07-21 12:23 UTC (permalink / raw) To: Markus Mottl; +Cc: John Gerard Malecki, OCAML Markus Mottl writes: > On Wed, 19 Jul 2000, John Gerard Malecki wrote: > > type male = { male_name : string; male_salary : int } > > type female = { female_name : string; female_salary : float } > [..] > Well, anyway, modules solve the problem quite well - why not use them? The > effort is hardly worth mentioning. > > E.g.: > > module Male = struct > type t = { name : string; salary : int } > let raise_salary p n = { p with salary = p.salary + n } > end > > module Female = struct > type t = { name : string; salary : float } > let raise_salary p n = { p with salary = p.salary +. n } > end I used to do this. (Actually, in this case I would have used a functor to capture the commonality.) But I stopped because inevitably, after some development, the type t becomes recursive, and you cannot have recursive types spanning modules, so I would have to go back to the straightforward method. > > The idea is to allow the disambiguation to be optional. It may > > confuse novices but ... > > I'd opt against this: to me, modules already provide a regular way to > organize namespaces - no need to add even further constructs to the > language... I disagree. In fact, I think one should divorce the type abstraction and namespace-handling aspects of modules. It's true that the uses often coincide, but I think it obscures the issues. In particular, I think it encourages programmers to conflate syntactic information-hiding (like not exporting some constructors or functions) with type-theoretic information-hiding (like abstracting a type with a functor). The first ought to be considered only as an engineering technique to reduce complexity. The second OTOH is a logical technique to increase flexibility of implementation. As it stands, though, I realize that the current module system is far too entrenched to change, so I would be happy if we could just qualify constructor and field labels by their type constructor's name, so that this would typecheck: type r1 = { name: int } type r2 = { name: float } type t1 = A of int type t2 = A of float let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0 let (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2 I believe this issue came up a few months ago... -- 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 ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-21 12:23 ` Frank Atanassow @ 2000-07-21 20:00 ` Markus Mottl 2000-07-22 13:34 ` Frank Atanassow 0 siblings, 1 reply; 13+ messages in thread From: Markus Mottl @ 2000-07-21 20:00 UTC (permalink / raw) To: Frank Atanassow; +Cc: John Gerard Malecki, OCAML On Fri, 21 Jul 2000, Frank Atanassow wrote: > Markus Mottl writes: > > module Male = struct > > type t = { name : string; salary : int } > > let raise_salary p n = { p with salary = p.salary + n } > > end > > > > module Female = struct > > type t = { name : string; salary : float } > > let raise_salary p n = { p with salary = p.salary +. n } > > end > I used to do this. (Actually, in this case I would have used a functor to > capture the commonality.) Well, there is not so much commonality to catch in the upper example: to me, a functor would be a bit overkill here if the only thing you want to do is having a separate namespace. Unless you really see a longterm benefit in some abstraction, it's not a good idea to make the code more complex with functors. > But I stopped because inevitably, after some development, the type t > becomes recursive, and you cannot have recursive types spanning modules, > so I would have to go back to the straightforward method. Inevitably? Why? At least in the cases where I found a problem with building modules, I always discovered an easy (and generally much cleaner) way to restructure the design to get around it. In fact, such problems point me to design errors. (Yes, there are rare examples, where redesigning does not help, but I never felt the need to implement one for real purposes). > I disagree. In fact, I think one should divorce the type abstraction and > namespace-handling aspects of modules. I agree. > It's true that the uses often coincide, > but I think it obscures the issues. In particular, I think it encourages > programmers to conflate syntactic information-hiding (like not exporting some > constructors or functions) with type-theoretic information-hiding (like > abstracting a type with a functor). The first ought to be considered only as > an engineering technique to reduce complexity. The second OTOH is a logical > technique to increase flexibility of implementation. But how about "capturing logical invariants"? You need both ways of information hiding there: restricting the number of exported functions *and* restricting their types! Otherwise there could be ways to destroy the invariant. > As it stands, though, I realize that the current module system is far too > entrenched to change, so I would be happy if we could just qualify constructor > and field labels by their type constructor's name, so that this would > typecheck: > > type r1 = { name: int } > type r2 = { name: float } > type t1 = A of int > type t2 = A of float > let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0 > let (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2 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. Best regards, Markus Mottl -- Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-21 20:00 ` Markus Mottl @ 2000-07-22 13:34 ` Frank Atanassow 2000-07-22 18:31 ` Markus Mottl 0 siblings, 1 reply; 13+ messages in thread From: Frank Atanassow @ 2000-07-22 13:34 UTC (permalink / raw) To: Markus Mottl; +Cc: Frank Atanassow, John Gerard Malecki, OCAML [reusing record labels by putting them in different modules] Markus Mottl writes: > On Fri, 21 Jul 2000, Frank Atanassow wrote: > > But I stopped because inevitably, after some development, the type t > > becomes recursive, and you cannot have recursive types spanning modules, > > so I would have to go back to the straightforward method. > > Inevitably? Why? Because non-recursive datatypes are trivial, and baby programs are trivial, but they grow up into non-trivial adults. > At least in the cases where I found a problem with building modules, I > always discovered an easy (and generally much cleaner) way to restructure > the design to get around it. In fact, such problems point me to design > errors. (Yes, there are rare examples, where redesigning does not help, but > I never felt the need to implement one for real purposes). Let's not get into discussions about refactoring or recursive modules. The fact is that in your example you used only the namespace-handling aspect of modules to achieve field label overloading. The restriction against modules being recursive has nothing to do with their namespace-handling aspect, but rather implementation and type-theoretic issues. If you had opted to solve the problem by just adding a prefix to the labels (or used my proposed mechanism), and kept them in the same module, then you would not have had to appeal to (largely unrelated) issues like refactoring, and would have happily let there be recursive dependencies among the types in question, if the situation warranted it. What I'm saying is that, because the module system treats both the namespace-handling aspect and the type-theoretic aspects in one language construct, the restrictions on one aspect carry over to the other. Therefore, if you use the module system solely for namespace-handling, it's liable to bite you in the end. Of course for something like salary records, you aren't likely to engender any recursion no matter how long you develop the program; my objection is to the general applicability of the technique. > > It's true that the uses often coincide, but I think it obscures the > > issues. In particular, I think it encourages programmers to conflate > > syntactic information-hiding (like not exporting some constructors or > > functions) with type-theoretic information-hiding (like abstracting a > > type with a functor). The first ought to be considered only as an > > engineering technique to reduce complexity. The second OTOH is a logical > > technique to increase flexibility of implementation. > > But how about "capturing logical invariants"? You need both ways of > information hiding there: restricting the number of exported functions > *and* restricting their types! Otherwise there could be ways to destroy the > invariant. Can you be more specific about "capturing logical invariants"? I don't know quite what you mean. An instance I can think of where access to names could have semantic significance is if it has to do with generativity. I hate generativity with a passion, but eliminating it from ML modules would require a wholesale revision of the module system, which it is not my object to propose here. So, I will concede that generativity may cause name access to acquire semantic significance. (But I hope you agree that it is at least desirable that names and namespaces should have no semantic significance whatsoever.) BTW, I inadvertantly omitted the most important reason for namespace-handling constructs: to prevent conflicts and unwanted shadowing arising when you use modules developed by different people. > > As it stands, though, I realize that the current module system is far too > > entrenched to change, so I would be happy if we could just qualify > > constructor and field labels by their type constructor's name, so that > > this would typecheck: > > > > type r1 = { name: int } type r2 = { name: float } type t1 = A of int > > type t2 = A of float let (r2,t2) : r2 * t2 = { name = 1.0 }, A 2.0 let > > (r1,t1) : r1 * t2 = { r1.name = 1 }, t1.A 2 > > 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. In fact, I don't see how this makes programs any less readable. If you don't add this mechanism, then the rule remains, "an identifier X refers to the last definition of X in scope". If you do add this mechanism, then that doesn't change (since the identifier [path] "t.x" is still distinct from "x"). The only problem I see is that for the toplevel you will lose the ability to throw away bindings that got shadowed by newer definitions, even if they never appear inside some existing binding. But as far as I know, Ocaml's top-level doesn't garbage collect old bindings anyway, so it's a non-issue for now (unless the implementors intend to change this detail in the future). -- 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 ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-22 13:34 ` Frank Atanassow @ 2000-07-22 18:31 ` Markus Mottl 2000-07-23 13:55 ` Frank Atanassow 0 siblings, 1 reply; 13+ messages in thread From: Markus Mottl @ 2000-07-22 18:31 UTC (permalink / raw) To: Frank Atanassow; +Cc: John Gerard Malecki, OCAML On Sat, 22 Jul 2000, Frank Atanassow wrote: > > But how about "capturing logical invariants"? You need both ways of > > information hiding there: restricting the number of exported functions > > *and* restricting their types! Otherwise there could be ways to destroy the > > invariant. > > 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). > An instance I can think of where access to names could have semantic > significance is if it has to do with generativity. I hate generativity with a > passion, but eliminating it from ML modules would require a wholesale revision > of the module system, which it is not my object to propose here. So, I will > concede that generativity may cause name access to acquire semantic > significance. (But I hope you agree that it is at least desirable that names > and namespaces should have no semantic significance whatsoever.) 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. > > 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... What concerns type names: I guess this is a consequence of having an "open"-statement for modules, which shadows previous type declarations. Otherwise, forbidding it would probably be a good idea since its scope is the whole module from the point of definition. 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. 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... > 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... > If you don't add this mechanism, then the rule remains, "an identifier X > refers to the last definition of X in scope". Yes. > If you do add this mechanism, then that doesn't change (since the identifier > [path] "t.x" is still distinct from "x"). Right. But you have to invent additional syntax for doing this. Even though it seems to be a rather marginal addition, it also adds to making the language more complex. I haven't felt the need for it so far, but if other people have other requirements, they are free to ask for it... Regards, Markus Mottl -- Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-22 18:31 ` Markus Mottl @ 2000-07-23 13:55 ` Frank Atanassow 2000-07-23 15:20 ` Markus Mottl 0 siblings, 1 reply; 13+ messages in thread From: Frank Atanassow @ 2000-07-23 13:55 UTC (permalink / raw) To: Markus Mottl; +Cc: Frank Atanassow, John Gerard Malecki, OCAML 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 ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-23 13:55 ` Frank Atanassow @ 2000-07-23 15:20 ` Markus Mottl 2000-07-24 9:28 ` Frank Atanassow 0 siblings, 1 reply; 13+ messages in thread From: Markus Mottl @ 2000-07-23 15:20 UTC (permalink / raw) To: Frank Atanassow; +Cc: John Gerard Malecki, OCAML On Sun, 23 Jul 2000, Frank Atanassow wrote: > 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. The abstract type refers to a specific representation (you can't mix different ones - quantification on type), but also does not allow you to use datastructures of the same representation that were not created by the "right" functions (= quantification on values). That's at least what I think you mean - I am not a type-theorist. > 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. Right: you can make *some* functions available this way, but not all! There may be functions that are not defined (crash, loop, whatever) for all values, only for ones for which some semantic property holds. However, it may not even be the case that it holds for the abstract type itself, but only for the specific way in which the function is called internally, i.e. the precondition for the function to work correctly is stronger. You therefore still need means to hide such functions. In fact, I use your "trick of revelation" in some projects to export the internal representation of the abstract types safely and without computational costs. E.g. with the set-example val list_of_set : 'a set -> 'a list This could be the identity function internally. If I change the representation, I'd only have to write a conversion function. Of course, one shouldn't do such things with mutable values... > 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. Well, category theory is on my "to-learn-list" ;) I understand only some basic notions that allow me to make practical use of them (e.g. partial evaluation of strict languages with effects (impure functions, non-termination) using monads to handle the effect stuff). > 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.) Ok, I see what you mean (meant). > 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. Ok, this is a reasonable way to do it: I'd also like to be "kicked" by the compiler when I open several modules that have common names and when I indeed use one of them. This is bad style - other readers might become confused about what the program means (not everybody likes reading 1000 lines to find out about the order of import). So using this "lazy boot" to kick me would be fine. Maybe there could be a warning option for this in OCaml? > But that's just FYI; I'm not suggesting that Ocaml's shadowing rules be > changed in any way. This would also surely break tons of code (legacy is a burden). But I don't consider it to be so bad at all... > 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.) Well, there are also other reasons having to do with "shadowing module names" during linking... I don't know whether this "shadowing feature" is so useful at all. It just provokes bad style where a functor would be more appropriate. If we take out this feature and only allow side effecting value definitions in one module (better: compilation unit), then we could finally end up with a much nicer linking semantics (-> commuting module names! Great!). > > 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? I don't want to write { t1.v1 = x; t1.v2 = y; ... } but something similar to: { t1 | v1 = x; v2 = y; ... } However, maybe there could be a solution that makes use of the type system? (Though, I fear that this would require very incompatible changes). Could mandatory type annotations help here? I think there are several occasions where they might help, but I am not an expert here - maybe someone else can tell us more about this. If I am not mistaken, this could help solve this problem besides polymorphic recursion and maybe also remove the need for type coercions for objects (e.g. when you put several ones of different type into a list). > 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. This may be true - or not: I don't know. As I said: if enough people say "this is intuitive", I wouldn't be opposed to it. I don't feel annoyed by such a feature, but that's not enough to add it, because there are a zillion things that do not annoy me... > 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. Well, we are already nearly at mandatory type annotations ;-) Let's wait and see what people think of this problem in general. If it is important enough to them, they will say so... Best regards, Markus Mottl -- Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-23 15:20 ` Markus Mottl @ 2000-07-24 9:28 ` Frank Atanassow 2000-07-25 5:26 ` Alan Schmitt 0 siblings, 1 reply; 13+ messages in thread From: Frank Atanassow @ 2000-07-24 9:28 UTC (permalink / raw) To: Markus Mottl; +Cc: Frank Atanassow, John Gerard Malecki, OCAML Markus Mottl writes: > On Sun, 23 Jul 2000, Frank Atanassow wrote: > > 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. > > The abstract type refers to a specific representation (you can't mix > different ones - quantification on type), but also does not allow you to > use datastructures of the same representation that were not created by the > "right" functions (= quantification on values). That's at least what I > think you mean - I am not a type-theorist. > > > 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. > > Right: you can make *some* functions available this way, but not all! There > may be functions that are not defined (crash, loop, whatever) for all > values, only for ones for which some semantic property holds. I guess you mean a situation like this: module type FLAG = sig type t val from : bool -> t val to : t -> bool end module Flag3 = struct type t = On | Off | Undecided let from = function true -> On | false -> Off let to = function On -> true | Off -> false end module Flag : FLAG = Flag3 The thinking would be, then, that with the concrete representation I could construct a value Flag3.Undecided : Flag3.t which would cause Flag3.to to fail, whereas with Flag I cannot ever construct an Undecided variant, so Flag.to is effectively total. Correct? But while Flag3.Undecided is admittedly special (being a constructor), it is nevertheless an ordinary function. Hence it can be included in the scope of the quantification or not. If I quantify over it, then Flag = Flag3. If I don't quantify over it, but still include it in the signature, then Flag.Undecided : Flag3.t, so Flag.t only exposes two variants. Do you still think there is a situation where name-hiding is necessary in addition to type abstraction? > However, it > may not even be the case that it holds for the abstract type itself, but > only for the specific way in which the function is called internally, i.e. > the precondition for the function to work correctly is stronger. You > therefore still need means to hide such functions. I'm not sure I understand, but I think you are imagining a partial, auxiliary function which is only used internally. In that case, you can always define it locally, in the scope of a let-expression, say. However, if you have to use this function (call it aux) multiple times in different top-level definitions, you will end up convoluting your code. E.g., module M = struct let aux = ... let f1 = ... aux ... let f2 = ... aux ... end becomes module M = struct let (f1,f2) = let aux = ... in let f1 = ... aux ... in let f2 = ... aux ... in (f1, f2) end which is admittedly unsavory. > In fact, I use your "trick of revelation" in some projects to export the > internal representation of the abstract types safely and without > computational costs. E.g. with the set-example > > val list_of_set : 'a set -> 'a list > > This could be the identity function internally. If I change the > representation, I'd only have to write a conversion function. Of course, > one shouldn't do such things with mutable values... OK, this is a situation that doesn't fit my model. If you include a function in the scope of the quantification, you have to substitute all the occurrences in its type signature of the concrete type with the new abstract type. BTW, this discussion is no longer relevant to the discussion on field label syntax, so let's take it to e-mail from now on, OK? > > > 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? > > I don't want to write > > { t1.v1 = x; t1.v2 = y; ... } > > but something similar to: > > { t1 | v1 = x; v2 = y; ... } I see. You mean a "declaration" within the record-building syntax. Yeah, it is better to avoid repetition, and avoid making the programmer remember which labels are used in multiple record types. BTW, here is the URL of a previous discussion on this subject in the archives: http://pauillac.inria.fr/caml/caml-list/1136.html http://pauillac.inria.fr/caml/caml-list/1203.html (follow the thread) (There is also a long post somewhere by Xavier on the type inference problem with records, but I couldn't find it.) A solution suggested in the archives is to allow type declarations like: type point = Pt of { x: float; y: float } (Incidentally, this is how it is done currently in Haskell.) -- 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 ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-24 9:28 ` Frank Atanassow @ 2000-07-25 5:26 ` Alan Schmitt 0 siblings, 0 replies; 13+ messages in thread From: Alan Schmitt @ 2000-07-25 5:26 UTC (permalink / raw) To: caml-list Hi, >BTW, here is the URL of a previous discussion on this subject in the archives: > > http://pauillac.inria.fr/caml/caml-list/1136.html > http://pauillac.inria.fr/caml/caml-list/1203.html (follow the thread) > Why not use the new archiving of the list: http://pauillac.inria.fr/caml/archives/199902/msg00097.html http://pauillac.inria.fr/caml/archives/199903/msg00049.html >(There is also a long post somewhere by Xavier on the type inference problem >with records, but I couldn't find it.) This archiving system comes with a pretty good search engine: http://pauillac.inria.fr/bin/wilma/caml-list Alan Schmitt -- The hacker: someone who figured things out and made something cool happen. ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-11 11:32 [newbie] Define and use records in sum types David Mentré 2000-07-17 10:01 ` Markus Mottl @ 2000-07-19 19:21 ` Jean-Christophe Filliatre 2000-07-20 7:08 ` David Mentré 1 sibling, 1 reply; 13+ messages in thread From: Jean-Christophe Filliatre @ 2000-07-19 19:21 UTC (permalink / raw) To: David Mentré; +Cc: caml-list > I have problems with basic record and sum types use. > > I would like to define a sum type with records as constructor > parameters, records with the same field names. > > I have tried the follwing definition: > > <ocaml> > # type asp = A of { name : string } | B of { name : string ; ext : int };; > - > Syntax error > </ocaml> I don't know what you want to do exactly, but I applied to following idea (which you can find in the ocaml sources) for AST tagged with common informations: type t = { name : string; info : u } and u = A | B of int (in the case of AST, t and u are really mutually recursive, with occurrences of t in the arguments of u's constructors) Then you can still make pattern-matching like this match x.info with A -> ... | B n -> ... and still access the name field with x.name. Hops this helps, -- Jean-Christophe Filliatre Computer Science Laboratory Phone (650) 859-5173 SRI International FAX (650) 859-2844 333 Ravenswood Ave. email filliatr@csl.sri.com Menlo Park, CA 94025, USA web http://www.csl.sri.com/~filliatr ^ permalink raw reply [flat|nested] 13+ messages in thread
* Re: [newbie] Define and use records in sum types 2000-07-19 19:21 ` Jean-Christophe Filliatre @ 2000-07-20 7:08 ` David Mentré 0 siblings, 0 replies; 13+ messages in thread From: David Mentré @ 2000-07-20 7:08 UTC (permalink / raw) To: Jean-Christophe Filliatre; +Cc: caml-list Jean-Christophe Filliatre <filliatr@csl.sri.com> writes: > type t = { name : string; info : u } > and u = A > | B of int Many thanks to all people that kindly respond. It was pretty much the solution I took. d. -- David.Mentre@irisa.fr -- http://www.irisa.fr/prive/dmentre/ Opinions expressed here are only mine. ^ permalink raw reply [flat|nested] 13+ messages in thread
end of thread, other threads:[~2000-07-25 22:00 UTC | newest] Thread overview: 13+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2000-07-11 11:32 [newbie] Define and use records in sum types David Mentré 2000-07-17 10:01 ` Markus Mottl [not found] ` <14709.63462.792269.194367@ish.artisan.com> 2000-07-19 20:10 ` Markus Mottl 2000-07-21 12:23 ` Frank Atanassow 2000-07-21 20:00 ` Markus Mottl 2000-07-22 13:34 ` Frank Atanassow 2000-07-22 18:31 ` Markus Mottl 2000-07-23 13:55 ` Frank Atanassow 2000-07-23 15:20 ` Markus Mottl 2000-07-24 9:28 ` Frank Atanassow 2000-07-25 5:26 ` Alan Schmitt 2000-07-19 19:21 ` Jean-Christophe Filliatre 2000-07-20 7:08 ` David Mentré
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox