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
_______________________________________________
Axiom-mail mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-mail
