[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] Question concerning types...
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] Question concerning types... 
Date: 
17 Sep 2006 21:18:59 +0200 
Ralf Hemmecke <address@hidden> writes:
[...]
 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.
yes.
 Mathematically, that's not a big deal. But Aldor domains are actually
 multisorted algebras. That makes the situation a little more
 complicated.
but not impossible.
In this discussion, I'm going to ignore Aldor for a moment and
concentrate on SPAD because I don't have access to Aldor source code
and anything that might transpire out of this discoussion should
probably be recorded as a featurerequest for SPAD with all the
"insights" we might have gained.
 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).
I don't think it should be Variable(Integer). For me,
Variable(Integer) means a symbol who interpretation is of type
Integer. I don't like Indefinite(Integer) neither. So, it might very
well be that we're back to our old beloved friend Expression(Integer).
 Anyway, what we want is a nice way of adding elements and more or less
 keeping the type of the domain.
yes.
 And that is not possible if you just define "Indefinite" having one
 argument D.
I'm clear why not. Could you explain this a bit further?
 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.)
I suspect I'm being dense here. What would be wrong with Expression D?
 > [...]
 >  (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 entry is a Variable? I would expect the output to indicate
either the name or just m(1,1). Look at what Axiom prints when you
say
m * m
That matches my expectation.
 If that prints something reasonable
 then it tells me that the compiler knows about a special domain
 constructor, namely Expression.
yes.
 Drop "Expression" from above, what
 would be on screen for "stdout << m(1,1)"?
well, it Expression is dropped then we're back to the interpretation
we all agree on: A value of type Quaternion Fraction Integer.
Consequently m(1,1) must hold value of that type.
 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?
And
yes, but in my model much of the documentation is moved to code. In
this case, I would like to see properties() used to attach
mathematical properties.
 But that
 is not a nice thing to take into account for the compiler.
Why?
>From my point of view, the type of an operation is just as important
as its algebraic properties.
 It would be
 much better if Aldor allowed to state associativity in a formal manner.
SPAD does. See properties()
 > 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.
yes.
 >  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.
I did not transform a variable to FreeMonoid Variable Integer.
However, I did suggest that type for th _compound expression_ "x+y"
when the question was asked.
 >  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.
As syntactic obejcts, no, they are not. The issue can be rephrased as
whether they should remain nonequal in other nonsyntactical
intepretation. I think no.
 Not identical in Axiom and not identical in mathematics.
You have lost me on the last part. My book says that both A and B are
the same mathematical object. Why do you believe they are not?
 Note, we had a discussion whether "Fraction Fraction Integer" should
 be implemented to be the same as "Fraction Integer".
Under the mathematical interpretation they are the same. I believe
they should also be the same in Axiom  at least if you take
dependent types seriously.
 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.
By the same token we should prevent Axiom from simplifying 3+2 to 5.
 (Just consider fractions as equivalence classes of
 pairs of some type.
I don't follow.
 Gaby
 Re: [Axiomdeveloper] Question concerning types..., (continued)
 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, 2006/09/17
 Re: [Axiomdeveloper] Question concerning types...,
Gabriel Dos Reis <=
 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
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/18