Waldek Hebisch <[EMAIL PROTECTED]> writes: > So, to get practical compiler you need to compromise. I see some > possibilities here: > > 1) Defer typechecking to runtime > 2) Reject some programs that are allowed by Barendregt style typesystem > 3) Change point of view: instead of talking about types talk about > predicates (properties) satisfied by values in your program. > Claiming that property holds is a mathematical theorem, so it > requires a proof. And programmer should write the proof together > with the program.
> Doing thins Aldor way should be moderatly hard, say like implementing > extend. It requires some real work and will not happen overnight. OK, so I'll probably have to wait for a reasonably free Aldor compiler... :-( > Doing Barenrdregt style typesystem with arbitrary predicates? Well, > this is a research problem. I guess we should forget about that one for the moment :-) > I think that runtime checking idea is to allow Complex F, but when one uses > it as a Field check at runtime if it is ineded a Field (and signal error if > not). I suspect that Spad is doing this already, but only with conditions > which it allows. Quite right, this is nearly a workaround: in every function in Complex depending on Complex F being a field we could check whether it really is. This doesn't trap usage outside of Complex F, though - unless one uses one of the "Field" functions. It's good enough, given that we do not have a free Aldor, I'd say. Martin _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
