[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure)
From: 
Gabriel Dos Reis 
Subject: 
Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure) 
Date: 
Mon, 13 Aug 2007 12:06:16 0500 (CDT) 
On Mon, 13 Aug 2007, Bill Page wrote:
 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:

 http://wiki.axiomdeveloper.org/SandBoxMonad

 as it should.

 The question of coercing Monad to

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

 must be yes.
A question is "why must it be `yes'"?
 I guess the question still is how? and why? does it work.
Indeed.
 Gaby
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), (continued)
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), William Sit, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
 [Axiomdeveloper] "has" and "with" and bug, Ralf Hemmecke, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" and bug, William Sit, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" and bug, Ralf Hemmecke, 2007/08/13
 [Axiomdeveloper] Re: "has" and "with" and bug, Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure),
Gabriel Dos Reis <=
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16