Re: [Axiom-mail] Spad and inductive types

[Bill Page]

Quoting Ralf Hemmecke <address@hidden>:

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

I understand your point. For me it is still a little mysterious that
representation is involved here at all since the usual recursive
definition doesn't seem to need it. But you would agree of course
that both Expr and MkInt(Integer) are in ExprCat. The specific
representation of Expr is such that MkInt(Integer) is a subset of
that  Rep (as implemented by 'Union') and 'per' is a natural
isomorhism (Expr can be assigned the property 'canonical' as
defined in Axiom) because the Union is disjoint. So maybe I
should have said that it is a sub-type "up to an isomorphism". 

Another way of saying this is that objects in Expr are such that
their representation is a Union of sub-types of Expr, recursively,
down to MkInt(Integer) which is just represented by Integer. Really
it is not so peculiar to say that an expression should be represented
in terms of it's sub-expressions. Right?

(You see, I am really just trying to convince myself by convincing
you... :-) Thank you for persisting in this discussion. 

Regards,
Bill Page.