Re: [Axiom-mail] Equivalence between named domain and %

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

| On Monday, October 16, 2006 7:30 PM Gabriel Dos Reis wrote:
| 
| > | >   Consider the following code snipet:
| > | >
| > | >      )abbrev domain T T
| > | >
| > | >      Decl := Record(name: Symbol, type: T)
| > | >
| > | >      T(): Public == Private where
| > | >        Public ==> with
| > | >          type: Symbol -> %
| > | >          decl: (Symbol, %) -> Decl
| > | >        Private ==> add
| > | >          decl(n,t) == [n,t]
| > | >
| > | > The SPAD compiler complains on the definition of decl with the
| > | > following message
| > |
| > 
| > On Mon, 16 Oct 2006, Page, Bill wrote:
| > | Why would you consider the type T itself to be known in the scope
| > | where the value of Decl is computed?
| > 
| > Because inside the definition of T(), % is supposed to refer to the
| > domain defined, i.e. T.
| 
| Yes that is correct. But you are asking SPAD explicitly to evaluate
| Record(name: Symbol, type: T) outside of and *prior to* the definition
| of T(). It seems that in the normal mode of operation of the SPAD
| compiler this is out of context for T. (But see how this can be
| changed below.)
| 
| > Notice that the only thing that is needed to be known is the type
| > name.
| 
| I think it is instructive to see what Aldor says about this
| construction:
| 
| Decl := Record(name: Symbol, type: T)
| ^
| [L4 C1] #7 (Error) `Decl' is used in a type, so must be constant,
|   and so cannot be assigned to.
| 
| After correcting the definition, Aldor compiles this thing without
| complaint:

Bill -- 

Thank you for investigating this further.

My understanding of "==" in SPAD is that it is a "delayed evaluation",
whereas in Aldor it is a "constant declaration".  Of course, I'm not
interested in non-constant type Decl, but I'm wondering how
do you reconcile those two interpretations?

If my understanding is correct, this problem touches upon the fact
that the SPAD compiler does not know (at the moment) how to properly
resolve recursive declaration/definitions of types.  Is that correct?

Since, under the hood, almost everything is a pointer, why is the
compiler having trouble admitting recursion?

At the language semantics level, is the declaration in error?
If yes, it makes the language less regular and unintuitive.

I see the trick with $bootStrapMode, but I would think that is
essentially a hack to work around a bug in the compiler.  I would be
very much interested in laying down the semantics and see how the
compiler could be convinced to do the Right Thing.


If I have time today, I'll investigate the possibility of augmenting
the compiler to use the identity coercion from % to T, when T is the
current domain. 

Thanks!

-- Gaby