Re: [Axiom-developer] Re: fixing SPAD

[Martin Rubey]

Waldek Hebisch <address@hidden> 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