Re: Spad and inductive types

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