"Bill Page" <[EMAIL PROTECTED]> writes:
| On Thu, May 22, 2008 at 10:37 AM, Gabriel Dos Reis wrote:
| > Bill Page writes:
| >
| > | On Thu, May 22, 2008 at 9:39 AM, Gabriel Dos Reis wrote:
| > | > Bill Page writes:
| > | > ...
| > | > |
| > | > | 3) Can I use Tuple in a similar manner when calling a function?
| > | ...
| > | Please consider this a feature request. :-)
| >
| > We need a thorough analysis, otherwise we don't have a guarantee
| > that we have something sensible.
| >
| > Currently we don't have overloaded functions in the interpreter, but
| > that is a deficiency. Now, assume we are in a world where functions
| > can be overloaded in sciprs, and consider
| >
| > t: Tuple INT -> INT -- #1
| > t: (INT, INT) -> INT -- #2
| >
| > and the calls
| >
| > t (3) -- calls?
| > t (3,2) -- calls?
| > t (3,2,1) -- calls?
| >
| > I want a mechanism that yields a reliable call resolution, in the
| > `improved world'.
| >
|
| Yes, I see the problem. 't(3,2)' is ambiguous. It satisfies the
| signature of more than one function in this context. There are a few
| other situations where this can occur. I think that in this case the
| compiler (and the interpreter) could simply return an error message.
Yes, that is one possibility. One thing about catching ambiguities is that
one should also give programmers means to resolve them -- for example,
Spad has the notion of `package call' for ambiguous call, or `target
type restriction' for overloaded constants.
For the case of tuple, I suspect that people will consistently use the
unambiguous tuple notation so as to avoid that an unexpected
declaration hijacks their calls.
[...]
| > ...
| > | By "type name for 'x: T' " do you mean that 'x:T' would have a
| > | different type from 'T'?
| >
| > Yes. As far as I can tell, Record(gcd: Integer, lcm: Integer) is
| > very different from Record(foo: Integer, bar: Integer) -- think use of
| > those types in function types. The names of the fields are part of
| > the type.
|
| Ok. In fact I would like these names to be exported by the type. So
| the type of 'x:T' would be just 'Record(x:T)' which would export
|
| x: % -> T
|
| But notice that 'Union(x:T)' exports
|
| x: T -> %
|
I'm not convinced that I want the type of 'x:T' to be synonymous to
'Record(x:T)'.
Note that however this issue is resolved, it is not completely
independent of dependent types (no pun intended). For example, I
don't want
f: (n: NonNegativeInteger) -> DataBuffer n
be different from
f: (m: NonNegativeInteger) -> DataBuffer m
They declare the same function. On the other hand I really want
h: Record(gcd: Integer) -> Vector Integer
be different from
h: Record(foo: Integer) -> Vector Integer
| >
| > | I am not convinced that type is the right abstraction for the
| > difference between these expressions.
| >
| > Could you elaborate?
| >
|
| After thinking about it, I guess I have convinced myself that you are
| right. I was thinking about the way this is described in the Aldor
| documentation and I did not like that at all. But if 'x:T' is just
| 'Record(x:T)', then it seems ok to me. For example, if I define:
I don't like the Aldor description either. That is part of the
reasons why this has been lingering. I'm looking for good, simple,
alternatives that I can formally explain (preferably from a type
theoretic point of view).
[...]
| > | I don't understand. As far as I can see in the definition
| > |
| > | UnionDom(arg:Union(sym: Symbol, str:String, int: Integer)) ...
| > |
| > | arg has a specific type, thus 'UnionDom' is not overloaded in the same
| > | sense that the
| > |
| > | UnionDom(arg:Symbol) ...
| > | UnionDom(arg:String) ...
| > | UnionDom(arg:Integer) ...
| > |
| > | is an overloaded definition for 'UnionDom'.
| >
| > The overloading is between
| >
| > Union(Integer,String) -- union with unnamed fields,
| >
| > versus
| >
| > Union(f: Integer, g: String) -- union with named fields.
| >
| > They generate different operations and use different codes internally
| > in the compiler.
| >
|
| It seems to me that these can and should be implemented by essentially
| the same code.
In a world where 'f: Integer' is a type, I think the issue evaporates.
But, we're not in that world yet, and getting there is not easy and
sometimes does not seem natural -- even you expressed being uneasy
with Aldor's description. For many, it just sounds `weird', yet I
believe it makes sense; we just need to get used to it :-)
|
| 'Union(Integer,String)' is currently broken since it exports
|
| coerce: Integer -> %
| coerce: String -> %
|
| which doesn't make sense if the component types are the same.
That is explicitly documented in the Axiom Book as not supported :-)
| Similarly the construction
|
| x case Integer
|
| could be ambiguous.
|
| There is a need for some syntax to designate otherwise unnamed tags.
| Suppose we use '%1', '%2', ... for such names. Then
Numbers are easy because there is an infinite supply of them :-). I'm
not good at numbers -- my machines are. So, before I fall back to
that solution I would like to look other alternatives.
| 'Union(Integer,String)' could export:
|
| %1: Integer -> %
| %2: String -> %
|
| and we would write
|
| x case %1 => ...
This is essentially the solution adopted by Aldor.
[...]
| > | > You did not ask for Mapping, but one should be able to have it
| > | > for Mapping -- in fact, it was working on something related to
| > | > Mapping (modemaps) that prompted me to add the capability.
| > | >
| > |
| > | Could you give an example of how this might be applied to
| > | Mapping?
| >
| > Well, conceptually Mapping has type Tuple Type -> Type, and
| > follows exactly the calling convention implemented by the patch.
| >
|
| Ok, yes. 'Mapping' as a built-in type constructor is currently displayed as:
|
| Mapping(T:Type, S:Type, R:Type, ...): (S, R, ... ) -> T
|
| but of we cannot actually write and compile definitions like this. I
Yes.
| guess you are suggesting that we think of this as:
|
| Mapping(T:Type, S:Tuple Type): S -> T
|
| Of course we might also would like to be able to write:
|
| Mapping(T:Tuple Type, S:Tuple Type)
Almost. That was my initial thinking, naturally. However, I backed off
and implemented a very simply minded solution: Mapping could just be
defined as:
Mapping(ResultAndArgTypes: Tuple Type): Type ==
bundling together both the result type and the arg types. The first
type, if any, will always be intepreted as the result type. Notice
this does not exclude having Tuple as result type. For example, one
could write
Mapping((INT,INT), FLOAT, STRING)
which is another notation for
(FLOAT, STRING) -> (INT,INT)
|
| i.e. for the type of functions that return a tuple of values:
|
| f: (S,R,...) -> (T,U, ...)
|
| There is no need for Mapping to be defined with more than two arguments.
Yes.
One could also make sense of Mapping ().
-- Gaby
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
