[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 16:25:26 +0200 
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.
[...]
 (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.
[...]
 2)
 Now Gaby said that x+y should have type FreeMonoid Variable
 Integer. Why not FreeGroup?
I picked FreeMonoid because that is the least assumption with "+" from
Integer. But I'm OK to have the interpereter go directly to FreeGroup
 that would be even more consistent with my earlier suggestion of
lifting operations to Variable D.
 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. In fact I don't want the interpret to become
super smart. Just lift operations.
 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).
 Should the interpreter forbid such an
 addition?
there is no addition as far as I can see.
 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.
 And what would be the type of foo?(x,y)? Maybe I have extended Integer
 to contain a function foo: (%, %) > Boolean.
Yes, what is the resulting Algrbraci structrure?
 Variable(Integer) does
 however not export anything about its argument.
it does not have to.
 So who is going to find out that such a foo exists?
The process would be that of lifting operations from D to Variable(D).
Notice, this isn't a problem for programming languages. Think about
it from Universal Algebra perspective.
 Gaby
 Re: [Axiomdeveloper] Question concerning types..., (continued)
 Re: [Axiomdeveloper] Question concerning types..., Gabriel Dos Reis, 2006/09/16
 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 <=
 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/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