"Pervasive support for dependent types"
Posted Tue Mar 25 14:16:38 -0700 2008At
http://lambda-the-ultimate.org/node/2737#comment-40909
Quoting from the summary of Aldor at http://aldor.org
... Pervasive support for dependent types allows static checking of dynamic objects. ...
On Tue, 2008-03-25 12:36 Jim Apple asked:
If I remember correctly, Aldor does not allow Vector(3+4) to be simplified to Vector(7). Is that right?
------
From our discussions during the Aldor Workshop 2007 I believe that Jim is correct. On the other hand I am not sure how such simplifications would add to the expressivity or power of the Aldor language - especially since in general we do not have (cannot have?) a strong definition of equality between types.
Perhaps some other Aldor developers would care to comment?
I am not an Aldor developer. However, the question is equally valid in Axiom. Jim's example is meant, I believe, to show static checking limits the power of the language. I can imagine occasions where at code/compile time, where n is not known, there may be need to construct Vector(n+1). I think this is possible in Axiom.
Why is this related to a strong definition of equality between types?
I would think the reason for not allowing Vector(3+4) is to simplify the parser or memory allocation. It may also be similar to requiring the limits of a loop to be constant?
William
In his post: "Should 3+4 = 7?" on
http://lambda-the-ultimate.org/node/2737#comment-40941
Stephen Watt explained the rational for why Vector(3+4) is not equivalent to Vector(7) in Aldor (I agree the same applies to Axiom):
"The other stance that would allow all types to be treated completely uniformly would be to have all type expressions fully evaluate at compile time. I believe this would lead to worse problems however in the Aldor setting. With the heavy use of mutually recursive and dependent types in the library, we could not have separate compilation with static type checking."
So this is not so much a limitation of static type checking as such but rather the way the compiler interacts with the library. The relationship to the definition of equality between types is simply this: that in comparing Vector(3+4) to Vector(7), 3+4 is not evaluated. Syntactically speaking they are not identical and Aldor does not make any attempt to look deeper. So this is a "weaker" sense of equality of types than if the compiler treated '3' and '4' as integers and computed there sum before making the comparison.
Treating an type expression "Vector(n+1)" as a constructor with n a parameter is certainly possible.