[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] "has" and "with" (was curious algebra failure)
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] "has" and "with" (was curious algebra failure) |
Date: |
13 Aug 2007 00:39:45 -0500 |
"Bill Page" <address@hidden> writes:
| Gaby,
|
| On 8/12/07, you wrote:
| > On Sun, 12 Aug 2007, William Sit wrote:
| >
| > | Isn't the problem whether 'Monad has SetCategory with
| > | "*":(%,%)->%' ? My answer would be yes. This should not be
| > | related to equivalence of categories or domains. We
| > | already have seen examples that Integer has with
| > | _*:(Integer, Integer)->Integer. Here, we are not saying
| > | 'Monad is SetCategory with "*":(%,%)->%'.
| >
|
| Sorry for my confusion. In fact I agree with William. This is not
| directly related to type equivalence. We need something more general
| than type equivalence. We need to know when one category is a
| subcategory of another. The type equivalence rules to which Juergen
| referred must be applied to the parts of the category expressions in
| order to determine this relationship.
|
| You wrote:
|
| > > 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. It is
| > > that parameter S which is being used to instantiate
| > >RepeatedSquaring. However, RepeatedSquaring expects its
| > >(domain) argument to be of the unnamed category
| > >
| > > SetCategory with "*": (%,%) -> %
|
| Your statement of the problem is a little confusing to me since the
| parameter S is the parameter of RepeatedSquaring. But as you say, it's
| type is given by the unnamed category above. You are concerned because
| what is being passed to RepeatedSquaring is a domain of type category
| named Monad. But clearly a domain of type Monad is also is a member of
|
| SetCategory with "*": (%,%) -> %
|
| since Monad is a subcategory of this category - any domain that "has"
| Monad will necessarily provide all of the exports required by
| RepeatedSquaring. RepeatedSquaring requires it's (domain) argument to
| be of type that is a subcategory of this unnamed category.
A few obversations:
1. When a function is called, the compiler/interpreter determines
whether the arguments used to call the function are coercible
to the type of the formal parameters of the function, when it
was declared.
What that means concretely is that when we declare a function
like
foo: Double -> Double
and we attempt foo(4), the compiler/interperter does not start
looking whether the value 4 "has" sin, cos, and many operations
that hold for Doubles. Rather, it determins whether the value
4 can be converted the type Double, if yes, it applies that
conversion and generate call to foo() with the result of the
of the conversion as argument.
That looks intuitive enough. And I suspect we all agree.
2. When one defines a category with default implementation, like
Monad, the compiler extracts the "purely categorial" part of
Monad, e.g. the exports; then it implicitly creates a package
Monad& with an implicit parameter S of type Monad. E.g., it is
as if the code was written:
)abbrev package MONAD- Monad&
Monad&(S: Monad): Public == Private where
Public ==> with
"**" : (S, PositiveInteger) -> S
Private ==> add
import RepeatedSquare(S)
x ** n == expt(x, n)
Now the compiler goes on typecheking the defnition x ** n.
It sees the use of expt() and find out that the only expt() in
scope if the one from RepeatedSquare(S). Then it tries
to instantiate that package -- just like a function call.
From there, it applies the usual rules: Can I coerce S of
type Monad to the expected argument type of RepeatedSquare()?
They answer comes out as "no". Hence the error.
Is that less confusing?
-- Gaby
- 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/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, 2007/08/13
- 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 <=
- 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
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16