Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

On 05/09/2007 10:02 AM, Bill Page wrote:
> 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. It is type *constructor*,
> that is, when given 'Int' MkInt returns a subtype of Expr.

Before you criticize... I don't claim that I am right. What comes is 
just my current understanding.

Let me quote from
http://en.wikipedia.org/wiki/Algebraic_data_type

  Here, Empty, Leaf and Node are the constructors. Somewhat similar
  to a function, a constructor is applied to arguments of an
  appropriate type, then yielding an instance of the data type
  to which the constructor belongs.

> The
> difference might seem a little subtle at first but we
> can clearly distinguish such things in languages like
> Spad and Aldor.
> In Spad and Aldor a type constructor is a function that
> returns a Type.

I agree on the latter, but as you said, it is a "type constructor".
In the wikipedia article "constructor" sounds to me more like a 
constructor in object oriented languages like Java. One creates an 
instance of the type. So as in
http://lists.nongnu.org/archive/html/axiom-mail/2007-05/msg00001.html
one says

eval (MkInt i) = i

i.e. the argument is an integer and not the type Integer. And since

eval::Expr -> Int

the input to eval should be an actual element of type Expr, not the type 
Expr itself.

> For example 'Complex' is such a
> constructor, so 'Complex Integer' is the domain of
> Gaussian Integers.
> Similarly in Haskel 'MkInt' is a type constructor and
> 'MkInt Int' is an algebraic type, in exactly the same way
> that  'Complex Integer' is a domain in Axiom. One should
> not be tempted to write: 'Complex 1'. Similarly 'MkInt 1'
> would not make sense.

Ah, is begin to understand. Have you seen my note on the use of the maros

Mkint ==> MkInt;
Mkadd ==> MkAdd;
Mkmul ==> MkMul;

? MkInt is the constructor (in the oo sense) and Mkint is just a tag.

The tag Mkint corresponds to the MkInt in the above Haskell code. And a 
tag (together with the (aldor) functions MkInt, etc. is enough to 
simulate the Haskell code. In the Haskell code Mkint and MkInt is 
denoted by the same identifier.

I still don't say that one cannot simulate Haskell's MkInt by a Aldor 
domain constructor. You have shown that it works on
http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes .
But it seems to be unnecessary overhead to me.

And I cannot say whether MkInt is a type constructor in Haskell, since I 
don't know the language very well. An argument against it would be that
there is no code of the form

data MkInt a = ...

But I better should be quiet, I simply don't know enough of Haskell.


>> Well. What do you do with a data structure that has no
>> accessor functions?
>
> One is supposed to define functions over an algebraic data
> type by recursion. So what in Gaby wrote:
>
>   eval::Expr -> Int
>   eval (MkInt i) = i
>   eval (MkAdd x y) = (eval x) + (eval y)
>   eval (MkMul x y) = (eval x) * (eval y)
>
>
> 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.

I agree that it's a source of confusion. But I must admit that I would 
have written

  MkInt: Int -> Expr

instead. Otherwise there would be a type mismatch in

  eval (MkInt i) = i

since MkInt(Int) is not equal to Expr. Don't you agree?

>> What do you gain by introducing the domains MkAdd and
>> MkMul?
>
> Well, it allows me to write
>
> Expr: ExprCat
>   == add
>     Rep == Union(Mkint:MkInt(Integer),
>                  Mkadd:MkAdd(%,%),
>                  Mkmul:MkMul(%,%))
>
> where Rep is a union of types in ExprCat. Then
>
>   rep: % -> Rep
>
> automatically classifies members of Expr (implements the
> pattern matching) and
>
>   per: Rep -> %
>
> injects these subtypes into Expr.

Unfortunately, in Aldor rep and per are macros and actually only do some 
"pretend". What you need is an actual functions "union" to map an 
element of type MkInt(Integer) into Rep.


>> That is a step to avoid a lot of (if not all) mutual
>> recursion in the construction of the Axiom library.

> I still think that is wishful thinking. :-(

It is probably not so wishful if you have looked a bit at the 
bootstrapping of LibAldor and LibAlgebra. For example, Integer is not a 
Ring in LibAldor, because Ring is only introduced in LibAlgebra. Still 
one can do lots of things already with LibAldor. I must say, I don't see 
a big bootstrapping problem at all in LibAldor.

Ralf