this domain %
Bill Page
represents "this domain" (or self in some programming languages). So
we commonly write for example
with
f: (%,%) -> %
to indicate a function f which takes a pair of values in this domain
and returns a value in this same domain - whatever domain we happten
to be talking about in this context.
But what if we are interested in the domain as a functor? Suppose I
was writing an "endofunctor" domain constructor like 'Set' and I
wanted to treat constructions like 'Set Set R', i.e. sets of sets as
something special. E.g.
MySet:(T:SetCategory):SetCategory == with
join: MySet MySet T -> MySet T
...
I cannot really use MySet here because MySet is not defined yet and
the compiler complains. I cannot use % here like this:
join: % % T -> % T
because % refers to 'MySet(T)' for some domain T in SetCategory. But
MySet(T) is itself a domain in SetCategory so it does make sense to
iterate it. How can I do this?
I recall another related notation %% (perhaps only in Aldor?) what is
it used for?
Regards,
Bill Page.
Gabriel Dos Reis
| In a domain and in categories referenced in a domain the notation %
| represents "this domain" (or self in some programming languages). So
| we commonly write for example
|
| with
| f: (%,%) -> %
|
| to indicate a function f which takes a pair of values in this domain
| and returns a value in this same domain - whatever domain we happten
| to be talking about in this context.
|
| But what if we are interested in the domain as a functor?
I am having trouble understanding why you think using the domain functor
would be a problem.
| Suppose I
| was writing an "endofunctor" domain constructor like 'Set' and I
| wanted to treat constructions like 'Set Set R', i.e. sets of sets as
| something special. E.g.
|
| MySet:(T:SetCategory):SetCategory == with
| join: MySet MySet T -> MySet T
This would not compile in OpenAxiom because of syntax errors, etc.
I suspect the colon before the open parenthesis is a typo. I removed
it, but then I could not make sense of the rest. The return type
"SetCategory" indicates that MySet is intended to be a functor, however
the body, i.e. the right hand side of the '==' is a category expression
not a domain expression. The OpenAxiom compiler rejects the construct
for that reason. I tried a variation of what you wrote
)abbrev domain MYSET MySet
MySet(T:SetCategory): SetCategory with
join: MySet MySet T -> MySet T
== add
Rep == Void
join x == per void()
that compiles just fine.
Whether one can use it is a different issue: that is a co-inductive
definition without a witness of it being inhabited.
-- Gaby
Bill Page
On Mon, Nov 21, 2011 at 8:52 AM, you wrote:
> Bill Page <bill...@newsynthesis.org> writes:
> ...
> | Suppose I
> | was writing an "endofunctor" domain constructor like 'Set' and I
> | wanted to treat constructions like 'Set Set R', i.e. sets of sets as
> | something special. E.g.
> |
> | MySet:(T:SetCategory):SetCategory == with
> | join: MySet MySet T -> MySet T
>
> This would not compile in OpenAxiom because of syntax errors, etc.
>
> I suspect the colon before the open parenthesis is a typo. I removed
> it, but then I could not make sense of the rest. The return type
> "SetCategory" indicates that MySet is intended to be a functor, however
> the body, i.e. the right hand side of the '==' is a category expression
> not a domain expression. The OpenAxiom compiler rejects the construct
> for that reason.
Yes. I am sorry that my example was so sloppy and I appreciate your
effort to understood my intention. Thank you.
> I tried a variation of what you wrote
>
> )abbrev domain MYSET MySet
> MySet(T:SetCategory): SetCategory with
> join: MySet MySet T -> MySet T
> == add
> Rep == Void
> join x == per void()
>
> that compiles just fine.
>
Yes, thank you for giving this example. Maybe it is interesting that
this example does not compile in FriCAS.
> Whether one can use it is a different issue: that is a co-inductive
> definition without a witness of it being inhabited.
>
Here is some more realistic example code that does compile and run:
)abbrev domain MYSET MySet
MySet(T:SetCategory): SetAggregate(T) with
finiteAggregate
join: MySet % -> MySet T
== add
Rep == List T
--rep(x:%):Rep == x pretend Rep
--per(x:Rep):% == x pretend %
Rep2 := List List T
rep2(x:MySet(%)):Rep2 == x pretend Rep2
per2(x:Rep2):MySet(%) == x pretend MySet(%)
coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
x = y == rep(x) = rep(y)
construct(x) == per removeDuplicates(x)$Rep
parts(x:%):List T == rep x
join x == construct concat rep2 x
--
(1) -> m1:MySet(Integer) := construct([1,2,3])$MySet(Integer)
(1) {1,2,3}
Type: MySet Integer
(2) -> m2:MySet(Integer) := construct([4,5,6])$MySet(Integer)
(2) {4,5,6}
Type: MySet Integer
(3) -> m12:=construct([m1,m2])$MySet(MySet Integer)
(3) {{1,2,3},{4,5,6}}
Type: MySet MySet Integer
(4) -> join m12
(4) {1,2,3,4,5,6}
Type: MySet Integer
--
Could you elaborate a little on what you mean by:
"that is a co-inductive definition without a witness of it being inhabited"
Does this have something to do with the need to for a type coercion
such as 'rep2' above?
Regards,
Bill Page.
Bertfried Fauser
Your code (which I copied and pasted into monad2.spad):
> Here is some more realistic example code that does compile and run:
>
> )abbrev domain MYSET MySet
> MySet(T:SetCategory): SetAggregate(T) with
> finiteAggregate
> join: MySet % -> MySet T
> == add
> Rep == List T
> --rep(x:%):Rep == x pretend Rep
> --per(x:Rep):% == x pretend %
>
> Rep2 := List List T
> rep2(x:MySet(%)):Rep2 == x pretend Rep2
> per2(x:Rep2):MySet(%) == x pretend MySet(%)
>
> coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
> x = y == rep(x) = rep(y)
> construct(x) == per removeDuplicates(x)$Rep
> parts(x:%):List T == rep x
> join x == construct concat rep2 x
>
(1) -> )co monad2
Compiling FriCAS source code from file
/home/fauser/fricas/monad2.spad using old system compiler.
MYSET abbreviates domain MySet
------------------------------------------------------------------------
initializing NRLIB MYSET for MySet
compiling into NRLIB MYSET
compiling local rep2 : MySet $ -> Rep2
MYSET;rep2 is replaced by x
Time: 0.03 SEC.
compiling local per2 : Rep2 -> MySet $
MYSET;per2 is replaced by x
Time: 0 SEC.
compiling exported coerce : $ -> OutputForm
Internal Error
Error while instantiating type MySet$$
?
Cheers
BF.
--
% PD Dr Bertfried Fauser
% Research Fellow, School of Computer Science, Univ. of Birmingham
% Honorary Associate, University of Tasmania
% Privat Docent: University of Konstanz, Physics Dept
<http://www.uni-konstanz.de>
% contact |-> URL : http://www.cs.bham.ac.uk/~fauserb/
% Phone : +44-121-41-42795
Bill Page
In FriCAS you should make the following change (:= instead of == and
explicitly define rep and per):
Rep := List T
rep(x:%):Rep == x pretend Rep
per(x:Rep):% == x pretend %
But as I mentioned in my email to Gaby this code does not compile in
FriCAS. It does compile and run in OpenAxiom. I haven't tried with
old Axiom yet.
Here is another variant that works in OpenAxiom but still fails in
FriCAS where I have just replaced 'MySet %' with 'MySet MySet T'. As I
understand it, this is now syntactically equivalent in OpenAxiom. I am
not sure if this is the case in FriCAS.
)abbrev domain MYSET MySet
MySet(T:SetCategory): SetAggregate(T) with
finiteAggregate
join: MySet MySet T -> MySet T
== add
Rep == List T
--rep(x:%):Rep == x pretend Rep
--per(x:Rep):% == x pretend %
Rep2 := List List T
rep2(x:MySet MySet T):Rep2 == x pretend Rep2
per2(x:Rep2):MySet MySet T == x pretend MySet MySet T
coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
x = y == rep(x) = rep(y)
construct(x) == per removeDuplicates(x)$Rep
parts(x:%):List T == rep x
join x == construct concat rep2 x
--
Perhaps as you know the point of this exercise was to be able to write
'MySet MySet T' (or equivalent) in the definition of MySet itself.
There are still many functions missing in this definition. Of course
as a functor we also need the equivalent of fmap, etc. Then my goal
was to abstract the part of the definition involving join and return
as a Monad category.
Cheers,
Bill Page.
Bertfried Fauser
thank you for the explanation, I was not aware that this code is for
OpenAxiom (I have
only FriCAS installed currently, and as I am moving to a new computer
I will not add
anything on my old one)
> )abbrev domain MYSET MySet
> MySet(T:SetCategory): SetAggregate(T) with
> finiteAggregate
> join: MySet MySet T -> MySet T
> == add
> Rep == List T
Why are the next two lines commented out?
> --rep(x:%):Rep == x pretend Rep
> --per(x:Rep):% == x pretend %
>
> Rep2 := List List T
> rep2(x:MySet MySet T):Rep2 == x pretend Rep2
> per2(x:Rep2):MySet MySet T == x pretend MySet MySet T
>
> coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
> x = y == rep(x) = rep(y)
> construct(x) == per removeDuplicates(x)$Rep
> parts(x:%):List T == rep x
> join x == construct concat rep2 x
> Perhaps as you know the point of this exercise was to be able to write
> 'MySet MySet T' (or equivalent) in the definition of MySet itself.
Yes, I got that, and that was the reason why I tried to compile it.
To define a monad,
we need something which can operator on a (mathematical) category (say Set). Now
sets itself may be structured, eg a set of elements, or a set of sets
(take lists if you like).
So I wondered if one could have something like a `lazy type'. We want to have
on the _category_ Set (List if you like) an endofunctor T : Set -->
Set, which has as a codomain possibly a structured datatype (think of
the power set functor) hence a set of
sets (list of lists).
As the functor can be applied indefinitely often, we get data types
of the form Set(Set(...(Set)...)). Clearyl that is not a definable
instance in a CAS. So I would like to see something
as a type:
lazyType = Type + T( lazyType )
where the rhs is not evaluated (lazy). In terms of sets of elements of
some type foo, we have
foo, Set(foo), Set(Set(foo)), etc
The monad multiplication operation will not look into the deeper
nesting if always allied on the outer level (which is feasible due to
associativity). So if the type checking would just see that there is
at least on Set(bar) there, then the type of bar would not matter. I
had the feeling that your code wanted to do this just for three
levels:
I, List(I), List(List(I))
Bill Page
On Sat, Dec 3, 2011 at 11:27 AM, you wrote:
>
>> )abbrev domain MYSET MySet
>> MySet(T:SetCategory): SetAggregate(T) with
>> finiteAggregate
>> join: MySet MySet T -> MySet T
>> == add
>> Rep == List T
>
> Why are the next two lines commented out?
>
In OpenAxiom (like Aldor) rep and per are built-in. In FriCAS one must
define them explicitly. The uncommenting these lines is needed when
attempting to compile this with FriCAS.
>> --rep(x:%):Rep == x pretend Rep
>> --per(x:Rep):% == x pretend %
>>
>> Rep2 := List List T
>> rep2(x:MySet MySet T):Rep2 == x pretend Rep2
>> per2(x:Rep2):MySet MySet T == x pretend MySet MySet T
>>
>> coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
>> x = y == rep(x) = rep(y)
>> construct(x) == per removeDuplicates(x)$Rep
>> parts(x:%):List T == rep x
>> join x == construct concat rep2 x
>
>> Perhaps as you know the point of this exercise was to be able to write
>> 'MySet MySet T' (or equivalent) in the definition of MySet itself.
>
> Yes, I got that, and that was the reason why I tried to compile it.
I would like to write:
)abbrev category MONADC MonadCat
MonadCat(T:Type, M:T->T):Category == with
join: M M T -> M T
)abbrev domain MYSET MySet
MySet(T:SetCategory): MonadCat(T,MySet) with
finiteAggregate
== add
...
But this doesn't work even in OpenAxiom (yet).
> To define a monad,
> we need something which can operator on a (mathematical) category
> (say Set). Now sets itself may be structured, eg a set of elements,
> or a set of sets (take lists if you like).
Yes. As I currently understand that is what I intend by MonadCat above.
> So I wondered if one could have something like a `lazy type'. We want
> to have on the _category_ Set (List if you like) an endofunctor
> T : Set --> Set,
> which has as a codomain possibly a structured datatype (think
> of the power set functor) hence a set of sets (list of lists).
If I understand you correctly I think would could say that Axiom types
are always "lazy" in this sense.
> As the functor can be applied indefinitely often, we get data types
> of the form Set(Set(...(Set)...)). Clearly that is not a definable
> instance in a CAS.
This is not clear to me. I do not set any problem (in principle) with
such a type. What problems to you see?
> So I would like to see something as a type:
> lazyType = Type + T( lazyType )
> where the rhs is not evaluated (lazy). In terms of sets of elements
> of some type foo, we have foo, Set(foo), Set(Set(foo)), etc
> The monad multiplication operation will not look into the deeper
> nesting if always applied on the outer level (which is feasible due
> to associativity).
Yes. I don't think this is a problem. This is possible now. In fact
this is (more or less) done in the Axiom category ListAggregate now
for the specific case of List. The idea of MonadCat is to do this in
general for all monad-like types.
> So if the type checking would just see that there is
> at least on Set(bar) there, then the type of bar would not matter.
> I had the feeling that your code wanted to do this just for three
> levels:
> I, List(I), List(List(I))
No. Join requires the top two levels but th
Regards,
Bill Page.
Martin Baker
> I would like to write:
>
> )abbrev category MONADC MonadCat
> MonadCat(T:Type, M:T->T):Category == with
> join: M M T -> M T
>
> )abbrev domain MYSET MySet
> MySet(T:SetCategory): MonadCat(T,MySet) with
> finiteAggregate
> == add
> ...
>
> But this doesn't work even in OpenAxiom (yet).
Do you have any views on why this is and whether there is any prospect
of a change to SPAD to allow this?
Just to try to help my own understanding of the issue I have been
thinking about it and it seems to my non-expert eye that 'Type' in:
MonadCat(T:Type, M:T->T):Category == with
is too general(no type checking), in that if Type is the top if the
category lattice then T should bind with values like '3' and "text" as
well as types like Integer?
Would it help the compiler, as well as human readers of the program,
if we could specify a higher kinded type like this:
MonadCat(T:HigherType, M:T->T):Category == with
Another idea that occurred to me would be to have an equivalent to the
Haskell typeclass. Like a higher order (non-concrete) category, say a
category where all the function parameters and returns are only
specified in terms of types (not values). So the equivalent to the
Haskell typeclass might be:
)abbrev hcategory MONADC MonadCat
MonadCat(M):Category == with
join: M M A -> M A
So this could be implemented with 'M' as say:
Integer -> Set Integer or Set Integer -> Set Set Integer ...
Ideally 'A' would only need to be defined in join.
I was thinking that the advantage of this would be that the compiler
would know that a functor could be applied to a type when they are
adjacent so
(A -> M A) A
would bind to M A
As I say, I'm just trying to get these issues clear in my mind and to
try to understand if SPAD will ever be as powerful as Haskell with
this type of construct.
Martin
Bill Page
> On Saturday 03 Dec 2011 21:42:20 Bill Page wrote:
>> I would like to write:
>>
>> )abbrev category MONADC MonadCat
>> MonadCat(T:Type, M:T->T):Category == with
>> join: M M T -> M T
>>
>> )abbrev domain MYSET MySet
>> MySet(T:SetCategory): MonadCat(T,MySet) with
>> finiteAggregate
>> == add
>> ...
>>
>> But this doesn't work even in OpenAxiom (yet).
>
> Do you have any views on why this is and whether there is any prospect
> of a change to SPAD to allow this?
>
I reported this as a bug in OpenAxiom
http://sourceforge.net/tracker/?func=detail&atid=984524&aid=3448475&group_id=203172
Recent changes in OpenAxiom have changed the error message. The
original message "cannot form Join" is probably more indicative of
what is going wrong. The "apparent user error"
Cannot coerce #1 of mode Type to mode SetCategory
suggests to me that perhaps the compiler is not passing all the
information about the types of the arguments to MonadCat or perhaps
that the type inference is somehow incomplete. I expect that the more
recent message "The value NIL is not of type DATABASE." is likely due
to unrelated changes that Gaby is currently making to the compiler.
But that is just a guess. I wish I had enough time and skill to
actually work on these sort of compiler internals. These are in short
supply in all the Axiom projects. Although fixing this or explaining
why should not work may not be a currently priority, I am fairly sure
that the changes Gaby is making to the compiler will eventually
resolve it one way or another.
> Just to try to help my own understanding of the issue I have been
> thinking about it and it seems to my non-expert eye that 'Type' in:
> MonadCat(T:Type, M:T->T):Category == with
> is too general(no type checking), in that if Type is the top if the
> category lattice then T should bind with values like '3' and "text" as
> well as types like Integer?
Yes, Type is the top of the category lattice but values like '3' and
"text" are ... well, just values. T is necessarily a domain in the
category Type. It does not make sense in Axiom to talk about values
binding to categories. Axiom has a two-level type system consisting of
categories and domains. In fact in Axiom values do not "bind" even to
domains. Values have no type in and of themselves. Only variables,
constants and formal parameters have types.
> Would it help the compiler, as well as human readers of the program,
> if we could specify a higher kinded type like this:
> MonadCat(T:HigherType, M:T->T):Category == with
>
No, I don't think so.
In MonadCat T is just some domain with an endofunctor M. A domain that
satisfies MonadCat(T,M) is expected to be a monad, i.e. it must export
operations that satisfy the monad axioms.
In MySet(T:SetCategory) we so specify that T satisfies SetCategory.
MonadCat(T,MySet) is a dependent type in this context.
> Another idea that occurred to me would be to have an equivalent to the
> Haskell typeclass. Like a higher order (non-concrete) category, say a
> category where all the function parameters and returns are only
> specified in terms of types (not values). So the equivalent to the
> Haskell typeclass might be:
>
> )abbrev hcategory MONADC MonadCat
> MonadCat(M):Category == with
> join: M M A -> M A
>
Except for omitting the type of M, I do not see much difference from
what I wrote above.
> So this could be implemented with 'M' as say:
> Integer -> Set Integer or Set Integer -> Set Set Integer ...
I don't think this makes sense. M must be an endofunctor, i.e.
something like 'Set' itself.
> Ideally 'A' would only need to be defined in join.
As I described T above, A must be the formal parameter of the monad
MySet as the endofunctor M .
> I was thinking that the advantage of this would be that the compiler
> would know that a functor could be applied to a type when they are
> adjacent so
> (A -> M A) A
> would bind to M A
>
I think this happens (or should happen) now.
> As I say, I'm just trying to get these issues clear in my mind and to
> try to understand if SPAD will ever be as powerful as Haskell with
> this type of construct.
>
I do not see any reason to claim that SPAD is somehow less "powerful"
than Haskell even as it stands now. To be sure both SPAD and Haskell
(not to mention, Lisp, C and assembler language, etc. ) are formally
universal. The concept of the "power" of a language is almost too
vague to be useful. Even the idea of the "expressiveness" of a
language is hard to quantify. How much "effort" it takes to write code
in one language or another is highly subjective. To a large extent it
comes down to a choice of style.
Regards,
Bill Page.
Martin Baker
> > Another idea that occurred to me would be to have an equivalent to the
> > Haskell typeclass. Like a higher order (non-concrete) category, say a
> > category where all the function parameters and returns are only
> > specified in terms of types (not values). So the equivalent to the
> > Haskell typeclass might be:
> >
> > )abbrev hcategory MONADC MonadCat
> > MonadCat(M):Category == with
> > join: M M A -> M A
>
> Except for omitting the type of M, I do not see much difference from
> what I wrote above.
>
> > So this could be implemented with 'M' as say:
> > Integer -> Set Integer or Set Integer -> Set Set Integer ...
>
> I don't think this makes sense. M must be an endofunctor, i.e.
> something like 'Set' itself.
>
> > Ideally 'A' would only need to be defined in join.
>
> As I described T above, A must be the formal parameter of the monad
> MySet as the endofunctor M .
This is a difference between what I wrote (which seem to me to be the
Haskell way of doing it) and your code. Because-
M=Set A=PI gives:
join: Set Set PI -> Set PI
M=Set A=Set PI gives:
join: Set Set Set PI -> Set Set PI
M=Set A=Set Set PI gives:
join: Set Set Set Set PI -> Set Set Set PI
So the same category represents all these, but not if A is a parameter
of the whole monad, this seems to me quite a fundamental aspect of
monads which your code does not support?
> > As I say, I'm just trying to get these issues clear in my mind and to
> > try to understand if SPAD will ever be as powerful as Haskell with
> > this type of construct.
>
> I do not see any reason to claim that SPAD is somehow less "powerful"
> than Haskell even as it stands now. To be sure both SPAD and Haskell
> (not to mention, Lisp, C and assembler language, etc. ) are formally
> universal. The concept of the "power" of a language is almost too
> vague to be useful. Even the idea of the "expressiveness" of a
> language is hard to quantify. How much "effort" it takes to write code
> in one language or another is highly subjective. To a large extent it
> comes down to a choice of style.
When I said "powerful as Haskell with this type of construct" I
specifically meant Haskell seems more powerful in the ways that it can
match on and combine these higher kinded types (I still get that
impression but perhaps I'll be proved wrong). It goes without saying
that SPAD is more powerful in other ways such as dependant types. I
hope you did not assume I was knocking SPAD in general, I do think it
helps to be clear about specific strengths and weaknesses of each
language.
Martin
Bill Page
Your comments have made me look more carefully at what I wrote in my
reply and you are right, there was something wrong with my original
code:
> On Saturday 03 Dec 2011 21:42:20 Bill Page wrote:
>> I would like to write:
>>
>> )abbrev category MONADC MonadCat
>> MonadCat(T:Type, M:T->T):Category == with
>> join: M M T -> M T
>>
>> )abbrev domain MYSET MySet
>> MySet(T:SetCategory): MonadCat(T,MySet) with
>> finiteAggregate
>> == add
>> ...
It does not make sense for me to write M:T->T.
T is a *domain* but M is supposed to be an endofunctor from some
*category* to the same category.
We really want
)abbrev category MONADC MonadCat
MonadCat(T:Type, M:Type->Type):Category == with
join: M M T -> M T
This is equivalent in this context to what actual appears in my
OpenAxiom bug report.
)abbrev category MONADC MonadCat
MonadCat(A : Type, M: Type -> Type): Category == with
if A has SetCategory then SetCategory
fmap: (A->A, %) -> %
unit: A -> %
join: M % -> %
mult: (%, %) -> %
--
Just replace % by 'M T'. And the error message is the same.
Oddly, this variant:
MonadCat(A : SetCategory, M: SetCategory -> SetCategory): Category == with
join: M M A -> M A
gives a different result:
>> System error:
Control stack exhausted (no more space for function call frames).
This is probably due to heavily nested or infinitely recursive function
calls, or a tail call that SBCL cannot or has not optimized away.
PROCEED WITH CAUTION.
--
But contrary to what you say, there is no problem (in principle) to write:
MonadCat(PI,Set) to get
join: Set Set PI -> Set PI
MonadCat(PI,Set Set) to get
join: Set Set Set PI -> Set Set PI
etc.
Regards,
Bill Page.
Gabriel Dos Reis
[...]
| We really want
|
| )abbrev category MONADC MonadCat
| MonadCat(T:Type, M:Type->Type):Category == with
| join: M M T -> M T
As far as I can tell, that compiles fine in OpenAxiom.
| This is equivalent in this context to what actual appears in my
| OpenAxiom bug report.
|
| )abbrev category MONADC MonadCat
| MonadCat(A : Type, M: Type -> Type): Category == with
| if A has SetCategory then SetCategory
| fmap: (A->A, %) -> %
| unit: A -> %
| join: M % -> %
| mult: (%, %) -> %
This also compiles just fine.
| --
|
| Just replace % by 'M T'. And the error message is the same.
|
| Oddly, this variant:
|
| MonadCat(A : SetCategory, M: SetCategory -> SetCategory): Category == with
| join: M M A -> M A
|
| gives a different result:
|
| >> System error:
| Control stack exhausted (no more space for function call frames).
| This is probably due to heavily nested or infinitely recursive function
| calls, or a tail call that SBCL cannot or has not optimized away.
|
| PROCEED WITH CAUTION.
That compiles fine with OpenAxiom.
Bill Page
> Bill Page <bill...@newsynthesis.org> writes:
> ...
> |
> | MonadCat(A : SetCategory, M: SetCategory -> SetCategory): Category == with
> | join: M M A -> M A
> |
> | gives a different result:
> |
> | >> System error:
> | Control stack exhausted (no more space for function call frames).
> | This is probably due to heavily nested or infinitely recursive function
> | calls, or a tail call that SBCL cannot or has not optimized away.
> |
> | PROCEED WITH CAUTION.
>
> That compiles fine with OpenAxiom.
>
I am sorry. I took it for granted that it was understood that these
errors are all generated when compiling MySet with this or another
definition of MonadCat.
Regards,
Bill Page.
Gabriel Dos Reis
that wasn't clear to me as you seemed to report many bugs at the same
time (or maybe wa sit just refinements?); I thought I had to compile
each file (in the bug report) to reproduce them each of time. I will
try again. Thanks.
PS: Ideally, it would be nice if I could just download one file and feed
it to OpenAxiom to reproduce the bug.
|
| Regards,
| Bill Page.
Bill Page
> Bill Page <bill...@newsynthesis.org> writes:
>
>
> | I reported this as a bug in OpenAxiom
> |
> | http://sourceforge.net/tracker/?func=detail&atid=984524&aid=3448475&group_id=203172
> |
> | Recent changes in OpenAxiom have changed the error message. The
> | original message "cannot form Join" is probably more indicative of
> | what is going wrong. The "apparent user error"
>
>
> When you write
>
> MySet(T:SetCategory): Join(MonadCat(T,MySet),SetAggregate(T)) with --...
>
> At the point where you are using MySet as argument to MonadCat, there
> is no indication of what the return type of MySet, and that is apparent :-)
>
There are numerous cases in the library where % occurs in the type of
a constructor. Consider:
-- lodop.spad.pamphlet: --
...
OrdinaryDifferentialRing(Kernels,R,var): DRcategory == DRcapsule where
Kernels:SetCategory
R: PartialDifferentialRing(Kernels)
var : Kernels
DRcategory == Join(BiModule(%,%), DifferentialRing, HomotopicTo R) with
if R has Field then Field
DRcapsule == R add
--
Apparently % refers to the functor 'OrdinaryDifferentialRing' applied
to the arguments '(Kernels,R,var)' but the compiler does not complain
of an apparent user error even though obviously there is no indication
of what the return type of 'OrdinaryDifferentialRing' is at that
point. Is this use of % somehow special to the compiler?
In another email thread I was asking for a method to refer to just the
functor, e.g. just 'OrdinaryDifferentialRing' not the whole
expression 'OrdinaryDifferentialRing(Kernels,R,var)'. Suppose this
was denoted by %%. Then
%%(Kernels,R,var)
would supposedly be equivalent to %.
This %% is essentially what I wanted to write instead of 'MySet'
above. It seems to me that whatever is special about % could also be
special about %%, no?
I would like to be able to declare that some domain constructor is a
monad in the same way that 'OrdinaryDifferentialRing' is declared to
satisfy 'BiModule(%, %)'. But to do this I need a way to refer to
"this functor" because in the definition of MonadCat I need to be able
to apply that functor twice. In this case the use of % (a single
application of the functor) is not enough.
%%( %%( A ) )
> | Cannot coerce #1 of mode Type to mode SetCategory
>
> There is a cascade of errors, and this one relates to dependent
> contravariant coercion that I discussed a couple of weeks ago.
>
> | suggests to me that perhaps the compiler is not passing all the
> | information about the types of the arguments to MonadCat or perhaps
>
> that is correct. But the use of MySet as argument of MonadCat needs to
> be fixed first.
>
Is possible to reference MySet implicitly as "this functor" in a
manner similar to the use of % ?
> | that the type inference is somehow incomplete. I expect that the more
> | recent message "The value NIL is not of type DATABASE." is likely due
> | to unrelated changes that Gaby is currently making to the compiler.
> | But that is just a guess. I wish I had enough time and skill to
> | actually work on these sort of compiler internals. These are in short
> | supply in all the Axiom projects. Although fixing this or explaining
> | why should not work may not be a currently priority, I am fairly sure
> | that the changes Gaby is making to the compiler will eventually
> | resolve it one way or another.
>
> Believe it or not, Gaby has a lot on his hands -- far more than it can
> handle just now :-)
>
Understood and much appreciated!
> I appreciate bug reports in experimenting with new constructs.
> One should also note that transliterating Haskell into Spad can be
> as fun and entertaining as transliterating English to French or the
> other way around. Certain things will just sound OK; others might
> give you a pause :-)
>
Sure, but the abstraction of "monad" really has nothing directly to do
with Haskell of other languages as such. It seems reasonable to
consider independently how this notion should be expressed in Spad.
Regards,
Bill Page.
Gabriel Dos Reis
| On Mon, Dec 5, 2011 at 6:37 PM, Gabriel Dos Reis wrote:
| > Bill Page <bill...@newsynthesis.org> writes:
| >
| > [...]
| >
| > | I reported this as a bug in OpenAxiom
| > |
| > | http://sourceforge.net/tracker/?func=detail&atid=984524&aid=3448475&group_id=203172
| > |
| > | Recent changes in OpenAxiom have changed the error message. The
| > | original message "cannot form Join" is probably more indicative of
| > | what is going wrong. The "apparent user error"
| >
| > It is indeed "apparent user error" :-)
| >
| > When you write
| >
| > MySet(T:SetCategory): Join(MonadCat(T,MySet),SetAggregate(T)) with --...
| >
| > At the point where you are using MySet as argument to MonadCat, there
| > is no indication of what the return type of MySet, and that is apparent :-)
| >
|
| There are numerous cases in the library where % occurs in the type of
| a constructor.
MySet is a functor not a domain, you are defining its *return* type by
using it in positing where the return type is expected to be known,
i.e. when the compiler is expanding MonadCat(T,MySet) to see whether it
makes sense as a category.
% is a special variable in that it is the only one in the system (if my
count is correct) that implements a co-inductive fixpoint. Furthermore,
it is a domain, not a constructor.
And the current implementation of co-induction semantics for % in the
compiler is "quick and dirty" hack, see line 1075 of
http://svn.open-axiom.org/viewvc/open-axiom/1.4.x/src/interp/define.boot?revision=2519&view=markup
[...]
| Is this use of % somehow special to the compiler?
Yes, see above.
| In another email thread I was asking for a method to refer to just the
| functor, e.g. just 'OrdinaryDifferentialRing' not the whole
| expression 'OrdinaryDifferentialRing(Kernels,R,var)'. Suppose this
| was denoted by %%. Then
|
| %%(Kernels,R,var)
|
| would supposedly be equivalent to %.
|
| This %% is essentially what I wanted to write instead of 'MySet'
| above. It seems to me that whatever is special about % could also be
| special about %%, no?
Yes, sort of.
For OpenAxiom, I would prefer to have a general principled mechanism to
write co-inductive definitions than special variable hacks.
Or, maybe all constructors should be co-inductive and only ordinary values
should be inductive I do not know yet.
This kind of co-inductive-style use is quite popular in mainstream
languages such as C++, Java, or C#. Usually it comes at some price --
e.g. you would have to accept that the compiler can't catch some
"useless" definitions which might be result of typos as opposed to
intentional or mere curiosities.
[...]
| Is possible to reference MySet implicitly as "this functor" in a
| manner similar to the use of % ?
As I said above, for OpenAxiom I would prefer a principled way to write
co-inductive definitions and not introduce yet another special variable.
If I have two, then surely I will have three; so I would prefer to have
a general feature. This needs some thinking.
[...]
| > I appreciate bug reports in experimenting with new constructs.
| > One should also note that transliterating Haskell into Spad can be
| > as fun and entertaining as transliterating English to French or the
| > other way around. Certain things will just sound OK; others might
| > give you a pause :-)
| >
|
| Sure, but the abstraction of "monad" really has nothing directly to do
| with Haskell of other languages as such. It seems reasonable to
| consider independently how this notion should be expressed in Spad.
I hope nobody is under the illusion that I believe the mathematical
notion of monad is Haskell-specific. My observation was merely related
to the fact that since the beginning I was under the impression that
people are saying "here is what people write in Haskell as monad; how do
I write that code in Spad?"
-- Gaby