Re: [Axiom-mail] Spad and inductive types

[Gabriel Dos Reis]

"Bill Page" <address@hidden> writes:

| Quoting Ralf Hemmecke <address@hidden>:
| 
| >
| >>  All the exports that appear are basically the
| >>> exports of the Union (OK, Union still has a few more.)
| >
| >>> ---BEGIN aaa.as
| >>> #include "aldor"
| >>> #include "aldorio"
| >>>
| >>> define ET: Category == with; -- ExpressionType
| >>> Expr: ET with {
| >>>     MkInt: Integer -> %;
| >>
| >> It doesn't look right to me that the MkInt constructor
| >> takes a specific integer as a parameter while MkAdd and
| >> MkMul take a type.
| >
| > Huh? The MkAdd also take specific elements of Expr. That
| > is not different from an element of Integer. It's at the
| > same level.
| 
| No, I think there is a serious misunderstanding here. What
| Gaby is talking about are "algebraic data types". See for
| example:
| 
| http://en.wikipedia.org/wiki/Algebraic_data_type
| 
| In Gaby's example Haskell code:
| 
|    data Expr = MkInt Int
|            | MkAdd Expr Expr
|            | MkMul Expr Expr
| 
| MkInt is *not* a function which when given an Integer
| returns something of type Expr.

I disagree: MkInt *IS* such a function.  

| It is type *constructor*,
      ^^^^^^^^^^^^^^^^^^^^

No, that is incorrect.

| that is, when given 'Int' MkInt returns a subtype of Expr. The
| difference might seem a little subtle at first but we
| can clearly distinguish such things in languages like
| Spad and Aldor.

I believe you're confused.  MkInt, MkAdd, and MkMul are *data*
constructors -- I believe I've said that many times.

A type constructor is a different thing.

-- Gaby