Re: [Axiom-developer] A curious algebra failure

[Stephen Wilson]

Gabriel Dos Reis <address@hidden> writes:
[...]
> | Right.  What I am saying is that in the type context
> | 
> |     S : SetCategory with "*": (%, %) -> %
> | 
> | when % denotes MONAD, the category of % (its `principle category' as I
> | called it, since in the general case it is anonymous), satisfies the
> | context.  Certainly MONAD has SetCategory and an export "*": (%, %) ->
> | %.  The nominal/structural typing rules (not that I have tried to
> | define them formally) are just my way of thinking about the issue.
> 
> I think I understand what you're saying.  I'm not sure they match Spad typing
> rules.  See the discussions in sections 12.8 and 12.12 of the Axiom book.
> The short version is that 
> 
>     domains belong to categories by assertions.

Yes.  I agree with the sections you cited and in particular the quote
above.  The basic detail is that for some domain definition D and
category C:

   D() : Exp == Impl where
    Exp == C with
      foo : () -> %
    Impl == add ...

By assertion and assertion alone does D satisfy C.  It is not enough
to list the exports of C explicitly.  We agree on that, I think.

Now, C is not the most general category which D inhabits, which I
think we both agree on too.  In fact, any `add' expression could
inhabit many several Categories, we simply refine the possibilities
when we bind an `add' in a definition. Just for the sake of this
discussion, imagine if there were a categoryOf operator, then one
value for it to return is:

   categoryOf(D)  ==>  C with foo : () -> %

In other words, an anonymous category can capture both a nominal
assertion (the named categories on the lhs), and a structural
assertion (the lhs exports).  For example:

   C (S : with foo : () -> %) : Category == with ...

Here, S will match _any_ domain with an export `foo' of the
appropriate type.  Although it may not be explicitly documented, I do
think that this is the intent of the Spad language.
 
Similarly, anonymous `add' expressions should work in a comparable
way. Using C above, the following should be well typed:

   C( add foo(): % == ... )

This is using the very same type rules that would apply to a named
definition:

   D : C == add 
     foo(): % == ...

So I think we need this nominal/structural interpretation for `with'
expressions in order for the type system to make sense.


> | If this interpretation does not hold, what kind of expression could
> | possibly satisfy the context S above?
> 
> That is the whole problem. :-)
> 
> As you suggested, I suspect it should have been written like
> 
>      if S has SetCategory and S has "*"
> 
> The trouble is that we don't want to test just for the name "*".  We
> want to test for the signature
>           
>           "*":(%, %) -> %
> 
> I don't know how to write that in Spad -- Ralf?

In Aldor you can write the full `with' expression:

      if S has SetCategory with { *:(%, %) -> % }

I certainly think this would be good for Spad.  I think it effectively
captures the meaning of what anonymous categories denote.  

As a little aside, I am still thinking about `type patterns', so the
above `has' expression might we reducible to a function in that
context.  Imagine ML or Haskell style function definition by cases:

     fn (D : SetCategory with { *:(%, %) -> % }) => ...
      | (_ : _) => ...

In other words, I do not see `has' as primitive, just a syntactic
sugar.  Even run time predicates could be handled using the same
techniques as is common in ML style languages:

     fn (r : Ring) when prime? r => ...  

Well, thats a little far afield, but I thought it might be worth
mentioning.  Even if such expressions are not visible to the
programmer, it _might_ be a decent model for the compiler to use
internally.


Steve