[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Question concerning types...
From: 
Ralf Hemmecke 
Subject: 
Re: [Axiomdeveloper] Question concerning types... 
Date: 
Sun, 17 Sep 2006 19:58:52 +0200 
Useragent: 
Thunderbird 1.5.0.5 (X11/20060719) 
On 09/17/2006 04:25 PM, Gabriel Dos Reis wrote:
Ralf Hemmecke <address@hidden> writes:
 >  > Intuitively I would expect Variable to mean simply "an
 >  > unspecified specific instance of a Domain/Type/what have you"
 >  > with ALL domains being possible  just so long as you specify
 >  > the type of the variable, e.g.:
 >  >  > a1 : Variable(Matrix Quaternion Fraction Integer)
 >  >   Suppose there was such a domain constructor named
 > Variable(D: domain)
 >  which had the properties you suggest. What operations would you expect
 >  this domain to export? Would it have the same operations as D? For
 >  example '+'. Given two objects from the domain Variable(Integer),
 >  say 'x' and 'y', what is the type of the result of 'x+y'? Is it
 >  still in Variable(Integer)?
 > FreeMonoid Variable Integer

 Gaby, do you really believe that? But in order to say x+y you have to
 have the type of Variable(D: domain) in the first place.
yes. My working assumption is that if we had Variable(D: domain) to
mean anything, it would be such that operations of D would be *lifted*
to Variable(D: domain) and would work as if we had an algebra (in the
Universal Algebra sense). In this case "+" would be lifted to
Variable Integer, so that x + y can be interpreted as an element a a
free monoid generated symbols. That is not rocket science.
I agree with you that if D had type T then Variable(D) should have type
T (plus maybe some exports that allow to create "indeterminates").
Looking at it mathematically (and simplified) then all we do is that we
take a universal algebra D = (A, F) where A is the carrier set and F are
the functions on it. Variable(D) is maybe a bad name, but all we do is
that Variable(D) = (A', F') is a universal algebra where A' is the union
of the set A, a set X of indeterminates, and all things that can be
generated from A and X by applying functions from F'. F and F' behave
identically on A.
Mathematically, that's not a big deal. But Aldor domains are actually
multisorted algebras. That makes the situation a little more complicated.
So I still disagree with you that x+y should be of type
FreeMonoid(Variable(Integer)). From what I said above, it seems more
natural to me that its type is Variable(Integer) (well, it's a bad name,
maybe Indefinite(Integer) would be better).
Anyway, what we want is a nice way of adding elements and more or less
keeping the type of the domain. And that is not possible if you just
define "Indefinite" having one argument D. One must know the type of D
(a category) so that the return type would be clear.
Indefinite(C: Catagory)(D: C): C == add {
Rep == Union(d: D, ???)
...
}
The ??? should be something that allows arbitrary expressions formed
from D, the functions in C and some indeterminates X. (I have no idea
how that would look like. Maybe just delayed evaluation of function
composition.)
[...]
 (1) > (a1,a2,a3,a4):Expression Quaternion Fraction Integer
 Type: Void
 (2) > m := matrix[[a1,a2],[a3,a4]]

 +a1 a2+
 (2)  
 +a3 a4+
 Type: Matrix Expression Quaternion Fraction Integer

 given by Bill suggest that the Axiom interpreter is a bit more relaxed.
Funny enough, I tried similar thing and sent a message before seeing
Bill's. That is a natural thing to do if you have a Universal Algebra
backgroud  e.g. you're used to the 3M's.
Maybe. I don't say that shouldn't be allowed in the interpreter, but the
compiler would generate a matrix of 4 uninitialized entries. Now what
happens if you print m(1,1)? If that prints something reasonable then it
tells me that the compiler knows about a special domain constructor,
namely Expression. Drop "Expression" from above, what would be on screen
for "stdout << m(1,1)"? The interpreter can add smart things. I am
asking for the compiler.
[...]
 I guess the interpreter has to do a lot of
 work to find the right interpretation for such a + and it must decide
 for one of possibly many choices.
If "+" is defined as beeing an associative operation , there would not
be much work to do.
Oh, who said that + is associative? The documentation, right? But that
is not a nice thing to take into account for the compiler. It would be
much better if Aldor allowed to state associativity in a formal manner.
In fact I don't want the interpret to become
super smart. Just lift operations.
I am completely with you. The interpreter should not have any
mathematical knowledge, just look into a database (basically the Axiom
libraries) and figure out what could be done. It should be possible to
change the libraries and work with the same interpreter.
 But assume I say x+z for
 z: Variable(Float) := "z"
 what is the type of that?
It is the type of its declaration: Variable(Float).
Oh, I meant the type of "x+z".
 Should the interpreter forbid such an
 addition?
there is no addition as far as I can see.
But there was also no addition until you transformed Variable(Integer)
into FreeMonoid Variable Integer.
 In the compiler I clearly don't want any guessing and not
 automatic conversion. Note that I prefer that (most of) the things
 that are possible in the interpreter could be compiled into stand
 alone programs.
 Anyway, if the type tower is always expanded like that you end up
 with the fact that
 (x+y)*x and x*x + x*y
 have types
 FreeMultiplicativeSemigroup FreeAdditiveSemigroup Variable Integer
 and
 FreeAdditiveSemigroup FreeMultiplicativeSemigroup Variable Integer
 and thus are not equal.
I don't see why.
OK, let's turn this into a mathematical example.
A := Fraction Complex Integer; a: A := 1
B := Complex Fraction Integer; b: B := 1
Clearly A and be are isomorphic as fields, but they are NOT identical.
Not identical in Axiom and not identical in mathematics.
Note, we had a discussion whether "Fraction Fraction Integer" should be
implemented to be the same as "Fraction Integer". Although I had even
given code to do that, I believe it should not be implemented that way.
Because an element that looks like (2/1)/(3/1) is NOT identical to 2/3.
(Just consider fractions as equivalence classes of pairs of some type.
Ralf
 Re: [Axiomdeveloper] Question concerning types..., (continued)
 Re: [Axiomdeveloper] Question concerning types..., C Y, 2006/09/16
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Martin Rubey, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Vanuxem GrĂ©gory, 2006/09/16
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/16
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types...,
Ralf Hemmecke <=
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18
 [Axiomdeveloper] equal or unequal (was: Question concerning types...), Ralf Hemmecke, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal (was: Question concerning types...), Gabriel Dos Reis, 2006/09/18
 [Axiomdeveloper] Re: equal or unequal, Ralf Hemmecke, 2006/09/18
 RE: [Axiomdeveloper] Question concerning types..., Bill Page, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types..., Ralf Hemmecke, 2006/09/18