Re: Spad and inductive types

On Tue, 8 May 2007, Ralf Hemmecke wrote:

| But I thought that the Haskell
| 
| data Expr = MkInt Int
|           | MkAdd Expr Expr
|           | MkMul Expr Expr
| 
| is more like
| 
| Union(Cross(Tag, Int),
|       Cross(Tag, Expr, Expr),
|       Cross(Tag, Exrp, Expr)).


yes, conceptually, that is the case.

[...]

| As I understood Gaby, he wanted to define just the data structure without any
| additional features like eval or coercion to OutputForm.

You understood right.

The data constructors

   MkInt: Integer -> Expr
   MkAdd: Expr -> Expr -> Expr
   MkMul: Expr -> Expr -> Expr

are essentially the only thing people need to know about the
Expr data type in order to write more operations on it. 
That realization has been taken furthermore to the notion of
"Generalized Algebraic Data Type" (or GADT for short).

Many thanks for your answers.

-- Gaby