Re: [Axiom-mail] Spad and inductive types

[Bill Page]

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. If we want to add more operations
on a given type, we have 'add inheritance', e.g. 

  NewExpr: ExprCat with ... = Expr add ... 

and even post-facto extension of domains in 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. 

Am I wrong in presuming this underlying motivation? But if you still
think I am just confused, please don't feel obliged to say more than
that you think so... 

Regards,
Bill Page.