I do not understand your objection to the use of a function here. It
seems to me that the type is "constant in context" as required for
compilation of static types in both Axiom and Aldor - even if the
function on whose result the type depends behaves
non-deterministically. There seems nothing remarkable about this. It
does not somehow make the type language "non-functional".
Let me illustrate the issue.
X ==> IntegerMod(random n)
Foo(n: Integer): with
foo: () -> X
== add
foo(): X == 1$X
I've deliberately used a macro for X. So we have in fact 3 places where
random might or might not be called. In a functional context, the X in
all places would be identical, so there would not be an issue and a type
check can be done on purely syntactical grounds.
If it's not functional, then it is not even clear whether Foo(..)
actually implements the function it exports. Not even is it clear
whether the type of 1$X is what is expected on the lhs of == in the add
part.
And suppose we accept that the code above should compile.
Now we compute
x := foo()$X
y := foo()$X
Should I be able to add x and y or will they have different type due to
different invocations of random?
As far as I understand, Aldor leaves the latter case unspecified, since
it doesn't say how often the type X in a "type context" is evaluated.
http://www.aldor.org/docs/HTML/chap7.html#3
I'm not an expert in these things, but I somehow fear, dependent types
with executed functions in their arguments defeats the "static type"
property.
Ralf
--
You received this message because you are subscribed to the Google Groups "FriCAS -
computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
