[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: Bill Page
Subject: Re: [Axiom-developer] "has" and "with" (was curious algebra failure)
Date: Mon, 13 Aug 2007 13:04:42 -0400

On 13 Aug 2007 00:39:45 -0500, Gabriel Dos Reis wrote:
> ...
>    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?

Yes, thank you! But of course that is how packages and domains in Spad
are normally written and this package does in fact compile just fine
in Spad. See:

as it should.

The question of coercing Monad to

   SetCategory with "*": (%, %) -> %

must be yes. I guess the question still is how? and why? does it work.

Bill Page.

reply via email to

[Prev in Thread] Current Thread [Next in Thread]