Re: [Axiom-mail] Spad and inductive types

[Gabriel Dos Reis]

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.


[...]

| Yes, "union" is needed in the implementation, but my point is that
| 
|   rep: % ->Rep
| 
| maps elements of Expr directly into the Union. 'case' can then be
| used to classify them as 'MkInt ...', 'MkAdd ...' or 'MkMul ...'. 

Indeed.

-- Gaby