On Sun, Jun 14, 2009 at 10:14 AM, Ralf Hemmecke wrote: > Gaby wrote: >> This patch adds ability to express that using an existential type >> scheme: >> >> x = y == >> case (x,y) is >> (x': exist(S: BasicType) . S, y': S) => x' = y' >> otherwise => EQ(x,y)$Foreign(Builtin) >> >> The expression >> >> exist(S: BasicType) . S >> >> is a type scheme saying that there is domain `S' which belongs to >> the category BasicType. Please, note that that expression does NOT >> designatue a domain. It is a type scheme. >
To me, the concept of a "type scheme" and the pattern matching introduced by the 'case' keyword seems entirely foreign to Spad. It is not like any other construction already implemented in the language. Before introducing something this drastically different in Spad I think it would good to have a motivating example much better than the Any domain. But since this is just a subjective statement Gaby might well be justified in simply dismissing it as begin "with with no sound ground or rational explanation". > In case of Any, we have > > http://svn.open-axiom.org/viewvc/open-axiom/trunk/src/algebra/any.spad.pamphlet?revision=1209&view=markup > > Rep := Record(dm: SExpression, ob: None) > > so the actual domain for x and y is explicitly given by x.dm and y.dm. > (Well, basically. Of course SExpression is not the actual domain.) > > Why would one need "exist" (in the particular case of the implementation > of Any) if it more or less could be done with current language > constructs, i.e. > ... Re-organizing your code a little if dom(x) = dom(y) then -- (+) if dom(x) has BasicType then obj(x) = obj(y) -- (*) else -- same memory address check else false I agree that there is no need to introduce type-schemes of the kind proposed by Gaby just to implement Any in a correct type-safe manner. > > (I don't argue in general against "exist", just speaking here of Any.) > Well I do argue against introducing fundamentally new low level constructs in Spad unless there is a very good reason. I think a good reference for existential types is http://portal.acm.org/citation.cfm?id=45065 @article{45065, author = {Mitchell, John C. and Plotkin, Gordon D.}, title = {Abstract types have existential type}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {10}, number = {3}, year = {1988}, issn = {0164-0925}, pages = {470--502}, doi = {http://doi.acm.org/10.1145/44501.45065}, publisher = {ACM}, address = {New York, NY, USA}, } or here: http://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf but it is not clear to me if Gaby intends existential types in OpenAxiom to implement all of the semantics for existential types that is described here. > Well that would require a definition like > > Rep == Record(X: with, obj: X) > > and > > dom: % -> with > Ralf, this nomenclature here is very poor. I would not call this domain 'with' !! There is already a domain in OpenAxiom called Domain. The proper definitions would be: Rep == Record(X: Domain, obj: X) dom: % -> Domain > Doesn't have at place (*) the compiler all knowledge it needs to figure > out that the = is actually equality from the domain dom(x) (or dom(y), > but they are identical anyway). > It is important to recall the side-effect produced by 'has'. In has ensures that all exports of BasicType are available in the then-clause. The extension to the compiler required to compile the code you propose is that the has operator must be able to take a value of type Domain on the lefthand side. dom(x) has BasicType The domain Domain is already treated in a special way by the interpreter so this extension in the compiler does not seem in any way unprecedented. Also I think it is reasonable to expect that the domain Any have the same semantics as Union in the following sense: Any == Union(d for all d in Domain) i.e. the union of all domains. The treatment of values of type Domain in 'has' is essentially the same as: (1) -> Union(String,Integer) has BasicType (1) true Type: Boolean But in defense of Gaby's approach I have to admit that the affect of 'has' on scope is in many ways the same as what he achieves in a somewhat more general manner by 'exist' and 'case'. My problem is that I think 'exist' and 'case' are too "low-level" for Spad and there introduction could have far reaching affects on how code is written in Spad and what built-in types are presumed necessary. For the most part I like the level at which most code in Spad is written now. Introducing 'exist' seems to make the resulting code a little too low-level. > Line (+) would be comparison of domains. Couldn't the compiler simply > check memory addresses here? Or would that be too naive? Equality in Domain is already defined. > I hesitate to suggest a function > > sExpression: with -> SExpression > > which would give the SExpression of a domain, because that basically > means reflection of the domain internals. I'm not sure whether any > domain or the compiler should offer such a function. > For more details of reflection in OpenAxiom take a close look at the domains Domain and Syntax. > BTW, in > > > case (x,y) is > > (x': exist(S: BasicType) . S, y': S) => x' = y' > > I don't quite understand what S, x' and y' then actually stand for. > Lacking documentation, I first thought that x' is the same as x, but > with the additional knowledge that it comes from a domain S that has > BasicType. But that doesn't make sense. Since x is either of type % or > Rep. So maybe that syntax means that x' is picking the ob entry from > > Record(dm: SExpression, ob: None) > No I don't think that is right. The new 'case' construct is a "pattern matching" operation. As I understand it it tries to match (x,y) with the pattern (x': exist(S: BasicType) . S, y': S) In effect it searches through all domains that satisfy BasicType until it finds a pair of retractions that take x into S and y into S. In that sense 'case' here is like the existing 'case' used with Union. Rather like 'has', 'case' introduces a new scope where the exports of S are available. > Would your construction also work if the representation were > > Record(ob: None, dm: SExpression, count: Integer) > > where count is just a dummy entry which is filled with a consecutive > number? Also note that I have reversed ob and dm. > Obviously yes. Regards, Bill Page. ------------------------------------------------------------------------------ Crystal Reports - New Free Runtime and 30 Day Trial Check out the new simplified licensing option that enables unlimited royalty-free distribution of the report engine for externally facing server and web deployment. http://p.sf.net/sfu/businessobjects _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
