RE: [Axiom-developer] "has" and "with" (was curious algebra failure)

[Gabriel Dos Reis]

On Mon, 13 Aug 2007, Weiss, Juergen wrote:

| I found the old document about type equivalence in Scratchpad. It's:
| A New Algebra System, May, 29 th 1984, James H Davenport. I have only
| found a paper version. Maybe someone has an online version.
| 
| It states that:
| 1. Two named types are only equivalent if the names are the same.
| 2. Anonymous types are equivalent when stucturally equivalent
| 3. An anonymous type is never equivalent to a named type.
| 
| So following 1.
| 
| t1 == List Term
| t2 == List Term
| x : t1
| y : t2
| y := x      
| 
| is not supposed to work,
| 
| but following 2.
| 
| x : List Term
| y : List Term
| y := x    
| 
| is ok,
| 
| and following 3.
| 
| t == List Term
| x : List Term
| y : t
| y := x   
| 
| is not supposed to work as well
| 
| All examples are taken from the paper.
| 
| I am not sure how much of this design is preserved in the current
| system. But without having had an intense look at the examples,
| I got the impression, that they follow the rules above.

Many thanks for digging up the archive.

I understand the above is about "type equivalence"; how about matching?
That is, which way do you think the checking of the  code in Monad should 
go according to that paper? 

-- Gaby