Re: [Axiom-mail] Spad and inductive types

[Bill Page]

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. It is type *constructor*,
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. 

In Spad and Aldor a type constructor is a function that
returns a Type. 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. 

> > >     MkAdd: (%, %) -> %;
> > >     MkMul: (%, %) -> %;

Here you have not defined algebraic type constructors. We
need 'MkAdd(MkInt Int,MkInt Int)' to be a *type*, like
'Cross(Integer,Integer)' is a type in Aldor. One would not
write: 'Cross(1,1)'. In fact, 'MkAdd(MkInt Int, MkInt Int)'
is another subtype of Expr. Even more generally
'MkAdd(Expr,Expr)' is a subtype of Expr which requires
of course that Expr be at least countably infinite. 

> > >     apply: (%, 'MkInt') -> Integer;
> > >     apply: (%, 'MkAdd') -> (%, %);
> > >     apply: (%, 'MkMul') -> (%, %);
> > >     case: (%, 'MkInt') -> Boolean;
> > >     case: (%, 'MkAdd') -> Boolean;
> > >     case: (%, 'MkMul') -> Boolean;
> >
> > I think having 'apply' and 'case' appear as exports of
> > Expr is very undesirable. 
>
> 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. 
In Axiom we would usually call this a coercion. 

Similarly 'MkAdd' denotes both a type constructor in
'MkInt Expr Expr' and a binary function

  MkAdd: (Expr,Expr) -> MkAdd Expr Expr

> > > } == add {
> > >     Rep == Union(
> > >         Mkint: Integer,
> > >         Mkadd: Record(left: %, right: %),
> > >         Mkmul: Record(left: %, right: %)
> > >     );
>
> > Why not write a Union of the constructors, instead of their
> > representation? I.e. something like:
>
> >      Rep == Union(
> >          Mkint: MkInt,
> >          Mkadd: MkAdd(%,%),
> >          Mkmul: MkMul(%,%)
> >      );
>
> Could probably be done, but how is MkInt different from
> Integer?

'MkInt Integer' is a type distinct from but isomorphic to
Integer so it is "natural" to take Integer as the
representation of the type 'MkInt Integer' and rep as the
coercion. In your case 'MkInt' is the coercion function. 

> 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. 

> If that is needed, it can be done as you showed at
> http://wiki.axiom-developer.org/SandBoxInductiveType . 
> 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, Expr, Expr)). 
>
> In Aldor the tags appear in front of : so the Cross
> would have one argument less (and I have replaced Cross
> by Record (which is probably not necessary). 

Well yes as a tagged union we might write:

Expr:Type == Union(MkInt:Integer,
                   MkAdd:Cross(Expr, Expr),
                   MkMul:Cross(Expr, Expr));

Aldor even appears to solve this recursion, but it does
not seem to export anything usable by Axiom. See:

http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes

I do agree that as types 'MkAdd Expr Expr' is isomorphic
to 'Cross(Expr,Expr)'. That is why I say MkAdd is a type
constructor. 

> > >     import from Rep;
> > >     MkInt(i: Integer): % == per union i;
> > >     MkAdd(x: %, y: %): % == per [Mkadd == [x, y]];
> > >     MkMul(x: %, y: %): % == per [Mkmul == [x, y]];
> > >
> > >     apply(x: %, t:'MkInt'): Integer == rep(x).Mkint;
> > >     apply(x: %, t:'MkAdd'): (%, %) == explode rep(x).Mkadd;
> > >     apply(x: %, t:'MkMul'): (%, %) == explode rep(x).Mkmul;
> > >
> > >     (x: %) case (t:'MkInt'): Boolean == rep(x) case Mkint;
> > >     (x: %) case (t:'MkAdd'): Boolean == rep(x) case Mkadd;
> > >     (x: %) case (t:'MkMul'): Boolean == rep(x) case Mkmul;
> >
> > Why does this construction look so different from the
> > definition of Expr2 in
> >
> > http://wiki.axiom-developer.org/SandBoxInductiveType ?
> >
> > > }
>
> I don't actually understand whether this is meant in a
> positive or negative sense. I would rather call my code
> a variation of yours. 

As explained above, I see major differences. 

> The biggest difference probably is that you cannot produce
> that what was in file bbb.as, because in an "extend Expr"
> you would have no way to access the internal structure of
> Expr. 

In

http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes

I show how to use extend. 

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

I tried to eliminate eval and coercion to OutputForm from
my example in SandBoxAldorInductiveTypes, but I ran into
problems because of the recursion and the fact that I
would have to extend the category ExprCat. Apparently
Aldor does not allow me to do this (yet, see chapter of
AUG on extend). 

> To such a data structure one could add features
> (= functions) later without changing or knowing the
> actual representation. 

In my example I do seem to require some knowledge of the
representation (i.e. define Rep == ...). Maybe this could
be avoided if I invented some other interface. 

> 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. :-(

Regards,
Bill Page.