From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA15708; Thu, 18 Apr 2002 11:04:20 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 LAA15704 for ; Thu, 18 Apr 2002 11:04:19 +0200 (MET DST) Received: from sunny.pacific.net.au (sunny.pacific.net.au [203.25.148.40]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g3I94Hb17324 for ; Thu, 18 Apr 2002 11:04:17 +0200 (MET DST) Received: from wisma.pacific.net.au (wisma.pacific.net.au [210.23.129.72]) by sunny.pacific.net.au with ESMTP id g3I94EXt010127; Thu, 18 Apr 2002 19:04:14 +1000 (EST) Received: from ozemail.com.au (ppp48.dyn71.pacific.net.au [202.7.71.48]) by wisma.pacific.net.au with ESMTP id TAA04181; Thu, 18 Apr 2002 19:04:10 +1000 (EST) Message-ID: <3CBE8C0A.7000500@ozemail.com.au> Date: Thu, 18 Apr 2002 19:04:10 +1000 From: John Max Skaller User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:0.9.2.1) Gecko/20010901 X-Accept-Language: en-us MIME-Version: 1.0 To: Jacques Garrigue CC: caml-list@inria.fr Subject: Re: [Caml-list] Polymorphic variants References: <3CBD4523.6080707@ozemail.com.au> <87y9fmr4fo.dlv@wanadoo.fr> <3CBE0A20.9090508@ozemail.com.au> <20020418102357P.garrigue@kurims.kyoto-u.ac.jp> Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Jacques Garrigue wrote: >>BTW: I can't write "t as x" in a type expression. Why not? >>I'm forced to name it in a type binding .. that means that inductive types, >>for example, can not be specified anonymously: >> >> [`Cons of list | `Empty] as list >> >>should work. [Can I use a 'constraint' here? I've never used >>a constraint before] >> > >Yes you can. Wasn't it in the tutorial: > > [`Cons of 'list | `Empty] as 'list > Argg. Sorry. Of course, I used a plain identifier instead of a type variable. >>It doesn't "must" be done. I think you mean, there are advantages >>only handling the easy cases: easy to write the compiler, >>easy to optimise, easy for the end user to monitor >>code complexity .. and easy for the programmer to handle >>the more difficult cases manually .. >> > >Not only that: easily understandable properties. This is the most >important part. > Yes, but it is an amorphous thing. The specification of an 'integer' is easily understandable. Only, the greatest minds in mathematics struggle to know what a prime number is. >>I certainly can write them both: >> >>`A 1; `A 1.1; >>type int_t = [`A of int]; >>type float_t = [`A of float];; >> >>No problem doing this. Perhaps there should be. >> > >There is no problem as long as these cases are used independently. >But you cannot mix them in the same variant type. > Yeah, I know .. but it isn't clear from the manual, perhaps because this very example is not included in it. > >How are we going to build a model of [`A of int | `A of float]. >Basically this suppose that we are able to build the union set of >ints and floats. All the type theory theory of ML is based on the fact >that there is no such set/type. > Not at all. Felix does this, just fine. And I'm no type theorist. But the algorithms work. I'm not saying ocaml should do what I did in Felix, but there is no problem at all building a model, `A is just a function, and in Felix functions can be overloaded. Including variant constructors. [These are classic ML style unions, not open ones like polymorphic variants: they have to be declared or it wouldn't work] In Felix, it is fine to duplicate not just constructors, but any function type: fun f:x->y = .. fun f:x->y= .. No problem. But here: print (f x); there is a problem: which f to use? Is this a good design decision? I don't know: I *could* report a duplicate definition (and I *do* for duplicate things other than than functions). But there is evidence that this IS a good design decision, it comes from overloading templates in C++. Since a template basically models a family of functions, two tempates often model the same type .. and it would be really silly to ban the templates because of this. Instead, an error is reported only when a particular instantiation is ambiguous. I'm not criticizing the decisions made for polymorphic variants, just pointing out that a lot of alternatives do exist, and it would be useful to see an explanation of why the various interesting nasty cases are handled the way they are. > >What this basically means is that any use of `A without type >annotation should generate an error. The whole point of polymorphic >variants being that they are independent from definitions, I really >cannot follow you here. > Nor I you. When the compiler sees: `A 1 in an expression then it silently replaces it with `A_int 1 so that the actual constructor name is distinct for every argument type. This is called 'name mangling' and C++ compilers do it all the time to every external function symbol in a program. In a pattern match, there is a problem because the mangling cannot be done when the expression being decoded is of a type with two constructor of the same unmangled name. So in this case ONLY, the client must disambiguate by specifying which type is meant: `A (x:int) is replaced by `A_int x > >Sorry, but the feature you are asking for is not polymorphic variants. > I am NOT asking for it. I am merely critiquing it from the point of view of a user. Remember, I am using them: the whole of my compiler uses polymorphic variants extensively and almost exclusively (only a few of the traditional sum types remain in a couple of places because there is no point replacing them). So you could say I'm a fairly heavy user of them :-) >>Things "must be so" if they are a consequence of theory, but it >>isn't always evident which theory is used, and why that one is best >>:-) >> > >Read the papers :-) >There is a whole literature about lambda-calculus, type systems, >models... >One trouble is that it is hard to explain all this theory in a few >lines. > And the other is that there are a LOT of theories. Furthermore, the theory upon which an implementation is based doesn't determine all the technical design decisions: like, for example, whether to report that a type with duplicate constructors is an error even if it isn't used, or whether to defer the error to the point of use .. and provide a disambiguation mechanism. C++ for example, adopts BOTH of these philosophies in different places, which is one reason it is a mess. >>Perhaps one consequence of this is that the documentation >>needs to be more specific and have more examples: >>the author knowing the chosen theory and implementation >>believes only lightweight coverage is necessary, not seeing >>the many alternatives someone less involved might. >> > >You're probably right. But your remark also describes the basic >problem: as long as the author is the only one to document a feature, >his description will only be partial. > So add in the example I gave? I can't do that, I don't have access to the document source. But I have 'documented' it in the email :-) > >Note that one could think of ways to make the above legal, using >intersection rather than union, but I don't see how it would be >useful, because you would have no way to access the value anyway. >Like throwing data into a black hole. > The pragmatics of programming often require useless things. For example, unreachable code .. because the programmer has commented something out. Empty types (why was [] removed??) because they're yet to be filled in with cases, but we want to name the type anyhow, perhaps to write a function signature .. The unit type. It is theoretically useless in a (purely) functional programming language. Why is it there? >>Well, having looked at the English translation of the >>Ocaml book by Emmanuel Chailloux, Pascal >>Manoury and Bruno Pagano, I think a big hole is going >>to be plugged. This book covers quite advanced topics, >>I might learn something here! >> > >This is indeed a nice book, but written before the introduction of >polymorphic variants. So almost nothing about them in it. > >Actually, this is one reason I would want to say: now polymorphic >variants are finished, let's work with them, and try to describe what >they can do. This is too hard to do that on a moving target. > Well, I'm doing my part: I'm using them all the time, and I'm relating my experience so you can get some feeling for how someone else views them that is. I was hoping to get much stronger static typing using them. In fact, I have better typing, but nowhere near as strong as I either expected initially, or would like. Some of the typing I'd like is plain impossible. And some is inconvenient to implement, or too quirky to bother with. And some is desirable but not implemented or not understood. And I don't really know the distinction between all these cases. -- John Max Skaller, mailto:skaller@ozemail.com.au snail:10/1 Toxteth Rd, Glebe, NSW 2037, Australia. voice:61-2-9660-0850 ------------------- 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