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