Ralf Hemmecke wrote:
>
> > 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
>
X makes no sense above, because IntegerMod has 'foo' as an export.
You probably mean:
x := foo()$Foo(10000)
y := foo()$Foo(10000)
^^^^^
or some other fixed number.
> 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.
Yes. Of course, I would like to forbid 'random' but I am
affraid it is not possible in general without also forbiding
functions which non-type arguments to types useful. More
precisely, it is user responsiblity to ensure that what they
use is true function and not someting with state-dependent
behaviour. The compiler could catch some obvious violations,
(like your random) and could verify some simple cases, but
in general it is up to user.
Why I do not want to forbid functions. Actually the
DirectProduct case is already an example: DirectProduct
fixes size of the product. Without fixed size all
operations would have to check that size matches.
But sometimes you have slightly more complicated
situations. In case of DMP number of variables
much match size of the product. For DirectProduct
one of natural operation is concatention, but
this takes arguments of size n and m and produces
result of size n + m. For kroneckerProduct of
matrices we need mutiplication on sizes. Once
you allow addition and mutiplication it is very
unnatural to reject polynomials.
To say it in different words: without functions in
type parameters it is impossible to provide various
interesing operation for fixed size domains, so
you are forced to use arbitrary size domain and
check sizes at runtime. Of course, if type
parameters are given by functions you can finish
typechecking only at runtime. But IMHO it still
has advanteges:
- some common cases can be checked at compile time
(by comparing parse trees of expressions)
- even if you need runtime checking (not implemented
in current compiler) checking in types should be
more efficient than checking in each operation and
checks in types can be automatically generated by
compiler, while for arbitrary sized domains programmer
need to insert checks by hand (and may forget some...).
--
Waldek Hebisch
[email protected]
--
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.
