Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

Dear Bill,

I only have a comment on the following.

> > 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?
>
> 'MkInt i' is a member of the type 'MkInt Integer' which is
> a subtype of Expr. The expression
>
>     eval (MkInt i) = i
>
> only defines eval over this subtype of Expr. The complete
> definition of 'eval' also requires two other definitions for
> 'MkAdd Expr Expr' and 'MkMul Expr Expr', respectively.

The "subtype" is the thing that bothers me. Not in Haskell, but in your 
Aldor code on
http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes

You define a domain

  MkInt(Z:IntegerNumberSystem): ExprCat == add ...

and then you use it in

Expr: ExprCat == add {
    Rep == Union(Mkint:MkInt(Integer), ...);
    ...
}

I don't think that construction qualifies MkInt to count as a subtype of 
Expr. Note that the representations of MkInt and Expr are different.

http://aldor.org/docs/HTML/chap7.html#5
(Although I find that section not very illuminating w.r.t. domains.)


Ralf