|
|
last edited 16 years ago |
1 | ||
Editor:
Time: 2007/11/17 22:31:07 GMT-8 |
||
Note: then fix 'ANY1' |
changed: - The Boolean test for equality in the domain Any fails for structured objects, e.g. of type List: \begin{axiom} )set message any off showTypeInOutput true; \end{axiom} \begin{axiom} a:Any:=[1,2] b:Any:=[1,2] a=b test % \end{axiom} Proposed Fix The problem seems to be the use of Lisp EQ instead of EQUAL in the domain Any. \begin{spad} ++ Author: Robert S. Sutor ++ Date Created: ++ Change History: ++ Basic Functions: any, domainOf, objectOf, dom, obj, showTypeInOutput ++ Related Constructors: AnyFunctions1 ++ Also See: None ++ AMS Classification: ++ Keywords: ++ Description: ++ \spadtype{Any} implements a type that packages up objects and their ++ types in objects of \spadtype{Any}. Roughly speaking that means ++ that if \spad{s : S} then when converted to \spadtype{Any}, the new ++ object will include both the original object and its type. This is ++ a way of converting arbitrary objects into a single type without ++ losing any of the original information. Any object can be converted ++ to one of \spadtype{Any}. Any(): SetCategory with any : (SExpression, None) -> % ++ any(type,object) is a technical function for creating ++ an object of \spadtype{Any}. Arugment \spad{type} is a \spadgloss{LISP} form ++ for the type of \spad{object}. domainOf : % -> OutputForm ++ domainOf(a) returns a printable form of the type of the ++ original object that was converted to \spadtype{Any}. objectOf : % -> OutputForm ++ objectOf(a) returns a printable form of the ++ original object that was converted to \spadtype{Any}. dom : % -> SExpression ++ dom(a) returns a \spadgloss{LISP} form of the type of the ++ original object that was converted to \spadtype{Any}. obj : % -> None ++ obj(a) essentially returns the original object that was ++ converted to \spadtype{Any} except that the type is forced ++ to be \spadtype{None}. showTypeInOutput: Boolean -> String ++ showTypeInOutput(bool) affects the way objects of ++ \spadtype{Any} are displayed. If \spad{bool} is true ++ then the type of the original object that was converted ++ to \spadtype{Any} will be printed. If \spad{bool} is ++ false, it will not be printed. == add Rep := Record(dm: SExpression, ob: None) printTypeInOutputP:Reference(Boolean) := ref false obj x == x.ob dom x == x.dm domainOf x == x.dm pretend OutputForm x = y == (x.dm = y.dm) and EQUAL(x.ob, y.ob)$Lisp objectOf(x : %) : OutputForm == spad2BootCoerce(x.ob, x.dm, list("OutputForm"::Symbol)$List(Symbol))$Lisp showTypeInOutput(b : Boolean) : String == printTypeInOutputP := ref b b=> "Type of object will be displayed in output of a member of Any" "Type of object will not be displayed in output of a member of Any" coerce(x):OutputForm == obj1 : OutputForm := objectOf x not deref printTypeInOutputP => obj1 dom1 := p:Symbol := prefix2String(devaluate(x.dm)$Lisp)$Lisp atom?(p pretend SExpression) => list(p)$List(Symbol) list(p)$Symbol hconcat cons(obj1, cons(":"::OutputForm, [a::OutputForm for a in dom1])) any(domain, object) == (isValidType(domain)$Lisp)@Boolean => [domain, object] domain := devaluate(domain)$Lisp (isValidType(domain)$Lisp)@Boolean => [domain, object] error "function any must have a domain as first argument" \end{spad} Re-test \begin{axiom} )set message any off showTypeInOutput true; \end{axiom} \begin{axiom} a:Any:=[1,2] b:Any:=[1,2] a=b test % \end{axiom} See also SandBoxSetAny From billpage Thu Apr 5 11:38:24 -0500 2007 From: billpage Date: Thu, 05 Apr 2007 11:38:24 -0500 Subject: domain Any Message-ID: <20070405113824-0500@wiki.axiom-developer.org> Category: Aldor Library Compiler => Axiom Library Status: open => fix proposed From kratt6 Thu Apr 5 16:15:06 -0500 2007 From: kratt6 Date: Thu, 05 Apr 2007 16:15:06 -0500 Subject: works only if canonical Message-ID: <20070405161506-0500@wiki.axiom-developer.org> I'm afraid that the design of the equality test in 'ANY' is completely broken. One would really need to call the appropriate '=' from the domain, but I don't think that this is possible in Axiom: \begin{axiom} p: Set ANY := set [1,2]; q: Set ANY := set [2,1]; test(p=q) test(p::ANY=q::ANY) \end{axiom} If the domain has 'canonical', the test using 'EQUAL' might work... \begin{axiom} test((3/4)::ANY = (3/4)::ANY) \end{axiom} Martin From kratt6 Thu Apr 5 16:54:17 -0500 2007 From: kratt6 Date: Thu, 05 Apr 2007 16:54:17 -0500 Subject: Better definition Message-ID: <20070405165417-0500@wiki.axiom-developer.org> Maybe the following definition works, at least, it seems to. Note that we should ask for 'BasicType', because otherwise equality is not even defined. \begin{verbatim} x = y == if (x.dm = y.dm) then D := (x.dm pretend BasicType) X:D := (obj x) pretend D Y:D := (obj y) pretend D (X=Y)$D else false \end{verbatim} I'm not sure how the correspondence 'SEX' and Type ought to work... From BillPage Thu Apr 5 23:45:34 -0500 2007 From: Bill Page Date: Thu, 05 Apr 2007 23:45:34 -0500 Subject: Excellent! Message-ID: <20070405234534-0500@wiki.axiom-developer.org> Martin, I like your "better definition" very much! I guess what you are not sure about is the reasonableness of:: D := (x.dm pretend BasicType) as a way to turn a member of the domain (SExpression) into a Type given that the representation of x is:: Record(dm: SExpression, ob: None) Of course the "normal" use of pretend is to treat a member of one domain "as if" it was a member of another domain but in this case you are treating a member of a domain as if it was a member of a category, i.e. a domain. That is very cool! In fact it's downright wonderful -- truly types as first class values in SPAD. I think your code ok since as I near as I can understand after some emails exchanged with Peter Broadbery #209 and in spite of nearly no documentation in "interop.boot.pamphlet":/axiom--test--1/src/interp/InteropBoot the Boot function:: devaluate(domain)$Lisp ensures that the domain will be representable as an Axiom SExpression. From kratt6 Fri Apr 6 00:36:48 -0500 2007 From: kratt6 Date: Fri, 06 Apr 2007 00:36:48 -0500 Subject: going further Message-ID: <20070406003648-0500@wiki.axiom-developer.org> So, if 'D := (x.dm pretend BasicType)' is OK, we should go further, and work a little on 'ANY'. At least, it should throw an error if 'x.dm' is not a 'BasicType'. In fact, I doubt, that 'ANY' should export equality at all. Is this functionality used anywhere? Similarly, should 'ANY' support coercion to 'OUTFORM' for *any* object? Martin From billpage Sat Apr 7 01:17:17 -0500 2007 From: billpage Date: Sat, 07 Apr 2007 01:17:17 -0500 Subject: Re: coercion to OUTFORM Message-ID: <20070407011717-0500@wiki.axiom-developer.org> I don't understand your question. The domain ANY already supports coercion to OUTFORM. We are using it in the examples on this page. You wrote:: In fact, I doubt, that ANY should export equality at all. Is this functionality used anywhere? Yes, for example in the domain Set(Any). Are you familiar with the functions defined in the ANY1 package? See also the page: DuckTyping From kratt6 Sat Apr 7 02:56:26 -0500 2007 From: kratt6 Date: Sat, 07 Apr 2007 02:56:26 -0500 Subject: being more precise Message-ID: <20070407025626-0500@wiki.axiom-developer.org> I see the situation as follows: an object in 'ANY' may *currently* be of any 'Type'. However, 'ANY' has 'SetCategory', i.e., it supports coercion to 'OutputForm' and equality. Thus, via 'ANY', *any* domain becomes of type 'SetCategory', which is something I do not like. As far as I can see, the only way apart from 'pretend' to create an object of type 'ANY' is via 'coerce$ANY1'. So, I'd suggest that we modify 'ANY1' to accept only arguments that have 'SetCategory'. If we want to support things that do not have equality, for example, we should create another domain, similar to 'ANY', that only has 'KOERCE OUTFORM', but I doubt that this is useful. In any case, I like the 'Object' implementation in the Aldor Compiler User Guide much better. Martin From billpage Sun Apr 8 00:35:12 -0500 2007 From: billpage Date: Sun, 08 Apr 2007 00:35:12 -0500 Subject: Re: Object domain in Aldor Message-ID: <20070408003512-0500@wiki.axiom-developer.org> http://www.aldor.org/docs/HTML/chap26.html#24 Does not seem to give much information about Object except:: Description: 'Object(C)' implements dynamic objects, pairing data values with associated domains. and that it exports two functions:: object : (T: C, T) -> % 'object(T, t)', where the type of `t' is `T', creates on object of the domain. avail : % -> (T: C, T) Can you say more about this domain and why you "like it much better"? From kratt6 Mon Apr 9 14:16:49 -0500 2007 From: kratt6 Date: Mon, 09 Apr 2007 14:16:49 -0500 Subject: Aldor Object Message-ID: <20070409141649-0500@wiki.axiom-developer.org> The difference between 'Object' and 'Any' is that the former stays much more in line with the strict typing philosophy. I believe that 'Any' was rather a hack to put up with the lack of dependent types as needed for the 'series' operations. The idea behind 'Object' is to wrap up an object together with its type. Thus, the operation 'object' corresponds to 'coerce\$ANY1', and 'avail' is roughly 'dom' and 'obj' followed by 'retract\$ANY1(dom)', except that the latter won't work... I'd say that 'Object' is rarely needed in Aldor. I guess, one cannot easily write 'Object' using SPAD, because of the lack of dependent types. I was probably too quick to say that I like 'Object' much better. I should have said: I like dependent types much better... From BillPage Mon Apr 9 14:36:32 -0500 2007 From: Bill Page Date: Mon, 09 Apr 2007 14:36:32 -0500 Subject: Re: Any is a hack? Message-ID: <20070409143632-0500@wiki.axiom-developer.org> I disagree that the domain Any is a hack (if you mean this word in the pejorative sense like "trick" or "quick fix"). Rather this domain implements DuckTyping in Axiom and DuckTyping is an important method of dealing with dynamic types in an otherwise statically typed language. These methods are popular in languages like Java, Python, Ruby etc. Since Martin showed earlier on this page how to deal with types in a first order fashion, then I think it is now clear that these methods could also be usefully applied in Axiom and the Axiom library. I am not suggesting that this means that all Axiom code should be written in this manner since clearly it is much less efficient in general, but there are certainly cases where dynamic typing is much more convenient. Therefore I think we need to document and extend the domain Any in a manner consistent with the use of DuckTyping in other modern programming languages. From kratt6 Mon Apr 9 15:24:45 -0500 2007 From: kratt6 Date: Mon, 09 Apr 2007 15:24:45 -0500 Subject: then fix 'ANY1' Message-ID: <20070409152445-0500@wiki.axiom-developer.org> I used "hack" in the sense of "trick". I.e., it is neither pejorative, nor it's opposite. I believe that dependent types should be used instead of 'ANY'. I fail to understand DuckTyping however. Wikipedia says: "a file-like object can implement only methods it is able to, and consequently it can be only used in situations where it makes sense." What does this have to do with 'ANY'? Apart from that, I did not propose to ban 'ANY'. Only, I would very much like to have 'ANY1' accept only 'SetCategory' instead of 'Type'. This would make 'ANY' "type-safe".
The Boolean test for equality in the domain Any fails for structured objects, e.g. of type List:
)set message any off
showTypeInOutput true;
a:Any:=[1,2]
![]() | (1) |
b:Any:=[1,2]
![]() | (2) |
a=b
![]() | (3) |
test %
![]() | (4) |
The problem seems to be the use of Lisp EQ instead of EQUAL in the domain Any.
++ Author: Robert S. Sutor ++ Date Created: ++ Change History: ++ Basic Functions: any,domainOf, objectOf, dom, obj, showTypeInOutput ++ Related Constructors: AnyFunctions1 ++ Also See: None ++ AMS Classification: ++ Keywords: ++ Description: ++ \spadtype{Any} implements a type that packages up objects and their ++ types in objects of \spadtype{Any}. Roughly speaking that means ++ that if \spad{s : S} then when converted to \spadtype{Any}, the new ++ object will include both the original object and its type. This is ++ a way of converting arbitrary objects into a single type without ++ losing any of the original information. Any object can be converted ++ to one of \spadtype{Any}.
Any(): SetCategory with any : (SExpression,None) -> % ++ any(type, object) is a technical function for creating ++ an object of \spadtype{Any}. Arugment \spad{type} is a \spadgloss{LISP} form ++ for the type of \spad{object}. domainOf : % -> OutputForm ++ domainOf(a) returns a printable form of the type of the ++ original object that was converted to \spadtype{Any}. objectOf : % -> OutputForm ++ objectOf(a) returns a printable form of the ++ original object that was converted to \spadtype{Any}. dom : % -> SExpression ++ dom(a) returns a \spadgloss{LISP} form of the type of the ++ original object that was converted to \spadtype{Any}. obj : % -> None ++ obj(a) essentially returns the original object that was ++ converted to \spadtype{Any} except that the type is forced ++ to be \spadtype{None}. showTypeInOutput: Boolean -> String ++ showTypeInOutput(bool) affects the way objects of ++ \spadtype{Any} are displayed. If \spad{bool} is true ++ then the type of the original object that was converted ++ to \spadtype{Any} will be printed. If \spad{bool} is ++ false, it will not be printed.
== add Rep := Record(dm: SExpression,ob: None)
printTypeInOutputP:Reference(Boolean) := ref false
obj x == x.ob dom x == x.dm domainOf x == x.dm pretend OutputForm x = y == (x.dm = y.dm) and EQUAL(x.ob,y.ob)$Lisp
objectOf(x : %) : OutputForm == spad2BootCoerce(x.ob,x.dm, list("OutputForm"::Symbol)$List(Symbol))$Lisp
showTypeInOutput(b : Boolean) : String == printTypeInOutputP := ref b b=> "Type of object will be displayed in output of a member of Any" "Type of object will not be displayed in output of a member of Any"
coerce(x):OutputForm == obj1 : OutputForm := objectOf x not deref printTypeInOutputP => obj1 dom1 := p:Symbol := prefix2String(devaluate(x.dm)$Lisp)$Lisp atom?(p pretend SExpression) => list(p)$List(Symbol) list(p)$Symbol hconcat cons(obj1,cons(":"::OutputForm, [a::OutputForm for a in dom1]))
any(domain,object) == (isValidType(domain)$Lisp)@Boolean => [domain, object] domain := devaluate(domain)$Lisp (isValidType(domain)$Lisp)@Boolean => [domain, object] error "function any must have a domain as first argument"
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7328750709169231775-25px003.spad using old system compiler. ------------------------------------------------------------------------ initializing NRLIB ANY for Any compiling into NRLIB ANY compiling exported obj : $ -> None ANY;obj;$N;1 is replaced by QCDR
;;; *** |ANY;obj;$N;1| REDEFINED Time: 0.01 SEC.
compiling exported dom : $ -> SExpression ANY;dom;$Se;2 is replaced by QCAR
;;; *** |ANY;dom;$Se;2| REDEFINED Time: 0 SEC.
compiling exported domainOf : $ -> OutputForm ANY;domainOf;$Of;3 is replaced by QCAR
;;; *** |ANY;domainOf;$Of;3| REDEFINED Time: 0 SEC.
compiling exported = : ($,$) -> Boolean
;;; *** |ANY;=;2$B;4| REDEFINED Time: 0 SEC.
compiling exported objectOf : $ -> OutputForm
;;; *** |ANY;objectOf;$Of;5| REDEFINED Time: 0.01 SEC.
compiling exported showTypeInOutput : Boolean -> String
;;; *** |ANY;showTypeInOutput;BS;6| REDEFINED Time: 0 SEC.
compiling exported coerce : $ -> OutputForm
;;; *** |ANY;coerce;$Of;7| REDEFINED Time: 0 SEC.
compiling exported any : (SExpression,None) -> $
;;; *** |ANY;any;SeN$;8| REDEFINED Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |Any| REDEFINED
;;; *** |Any| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor Any Time: 0.02 seconds
finalizing NRLIB ANY Processing Any for Browser database: --------constructor--------- --------(any (% (SExpression) (None)))--------- --------(domainOf ((OutputForm) %))--------- --------(objectOf ((OutputForm) %))--------- --------(dom ((SExpression) %))--------- --------(obj ((None) %))--------- --------(showTypeInOutput ((String) (Boolean)))--------- ; compiling file "/var/aw/var/LatexWiki/ANY.NRLIB/ANY.lsp" (written 18 JUL 2013 09:16:36 PM):
; /var/aw/var/LatexWiki/ANY.NRLIB/ANY.fasl written ; compilation finished in 0:00:00.032 ------------------------------------------------------------------------ Any is now explicitly exposed in frame initial Any will be automatically loaded when needed from /var/aw/var/LatexWiki/ANY.NRLIB/ANY
Re-test
)set message any off
showTypeInOutput true;
a:Any:=[1,2]
![]() | (5) |
b:Any:=[1,2]
![]() | (6) |
a=b
![]() | (7) |
test %
![]() | (8) |
See also SandBoxSetAny
ANY
is completely broken. One would really need to call the appropriate =
from the domain, but I don't think that this is possible in Axiom:
p: Set ANY := set [1,2];
q: Set ANY := set [2,1];
test(p=q)
![]() | (9) |
test(p::ANY=q::ANY)
![]() | (10) |
If the domain has canonical
, the test using EQUAL
might work...
test((3/4)::ANY = (3/4)::ANY)
![]() | (11) |
Martin
Maybe the following definition works, at least, it seems to. Note that we should ask forBasicType
, because otherwise equality is not even defined.
I'm not sure how the correspondence SEX
and Type ought to work...
I guess what you are not sure about is the reasonableness of:
D := (x.dm pretend BasicType)
as a way to turn a member of the domain (SExpression?) into a Type given that the representation of x is:
Record(dm: SExpression, ob: None)
Of course the "normal" use of pretend is to treat a member of one domain "as if" it was a member of another domain but in this case you are treating a member of a domain as if it was a member of a category, i.e. a domain. That is very cool!
I think your code ok since as I near as I can understand after some emails exchanged with Peter Broadbery #209 and in spite of nearly no documentation in interop.boot.pamphlet the Boot function:
devaluate(domain)$Lisp
ensures that the domain will be representable as an Axiom SExpression?.
So, ifD := (x.dm pretend BasicType)
is OK, we should go further, and work a little on ANY
. At least, it should throw an error if x.dm
is not a BasicType
.
In fact, I doubt, that ANY
should export equality at all. Is this functionality used anywhere? Similarly, should ANY
support coercion to OUTFORM
for any object?
Martin
I don't understand your question. The domain ANY already supports coercion to OUTFORM. We are using it in the examples on this page.You wrote:
In fact, I doubt, that ANY should export equality at all. Is this functionality used anywhere?
Yes, for example in the domain Set(Any).
Are you familiar with the functions defined in the ANY1 package?
See also the page: DuckTyping?
I see the situation as follows: an object inANY
may currently be of any Type
. However, ANY
has SetCategory
, i.e., it supports coercion to OutputForm
and equality. Thus, via ANY
, any domain becomes of type SetCategory
, which is something I do not like.
As far as I can see, the only way apart from pretend
to create an object of type ANY
is via coerce$ANY1
. So, I'd suggest that we modify ANY1
to accept only arguments that have SetCategory
. If we want to support things that do not have equality, for example, we should create another domain, similar to ANY
, that only has KOERCE OUTFORM
, but I doubt that this is useful.
In any case, I like the Object
implementation in the Aldor Compiler User Guide much better.
Martin
http://www.aldor.org/docs/HTML/chap26.html#24Does not seem to give much information about Object except:
Description: 'Object(C)' implements dynamic objects, pairing data values with associated domains.
and that it exports two functions:
object : (T: C, T) -> % 'object(T, t)', where the type of `t' is `T', creates on object of the domain. avail : % -> (T: C, T)
Can you say more about this domain and why you "like it much better"?
The difference betweenObject
and Any
is that the former stays much more in line with the strict typing philosophy. I believe that Any
was rather a hack to put up with the lack of dependent types as needed for the series
operations.
The idea behind Object
is to wrap up an object together with its type. Thus, the operation object
corresponds to coerce$ANY1
, and avail
is roughly dom
and obj
followed by retract$ANY1(dom)
, except that the latter won't work... I'd say that Object
is rarely needed in Aldor.
I guess, one cannot easily write Object
using SPAD, because of the lack of dependent types. I was probably too quick to say that I like Object
much better. I should have said: I like dependent types much better...
Therefore I think we need to document and extend the domain Any in a manner consistent with the use of DuckTyping? in other modern programming languages.
I used "hack" in the sense of "trick". I.e., it is neither pejorative, nor it's opposite. I believe that dependent types should be used instead ofANY
. I fail to understand DuckTyping? however. Wikipedia says:
"a file-like object can implement only methods it is able to, and consequently it can be only used in situations where it makes sense."
What does this have to do with ANY
?
Apart from that, I did not propose to ban ANY
. Only, I would very much like to have ANY1
accept only SetCategory
instead of Type
. This would make ANY
"type-safe".