Re: Spad and inductive types

On Wed, 9 May 2007, Ralf Hemmecke wrote:

| > 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.
| 
| Gaby, I think I must disagree with your last sentence. It might probably be
| correct for Haskell, because there is the pattern matching thing, but in
| general one would need also functions like
| 
| apply: (%, 'MkInt') -> Integer;
| apply: (%, 'MkAdd') -> %
| 
| case: (%, 'MkInt') -> Boolean;
| etc.
| 
| Accessor functions seem to be somewhat hidden in Haskell, but in Aldor they
| would have to be explicit.

Yes, you are right --  I implicitly assumed accessors (in terms of
pattern matching) or case expression in case of Spad or Aldor.

You're right that I should have spelled it out explicitly.

| Anyway, that GADT example above looks already surprisingly like Aldor
| (although it probably means something else --- what exactly?).

It means that Expr is a datatype with the data constructors listed
in the where clause, and only those.

I believe the core ideas are present in Boot and Aldor, but they have
not been made as explicit and concise as it could be.

-- Gaby