help links subscribe changes refresh edit

	IssueTracker
#347 bug in map$Set ←	↑	→ #35 Aldor compiler won't build

#348 Equality in Any

Edit detail for #348 Equality in Any revision 1 of 1

	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:

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