Re: [Axiom-mail] Spad and inductive types

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| Quoting Gabriel Dos Reis <address@hidden>:
| 
| > On Wed, 9 May 2007, Bill Page wrote:
| >
| > [...]
| >
| > | > > ... in Haskell, by a kind of convenient abuse of notation
| > | > > (or polymorphism if you wish) 'MkInt' also denotes a
| > | > > function
| > | > >
| > | > >   MkInt: Int -> MkInt Int
| > | > >
| > | > > that creates an object of type 'MkInt Int' from an object
| > | > > in 'Int'. I think this is a potential source of confusion. |
| > | Probably I should have avoided the wording above that might
| > | (incorrectly) be interpreted as a slur against Haskell. Well, I
| > did not interepret it as a slur against Haskell.  However, it did
| > appear to me to be fundamentally incorrect to miss the core ideas of
| > algebraic data typea and how they lead to GADT:
| >
| >     data Expr where
| >       MkInt:: Integer -> Expr
| >       MkAdd:: Expr -> Expr -> Expr
| >       MkMul:: Expr -> Expr -> Expr
| >
| > That is all that is needed to define more operations on values of
| > type Expr.
| 
| I agree that GADT is important in the context of Haskell which has
| (in principle) a complete and formal semantics. But I do not think it
| is so interesting in Spad and Aldor which already has the full
| machinery of abstract data types.

I beg to disagree; and furthermore, I do believe you are wrong about
the core ideas here.

| If we want to add more operations
| on a given type, we have 'add inheritance', e.g.  NewExpr: ExprCat
| with ... = Expr add ... 

Except that now you have a distinct domain from Expr; that may be what
is desired in some situations.  But it most situations, and the one I'm
particularly concerned about, that is NOT what is desired.

| and even post-facto extension of domains in Aldor.

Please, notice that the situation is radially different in Aldor than
in Spad, and please also remember that my question has to do with
Spad, not Aldor.

| I can see however why this is interesting from the point of
| view of
| Boot. If Boot could be given a formal semantics like Haskell, then
| one might be much more confident of it's use to implement Spad
| and therefore ultimately confidence in the semantics of Spad. 

That is one aspect of it; another is simply that what is so simple in
Boot must remain in Spad; and yet another one is from practical
introduction to proramming with Spad point of view.  

-- Gaby