Dylan Thurston
On Sat, Apr 08, 2006 at 10:16:53PM +0400, Serge D. Mechveliani wrote:
I think that without dependent types for a Haskell-like language, it is impossible to propose any adequate and in the same time plainly looking algebraic class system.
Agreed. Is there anything really wrong with the Kiselyov-Shan approach to dependent types? Does it look too bizarre?
http://okmij.org/ftp/Haskell/types.html#Prepose http://okmij.org/ftp/Haskell/number-parameterized-types.html
I am out of this field since about 2001. The first paper mentions the foreign function interface, and transmitting integer by means of tricks with types (I recall difficulties with existential types), and so on. It also mentions passing vocabularies (maybe, via foreign interface extension). Of course, if a language extension allows to express the constructs like if isPrime n then (pass inv (the inversion operation) to the vocabulary of (ResidueDomain Integer n), with this implementation ... ) else do not pass it , then this is what is needed: an equivalent of a dynamic conditional instance. In this example, passing inv expresses actially dynamic and conditional definition of the Field instance. Field a <==> (CommutativeRing a, `inv' is in vocabulary of a). In Magma system, and in Aldor, it can be, probably, written plainly. But these systems are not functional, nor lazy, have not pattern matching, etc. Currently I am out of this field, have not time to study all this. For example, if Dylan Thurston tries to implement the Basic Algebra proposal basing on the approach of `configurations' of http://okmij.org/ftp/Haskell/types.html#Prepose, and with the functionality as of the BAL proposal, then we could observe whether the thing looks natural enough. I could also think of doing an attentive investigation on this subject, maybe, together with some qualified people, if I have this project as somehow a visiting research job, and paid. And there is no guarantee that the result occurs positive. ----------------- Serge Mechveliani mechvel@botik.ru