[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Axiom-developer] "has" and "with" and bug
From: |
Ralf Hemmecke |
Subject: |
[Axiom-developer] "has" and "with" and bug |
Date: |
Mon, 13 Aug 2007 13:36:53 +0200 |
User-agent: |
Thunderbird 2.0.0.6 (X11/20070728) |
I'm saying that the parameter S of the default package
Monad& -- generated for the default implementation of the
category Monad -- is of the named category Monad.
Sorry, I am too lazy to go back where all began. But let me quote that
piece of code here.
Monad(): Category == SetCategory with
"*": (%,%) -> %
"**": (%,PositiveInteger) -> %
...
add
import RepeatedSquaring(%)
x:% ** n:PositiveInteger == expt(x,n)
...
RepeatedSquaring(S): Exports == Implementation where
S: SetCategory with "*":(%,%)->%
Exports == with
expt: (S,PositiveInteger) -> S
Implementation == add ...
First. % in RepeatedSquaring(%) can in general not be Monad.
Why? One should be able to pass the "add" part alone as an anonymous
domain to a function.
AUG Chp. 8.10:
An add expression also introduces a binding for the constant %, which
is a reference to the domain formed by the add expression.
So let's do something in Aldor. "add" has to be replaced by "default",
but this way it does not demonstrate what I wanted to show.
Let's compile and run the program below.
woodpecker:~/scratch>aldor -laldor -grun aaa.as
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
MDom has rhx? T
Ooops. I must say that is surprising. MDom exports foo, bar, ans, but
not rhx.
So my preferred output would have been:
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = F
MDom has rhx? F
blahrhx()$Blah(%) should give T, because (I believe) the whole add part
is passed to Blah and that is an anonymous domain with exports
(*)
foo: ()->()
bar: ()->()
rhx: ()->()
ans: (...)->()
AUG Chp. 7.8:
The type of the expression A add B is C with { x1: T1; ...; xn: Tn }
where C is the type of A, and x1,...,xn are the symbols defined
(using ==) in B, whose types are T1,...,Tn, respectively.
So that is another place where the Aldor compiler does not behave
according to specification.
Also try to copy the add part of MDom and pass it as an anonymous domain
argument to ans$MDom. That does not compile, since for some reason the
compiler thinks that the type of that "add {...}" thing is Type instead
of the category with exports given in (*).
In general, (as Bill already pointed out), "has" tests for "subcategory".
As a function "has" is of type
has: (Type, Category) -> Boolean
where the first argument is actually restricted to domains/packages.
See AUG.pdf page 96 "Has expressions".
In Aldor you cannot say
Monoid has with {1: %}
since Monoid is of type Category (though also of type Type).
----------------------------------------------------------------------
aldor -gloop
%1 >> #include "aldor"
%2 >> #include "aldorinterp"
%3 >> PrimitiveType
() @ Category == with
=: (%, %) -> Boolean
~=: (%, %) -> Boolean
default ((a: %) ~= (b: %)): Boolean == ..
Comp: 0 msec, Interp: 0 msec
%4 >> PrimitiveType has with {=:(%,%)->Boolean}
^
[L14 C1] #1 (Error) No meaning for identifier `PrimitiveType'.
%5 >> #quit
-----------------------------------------------------------------------------
Gaby, if you implement those stuff in SPAD, please don't apply some
automatic coercion. This whole stuff is about type satisfaction.
I am sure you know about AUG.pdf Chp. 7.5 "Subtypes", Chp. 7.7 "Type
satisfaction".
All the best
Ralf
---BEGIN aaa.as
#include "aldor"
#include "aldorio"
Blah(S: with {foo:()->()}): with {
blahfoo: ()->Boolean;
blahbar: ()->Boolean;
blahrhx: ()->Boolean;
} == add {
blahfoo(): Boolean == S has with {foo: ()->()};
blahbar(): Boolean == S has with {bar: ()->()};
blahrhx(): Boolean == S has with {rhx: ()->()};
}
MMM: Category == with {
foo: () -> ();
bar: () -> ();
}
MDom: MMM with {
ans: (with {foo:()->(); bar:()->()}) -> ();
} == add {
foo(): () == {
stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(%) << newline;
stdout << "has with {bar: ()->()} = " << blahbar()$Blah(%) << newline;
stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(%) << newline;
}
bar(): () == {}
rhx(): () == {}
ans(S: with {foo:()->(); bar: ()->()}): () == {
stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(S) << newline;
stdout << "has with {bar: ()->()} = " << blahbar()$Blah(S) << newline;
stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(S) << newline;
}
}
main(): () == {
foo()$MDom;
ans(MDom)$MDom;
stdout << "MDom has rhx? " << (MDom has with {rhx: ()->()}) << newline;
}
main();
---END aaa.as
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), (continued)
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/12
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- [Axiom-developer] "has" and "with" and bug,
Ralf Hemmecke <=
- Re: [Axiom-developer] "has" and "with" and bug, William Sit, 2007/08/13
- Re: [Axiom-developer] "has" and "with" and bug, Ralf Hemmecke, 2007/08/13
- [Axiom-developer] Re: "has" and "with" and bug, Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16