login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Submitted by : (unknown) at: 2007-11-17T22:31:07-08:00 (16 years ago)
Name :
Axiom Version :
Category : Severity : Status :
Optional subject :  
Optional comment :

The Boolean test for equality in the domain Any fails for structured objects, e.g. of type List:

fricas
(1) -> )set message any off
showTypeInOutput true;
Type: String

fricas
a:Any:=[1,2]

\label{eq1}{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })(1)
Type: Any
fricas
b:Any:=[1,2]

\label{eq2}{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })(2)
Type: Any
fricas
a=b

\label{eq3}{{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })}={{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })}(3)
Type: Equation(Any)
fricas
test %

\label{eq4} \mbox{\rm true} (4)
Type: Boolean

Proposed Fix

The problem seems to be the use of Lisp EQ instead of EQUAL in the domain Any.

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"
spad
   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 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 SEC.
compiling exported showTypeInOutput : Boolean -> String
;;; *** |ANY;showTypeInOutput;BS;6| REDEFINED Time: 0 SEC.
compiling exported coerce : % -> OutputForm ****** comp fails at level 6 with expression: ****** error in function coerce
(SEQ (|:=| (|:| |obj1| (|OutputForm|)) (|objectOf| |x|)) (SEQ (|:=| (|:| #1=#:G5 (|Boolean|)) (|deref| |printTypeInOutputP|)) (|exit| 1 (IF #1# |noBranch| (|exit| 2 |obj1|)))) (|:=| |dom1| (SEQ (|:=| (|:| |p| (|Symbol|)) ((|Sel| |Lisp| |prefix2String|) ((|Sel| |Lisp| |devaluate|) (|x| |dm|)))) (|:=| (|:| #2=#:G6 (|Boolean|)) (|atom?| (|pretend| |p| (|SExpression|)))) (|exit| 1 (IF #2# ((|Sel| (|List| (|Symbol|)) |list|) |p|) | << | ((|Sel| (|Symbol|) |list|) |p|) | >> |)))) (|exit| 1 (|hconcat| (|cons| |obj1| (|cons| (|::| ":" (|OutputForm|)) (COLLECT (IN |a| |dom1|) (|::| |a| (|OutputForm|)))))))) ****** level 6 ****** $x:= ((Sel (Symbol) list) p) $m:= (List (Symbol)) $f:= ((((#:G6 # #) (|p| # #) (#:G5 # #) (|obj1| # #) ...)))
>> Apparent user error: NoValueMode is an unknown mode

Re-test

fricas
)set message any off
showTypeInOutput true;
Type: String

fricas
a:Any:=[1,2]

\label{eq5}{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })(5)
Type: Any
fricas
b:Any:=[1,2]

\label{eq6}{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })(6)
Type: Any
fricas
a=b

\label{eq7}{{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })}={{\left[ 1, \: 2 \right]}: \hbox{\axiomType{List}\ } (\hbox{\axiomType{PositiveInteger}\ })}(7)
Type: Equation(Any)
fricas
test %

\label{eq8} \mbox{\rm true} (8)
Type: Boolean

See also SandBoxSetAny

domain Any --billpage, Thu, 05 Apr 2007 11:38:24 -0500 reply
Category: Aldor Library Compiler => Axiom Library Status: open => fix proposed

works only if canonical --kratt6, Thu, 05 Apr 2007 16:15:06 -0500 reply
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:
fricas
p: Set ANY := set [1,2];
Type: Set(Any)
fricas
q: Set ANY := set [2,1];
Type: Set(Any)
fricas
test(p=q)

\label{eq9} \mbox{\rm true} (9)
Type: Boolean
fricas
test(p::ANY=q::ANY)

\label{eq10} \mbox{\rm true} (10)
Type: Boolean

If the domain has canonical, the test using EQUAL might work...

fricas
test((3/4)::ANY = (3/4)::ANY)

\label{eq11} \mbox{\rm true} (11)
Type: Boolean

Martin

Better definition --kratt6, Thu, 05 Apr 2007 16:54:17 -0500 reply
Maybe the following definition works, at least, it seems to. Note that we should ask for BasicType, because otherwise equality is not even defined.


     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

I'm not sure how the correspondence SEX and Type ought to work...

Excellent! --Bill Page, Thu, 05 Apr 2007 23:45:34 -0500 reply
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 the Boot function:

   devaluate(domain)$Lisp

ensures that the domain will be representable as an Axiom SExpression?.

going further --kratt6, Fri, 06 Apr 2007 00:36:48 -0500 reply
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

Re: coercion to OUTFORM --billpage, Sat, 07 Apr 2007 01:17:17 -0500 reply
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?

being more precise --kratt6, Sat, 07 Apr 2007 02:56:26 -0500 reply
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

Re: Object domain in Aldor --billpage, Sun, 08 Apr 2007 00:35:12 -0500 reply
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"?

Aldor Object --kratt6, Mon, 09 Apr 2007 14:16:49 -0500 reply
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...

Re: Any is a hack? --Bill Page, Mon, 09 Apr 2007 14:36:32 -0500 reply
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.

then fix ANY1 --kratt6, Mon, 09 Apr 2007 15:24:45 -0500 reply
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".




  Subject: (replying)   Be Bold !!
  ( 15 subscribers )  
Please rate this page: