Dear haskellers, I suggest you the two notes on the Haskell language: (1) it is desirable to accommodate such features of Aldor language as types as values and dependent types (2) the properties of operations, like associativity, commutativity ..., can be handled by `usual' Haskell, to some extent. (1): As I wrote earlier, Haskell instances cannot model such domains as the residue ring Integer/(n), when n changes dynamically. This is why the BAL library applies the sample argument approach, and this somewhat complicates the program meaning. Now, we observe in the Aldor manual (http:/www.aldor.org), Section 7.8: `` Zmod(n: Integer) : Ring with { if prime? n then Field; } == Integer add { if prime? n then {inv (x: %) : % == ...} } Z_n, the domain of integers modulo n, is always a Ring. However, if n is prime, then Z_n is also a Field, meaning that it should provide a multiplicative inverse for nonzero values. In an `add' expression, a definition which appears in the consequence of an `if' expression is said to be a conditional definition ... '' But Aldor is non-functional, strict, has a bit of `garbage' in the language, has only one implementation, and this one is not free-with-source. Also I am not sure that the above example will really work in the existing Aldor implementation. Further, there exists a fully commercial Axiom program, which can be considered as a large nonstandard algebraic library for Aldor. This library is certain recommendation for the language. It will be good for Haskell, or any language of its type, to extend and drift towards Aldor, but with preserving functionality and elegance. I always thought (naively) that `unsolvability' of types is a fiction. Typically, types and instances resolve at the run-time. But the compiler has to try each time to resolve at compile time as much as possible. (2) I wrote in the BAL paper that meaningful standard algebraic categories (classes) may, in principle, help the compiler to optimize programs using the properties related to the category names (associativity, commutativity ...). On the other hand, people write now and then, that they consider such possible properties only as intended, saying that the language does not provide room for their explicit usage (the latter was also said by the referee of this paper). It occurs to me now that there may be certain misunderstanding. I kept in mind implicitly that as soon as these categories enter a library standard their names can also be added to the _key words of a language_. In this way the compiler is enabled to use the relevant properties. There remains a question of expressions like _|_ + 1 === 1 + _|_, but this is another matter, maybe, a matter of flags for the compiler and language version. Regards, ----------------- Serge Mechveliani mechvel@botik.ru
"S" == S D Mechveliani <mechvel@math.botik.ru> writes:
Dear haskellers, I suggest you the two notes on the Haskell language:
(1) it is desirable to accommodate such features of Aldor language as types as values and dependent types
You should take a look at Lennart Augustsson's Cayenne: http://www.cs.chalmers.se/~augustss/cayenne/index.html Quoting (most of) that web page: Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. There are very few building blocks in the language, but a lot of "syntactic sugar" to make it more readable. There is no separate module language in Cayenne since the dependent types allow the normal expression language to be used at the module level as well. The design of Cayenne has been heavily influenced by Haskell and constructive type theory and with some things borrowed from Java. The drawback of such a powerful type system is that the type checking becomes undecidable. In the fullness of time, it'd be useful to hear back from you: What parts of Cayenne (that Haskell lacks) are useful for your system? Which parts are a problem? Which parts are of no use for what you're trying to do? -- Alastair Reid reid@cs.utah.edu http://www.cs.utah.edu/~reid/
On Thu, Aug 23, 2001 at 03:02:28PM +0400, S.D.Mechveliani wrote:
(1): As I wrote earlier, Haskell instances cannot model such domains as the residue ring Integer/(n), when n changes dynamically. This is why the BAL library applies the sample argument approach, and this somewhat complicates the program meaning.
Now, we observe in the Aldor manual (http:/www.aldor.org), Section 7.8: `` Zmod(n: Integer) : Ring with { if prime? n then Field; } == Integer add { if prime? n then {inv (x: %) : % == ...} }
Z_n, the domain of integers modulo n, is always a Ring. However, if n is prime, then Z_n is also a Field, meaning that it should provide a multiplicative inverse for nonzero values. In an `add' expression, a definition which appears in the consequence of an `if' expression is said to be a conditional definition ... ''
Z_n indeed sometimes supports additional operations. But how is the user expected to use these operations in a type-safe, statically checked way? Any use of 'inv' for Z_n will necessarily involve a run-time check on n to see whether it is prime. In the context of a statically checked language like Haskell, you could easily arrange to have a function that (a) checks if the modulus is prime and (b) if so, returns a corresponding element of a type that supports the new operations. [assuming you only want 'inv' to be defined for prime moduli, which is not 100% clear.] I'm sure there are cases where algorithms are more efficient when n is a prime, but again, this can (and should) be special cased.
(2) I wrote in the BAL paper that meaningful standard algebraic categories (classes) may, in principle, help the compiler to optimize programs using the properties related to the category names (associativity, commutativity ...). On the other hand, people write now and then, that they consider such possible properties only as intended, saying that the language does not provide room for their explicit usage (the latter was also said by the referee of this paper).
It occurs to me now that there may be certain misunderstanding. I kept in mind implicitly that as soon as these categories enter a library standard their names can also be added to the _key words of a language_. In this way the compiler is enabled to use the relevant properties. There remains a question of expressions like _|_ + 1 === 1 + _|_, but this is another matter, maybe, a matter of flags for the compiler and language version.
One question I have here is, how much are compilers prepared to take advantage of such knowledge? (Also, does it really belong in the compiler? In, e.g., FFTW, all this is optimized by a user program rather than the compiler.) I'm slightly skeptical: it's not entirely obvious how to take proper advantage of commutativity/associativity, and this seems like something I'd want to program directly rather than trust the compiler to do. But I haven't thought about this much; other opinions? Best, Dylan Thurston
participants (3)
-
Alastair David Reid -
Dylan Thurston -
S.D.Mechveliani