Paper announcement ------------------ The file http://www.botik.ru/pub/local/Mechveliani/basAlgPropos/haskellInCA1.ps.zip contains more expanded explanations on the BAL (Basic Algebra Library) project (previous variant was haskellInCA.ps.zip). My real intention in whole this line of business was always not just to propose a standard but rather to discuss and to find, what may be an appropriate way to program mathematics in Haskell. The matter was always in parametric domains ... Whoever tried to program real CA in Haskell, would agree that such a problem exists. ----------------- Serge Mechveliani mechvel@botik.ru
Serge Mechveliani :
Paper announcement ------------------
The file http://www.botik.ru/pub/local/Mechveliani/basAlgPropos/haskellInCA1.ps.zip
contains more expanded explanations on the BAL (Basic Algebra Library) project (previous variant was haskellInCA.ps.zip).
My real intention in whole this line of business was always not just to propose a standard but rather to discuss and to find, what may be an appropriate way to program mathematics in Haskell. The matter was always in parametric domains ... Whoever tried to program real CA in Haskell, would agree that such a problem exists.
Absolutely. The point is that this seems - for various, perfectly understandable reasons - not to be the priority of the implementors. Graphics/imagery neither. Nor hard numeric work (efficient, easy to manipulate arrays). And now I will say something horrible. Despite my extremely deep respect for all people contributing to Haskell, despite my love for the language etc. I begin to suspect that it has been standardized too early, and if we (Sergey, other people interested in math, as Dylan Thurston, myself, etc., as well as people who want to do *serious* graphics in a functional way) want an adapted functional language, either we will have to wait quite long, or perhaps it is the time to invent another language, with a more dynamic type system, with intrinsic graphic utilities, and other goodies. For the moment - this is my personal viewpoint - it might be better to write concrete applications, and papers describing those applications. Then we shall perhaps know better what kind of structures, algorithms, representations, genericities, etc. we REALLY need for practical purposes. Anyway, Sergey did a formidable work, and this should be acknowledged even by those who on this list criticized his presentation. Thanks. Jerzy Karczmarczuk Caen, France
On Tue, May 15, 2001 at 06:33:41PM +0200, Jerzy Karczmarczuk wrote:
Serge Mechveliani :
... My real intention in whole this line of business was always not just to propose a standard but rather to discuss and to find, what may be an appropriate way to program mathematics in Haskell. The matter was always in parametric domains ... Whoever tried to program real CA in Haskell, would agree that such a problem exists.
Can you be more precise what the problem is? One problem I see is that referred to in Section 3 of the paper: you really need types that depend on parameters (in particular, integer parameters). This is, indeed, a problem--currently, you have to do runtime checks. Full-fledged dependent types � la Cayenne are undecidable, but there are weaker variants that are likely to be good enough.
The point is that this seems - for various, perfectly understandable reasons - not to be the priority of the implementors. Graphics/imagery neither. Nor hard numeric work (efficient, easy to manipulate arrays).
If I understand correctly, Marcin Kowalczyk is working on exactly this last point...
Despite my extremely deep respect for all people contributing to Haskell, despite my love for the language etc. I begin to suspect that it has been standardized too early, and if we [...] want an adapted functional language, either we will have to wait quite long, or perhaps it is the time to invent another language, with a more dynamic type system, with intrinsic graphic utilities, and other goodies.
For myself, I don't see a problem here. For "intrinsic graphic utilities", someone has to write the graphic libraries. (You don't mean they should be built into the language, do you?) The type system is about as strong as anyone knows how to make a static type system; and it's not too hard to fall back on run-time type checking when necessary (as Sergey does in BAL).
Anyway, Sergey did a formidable work, and this should be acknowledged even by those who on this list criticized his presentation. Thanks.
Yes, absolutely. I think perhaps some things could be done better (for instance, I see that all Sergey's classes derive from Eq, which is one of my principal complaints with the Haskell 98 classes), but I appreciate the work and want to study it more. Best, Dylan Thurston
Tue, 15 May 2001 21:14:02 +0300, Dylan Thurston <dpt@math.harvard.edu> pisze:
Nor hard numeric work (efficient, easy to manipulate arrays).
If I understand correctly, Marcin Kowalczyk is working on exactly this last point...
Well, I improved efficiency of ghc's arrays by removing various unnecessary overheads and I'm working on a generic interface of collections, but I don't have any deeper plans about arrays. What should be improved compared to existing STUArray Int Double and similar? -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
On 15 May 2001, Marcin 'Qrczak' Kowalczyk wrote:
Tue, 15 May 2001 21:14:02 +0300, Dylan Thurston <dpt@math.harvard.edu> pisze:
Nor hard numeric work (efficient, easy to manipulate arrays).
If I understand correctly, Marcin Kowalczyk is working on exactly this last point...
Well, I improved efficiency of ghc's arrays by removing various unnecessary overheads and I'm working on a generic interface of collections, but I don't have any deeper plans about arrays.
What should be improved compared to existing STUArray Int Double and similar?
QRCZAK
A simple standard proposal, not using ST and multiparameter type classes, so that it would be possible to implement it in other compilers (namely nhc), would be a great improvement for me. Wojciech Moczydlowski, Jr
On 15-May-2001, Wojciech Moczydlowski, Jr <khaliff@astercity.net> wrote:
On 15 May 2001, Marcin 'Qrczak' Kowalczyk wrote:
What should be improved compared to existing STUArray Int Double and similar?
A simple standard proposal, not using ST and multiparameter type classes, so that it would be possible to implement it in other compilers (namely nhc), would be a great improvement for me.
I think multiparameter type classes or other extensions to Haskell 98 are really needed to solve these kinds of problems in a simple and elegant way. The right solution, IMHO, is to extend nhc and other Haskell compilers to support multiparameter type classes, not to try to shoehorn things that don't fit into Haskell 98. -- Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit | of excellence is a lethal habit" WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
On Wed, 16 May 2001, Fergus Henderson wrote:
On 15-May-2001, Wojciech Moczydlowski, Jr <khaliff@astercity.net> wrote:
On 15 May 2001, Marcin 'Qrczak' Kowalczyk wrote:
What should be improved compared to existing STUArray Int Double and similar?
A simple standard proposal, not using ST and multiparameter type classes, so that it would be possible to implement it in other compilers (namely nhc), would be a great improvement for me.
I think multiparameter type classes or other extensions to Haskell 98 are really needed to solve these kinds of problems in a simple and elegant way.
The right solution, IMHO, is to extend nhc and other Haskell compilers to support multiparameter type classes, not to try to shoehorn things that don't fit into Haskell 98.
Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit
I don't like the idea of a program working which compiles only under compilers which have certain language extensions built in. If I understand things correctly, there is a list of language extensions (FFI for example), which has been accepted by all Haskell compilers developers. If multiparameter type classes were in that list, I would agree. Besides, MArray.lhs uses ST and ST requires not only multiparameter type classes, but also explicit universal quantification. I don't like ST and the idea that someone who wants to use arrays outside of IO has to use ST gives me creeps. By the way, I'm really surprised by the lack of time complexity information in MArray. I mean, that's the most important thing in arrays - that one can update/read a data in O(1). Wojciech Moczydlowski, Jr
On Tue, May 15, 2001 at 09:14:02PM +0300, Dylan Thurston wrote:
On Tue, May 15, 2001 at 06:33:41PM +0200, Jerzy Karczmarczuk wrote:
Serge Mechveliani :
... The matter was always in parametric domains ... Whoever tried to program real CA in Haskell, would agree that such a problem exists.
Can you be more precise what the problem is? One problem I see is that referred to in Section 3 of the paper: you really need types that depend on parameters (in particular, integer parameters). This is, indeed, a problem--currently, you have to do runtime checks.
Full-fledged dependent types à la Cayenne are undecidable, but there are weaker variants that are likely to be good enough.
What are the weaker variants? Do you know some references? Are they still decidable? That surprises me. If you allow integer arithmetic you can do already all computations (Church). -- Stefan Karrmann
On Wed, 16 May 2001, Stefan Karrmann wrote:
On Tue, May 15, 2001 at 09:14:02PM +0300, Dylan Thurston wrote:
On Tue, May 15, 2001 at 06:33:41PM +0200, Jerzy Karczmarczuk wrote:
Serge Mechveliani :
... The matter was always in parametric domains ... Whoever tried to program real CA in Haskell, would agree that such a problem exists.
Can you be more precise what the problem is? One problem I see is that referred to in Section 3 of the paper: you really need types that depend on parameters (in particular, integer parameters). This is, indeed, a problem--currently, you have to do runtime checks.
Full-fledged dependent types � la Cayenne are undecidable, but there are weaker variants that are likely to be good enough.
What are the weaker variants? Do you know some references? Are they still decidable? That surprises me. If you allow integer arithmetic you can do already all computations (Church).
The idea that `dependent types are undecidable' is a popular but understandable misconception arising from a particular design decision in a particular system---Cayenne. Dependent types as found in proof systems such as Coq and Lego do have decidable typechecking: programs may only use structural recursion, and hence all the evaluation which takes place during typechecking is guaranteed to terminate. However, in order to support real programming, Cayenne allows general recursion: as it makes no distinction between the programs which are executed at compile-time and those only executed at run-time, undecidability creeps in. Understandably, neither horn of this dilemma is particularly attractive to programmers who want to combine flexibility at run-time with a genuinely static notion of typechecking. (Of course, post-98 Haskell with certain type class options selected has a type-level language containing non-terminating programs, making typechecking undecidable for exactly the same reason as in Cayenne.) However, there is a middle way: we can distinguish compile-time programs from run-time programs and restrict the former to the structurally recursive fragment, leaving general recursion available in the latter. In this way, all the programs we know and love remain available at run-time, whilst the type system acquires a large yet decidable extension to its expressive power. The key is the application rule, for it is here that programs leak into types. G |- f :: all x::S . T G |- s :: S -------------------------------------- G |- f s :: [s/x]T If s is potentially non-terminating, typechecking becomes undecidable: [s/x]T may not have a normal form. Now let's separate compile-time programs (typed with `|-') from run-time programs (typed with `/-', say). Restricting the compile-time language to structural recursion, the above rule poses no threat. We can add G |- t :: T ------------- (a compile-time program is a run-time program) G /- t :: T G /- f :: all x::S . T G |- s :: S -------------------------------------- x free in T G /- f s :: [s/x]T G /- f :: S -> T G /- s :: S -------------------------------- (S -> T abbreviates all x::S. T G /- f s :: T when x is not free in T) G /- f :: T -> T -------------------- (fixpoint) G /- Y f :: T -> T compile-time structurally recursive programs, extending with general recursion only at run-time. Typechecking is thus decidable, with all your old code intact. Structural recursion is a syntactically checkable notion which allows a large, but obviously not complete language of terminating programs to be recognized as such. How large? Well, first-order unification is structurally recursive, and so is normalization for simply-typed lambda-calculus. As decidable type systems go, this one is better than a poke in the eye. I respectfully suggest that dependent types are worth a second look. Cheers Conor
C T McBride schrieb folgendes am Wed, May 16, 2001 at 01:03:25PM +0100:
On Wed, 16 May 2001, Stefan Karrmann wrote:
On Tue, May 15, 2001 at 09:14:02PM +0300, Dylan Thurston wrote:
On Tue, May 15, 2001 at 06:33:41PM +0200, Jerzy Karczmarczuk wrote: ... you really need types that depend on parameters (in particular, integer parameters). This is, indeed, a problem--currently, you have to do runtime checks.
Full-fledged dependent types à la Cayenne are undecidable, but there are weaker variants that are likely to be good enough.
What are the weaker variants? Do you know some references? Are they still decidable? That surprises me. If you allow integer arithmetic you can do already all computations (Church).
The idea that `dependent types are undecidable' is a popular but understandable misconception arising from a particular design decision in a particular system---Cayenne.
Dependent types as found in proof systems such as Coq and Lego do have decidable typechecking: programs may only use structural recursion, and hence all the evaluation which takes place during typechecking is guaranteed to terminate. However, in order to support real programming, Cayenne allows general recursion: as it makes no distinction between the programs which are executed at compile-time and those only executed at run-time, undecidability creeps in. Understandably, neither horn of this dilemma is particularly attractive to programmers who want to combine flexibility at run-time with a genuinely static notion of typechecking.
With constructor type we can do dimension checking, as shown earlier on this list. Can't we check in a similiar way an integer paramter? But is this general enough? You may compute some integer n and then do some calculations in Z/n. How can this be done? Do you need to do the calculation only with structural recursion?
(Of course, post-98 Haskell with certain type class options selected has a type-level language containing non-terminating programs, making typechecking undecidable for exactly the same reason as in Cayenne.)
If possibly non-terminating type analysis creeps into Haskell, why don't we choose the Cayenne style?
However, there is a middle way: we can distinguish compile-time programs from run-time programs and restrict the former to the structurally recursive fragment, leaving general recursion available in the latter.
Is there any (syntactical) proposal somewhere? -- Stefan Karrmann
Dylan Thurston cites :
... if we [...] want an adapted functional language, either we will have to wait quite long, or perhaps it is the time to invent another language, with a more dynamic type system, with intrinsic graphic utilities, and other goodies.
For myself, I don't see a problem here. For "intrinsic graphic utilities", someone has to write the graphic libraries. (You don't mean they should be built into the language, do you?) The type system is about as strong as anyone knows how to make a static type system; and it's not too hard to fall back on run-time type checking when necessary (as Sergey does in BAL).
Look what happens with functional graphics. Dozens of really good papers, I could mention many names here. (Some bad papers as well, some people formalize and formalize without any contact with reality...) So, one may want to check all this. You take Alastair Reid's Hugs graphic library, and you discover that: The IO monadic framework is so rigid that you program imperatively, and after a few minutes you ask yourself why for goodness sake do it in Haskell? The programming style is not functional at all. In C++ or Java you do it faster and without more pain. (From the syntactic point of view this is a step backward wrt. the Henderson's book showing how to compose graphics objects in Scheme...) You can't draw individual pixels. (OK, lines with length 1 work). So, impossible to create complicated textures. Impossible to generate complex geometric models rendered pixel by pixel. Try, please, to fill a rectangle with a texture. The graphic updates by the Draw monad will explode the memory quite fast. No relation between bitmaps and arrays. (If the bitmaps work at all.) Similar problems are visible in the Clean library. Both, Hugs and Clean libraries have been added ad hoc to the language environment. Plenty of horrible Windows quirks squeezed into a functional interface. What I mean by *intrinsic* graphics: The graphic primitives should be WELL integrated with the underlying virtual machine. No silly "external" bitmaps impossible to garbage-collect, and impossible to process (thresholding, transfer curves, algebra). No pixels drawn using "line". True, fast access to primitive data. Efficient 2dim and 3dim vectors, with optimized processing thereof. Mapped arrays, easy passage from screen to bitmap DContext. Possibility to have decent functional binding of OpenGL calls. And mind you, OpenGL is not just a bunch of graphic calls, but a "state machine". Some graphic data must be processed by strict algorithms, laziness may deteriorate the efficiency considerably. No, this is not JUST the problem of external libraries. It would be, if the language were at the level of, say, C. But if the runtime is complex with plenty of dynamical data to protect and to recover, and if the internal control transfer is non-trivial (continuations, private stacks, etc.) then adding efficient and powerful graphics <<ex post>> is not easy. === In my opinion one of best decisions taken by the Rice mafia was to base the DrScheme interface on WxWindows. What a pleasure to produce graphic exercises for students under Linux, test it under Solaris, and work with them under W2000 without a single incompatibility. I am still unhappy, because it is too slow to generate textures at a respectable rate, but no comparison with Hugs which bombs. But perhaps the next version (if ...) will optimize a few things. === And, if you want to have *interactive* graphics, then obviously you must provide some kind of event-processing functionalities. Is this just an external library question? ****************************** No place to discuss type systems here, but "falling back" into run-time checks is not enough in this context, we know that we need a genuine object-oriented genericity for graphical entities. Perhaps even with multiple inheritance or the java-style "interfaces". So, again, a bit more than just "graphic library". Jerzy Karczmarczuk Caen, France
Jerzy Karczmarczuk writes: [Some interesting points on functional wrappings of graphics libraries] Has anyone considered writing a haskell wrapper for SDL - Simple Directmedia Layer at http://www.libsdl.org ? This is a cross platform library intended for writing games, and aims for a high performance, low level API. It would be interesting to see how clean a functional API could be built around such an imperative framework. Tim
Timothy Docker wrote: for info, there is a gui lib on top of sdl (then portable to linux, win) at http://www.bms-austria.com/projects/paragui/
Jerzy Karczmarczuk writes:
[Some interesting points on functional wrappings of graphics libraries]
Has anyone considered writing a haskell wrapper for SDL - Simple Directmedia Layer at http://www.libsdl.org ?
This is a cross platform library intended for writing games, and aims for a high performance, low level API. It would be interesting to see how clean a functional API could be built around such an imperative framework.
Tim
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Tue, 15 May 2001 16:10:20 +0400, S.D.Mechveliani <mechvel@math.botik.ru> pisze:
The matter was always in parametric domains ...
The solution is simple: don't model domains as types. Model them as values (records with operations). Some simple domains can be also modelled as types for convenience. But it doesn't work in general. Similarly as standard sort :: (Ord a) => [a] -> [a] is not as expressive as soryBy :: (a -> a -> Ordering) -> [a] -> [a] even though it's more convenient in case it works. It doesn't work when various instances of the same kind of algebraic structure over the same carrier set are considered. And it doesn't work when a domain should be parametrized by something which is hard to express by a type. And it constrains programs which want to choose the domain dynamically. Carrier sets are modelled as types, OK. But it won't work for all algebraic structures. About program transformation possibility: I don't see how it would be applied in practice. There is no use of associativity of (+) for the compiler. It can do many optimizations, but it won't rewrite x+(y+z) to (x+y)+z nor vice versa. Sample arguments are ugly, almost always unnecessary, and constrain interfaces (functions like 'sum :: Num a => [a] -> a' would have to have a different intreface). They are a solution to a wrong problem: some domains should not have been modelled as types in the first place. Algebraic operations don't belong to elements of algebras; they belong to algebras. In simple cases they can be deduced from the types of elements if the given carrier has a reasonable default interpretation of these operations (e.g. (+) on Integers), but it's not general. I don't believe that dependent types would come into Haskell in the near future. And they are unnecessary for the discussed purpose: domains which would require them should not be modelled as types. Don't abuse types to model values. Haskell's types are too static for that. The class hierarchy is unacceptable for me as standard Haskell. It's way too complex. Currently I have to define instances of Eq, Show, Num and Fractional to have field operations. With BAL I would have to define instances of Eq, Show, Set, Additive, AddSemigroup, AddGroup, Multiplicative, MulSemigroup, Ring, CommutativeRing, GCDRing, EuclideanRing, FactorizationRing and Field. They require such things as specifying an arbitrarily chosen set of properties of the domain and partially defined versions of most operations... The hierarchy contains many unnecessary superclass relationships. For example Show, specifying bounds and conversion from 'Expression String' are not necessary for Ord, where your classes artificially require them. There are no class synonyms in Haskell, so classes like OrdAddGroup can't be treated as implicit. Later parts are too heavy for me to understand them well, but I see some ugly points, like abusing Char arguments to virtually extend the function name, or requirement to provide reflection capabilities at the very beginning by every type wanting to use overloading of basic operations, or requirement that the programmer knows more advanced math than should be necessary to use Haskell. I hope that a similar proposal won't go into standard Haskell. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
participants (10)
-
C T McBride -
Dylan Thurston -
Fergus Henderson -
Jerzy Karczmarczuk -
luc -
Marcin 'Qrczak' Kowalczyk -
S.D.Mechveliani -
Stefan Karrmann -
Timothy Docker -
Wojciech Moczydlowski, Jr