- Haskell - Haskell.org

Aldor, Cayenne
by S.D.Mechveliani 27 Aug '01

27 Aug '01

Lennart Augustsson responded recently about Aldor and Cayenne systems and on the possibility of proofs in these languages. Aldor www page shows the following among other Projects: > Mathematical libraries > * Atypical > Authors: Simon Thompson, James Beaumont, John Shackell, Leonid > Timochouk > The aim of the project is to integrate into Aldor a capability > for reasoning. The logic is embedded into the types of Aldor by > means of a modified version of Aldor's dependent types. > [..] This looks similar to what was being developed with Cayenne. ----------------- Serge Mechveliani mechvel(a)botik.ru

2 1

Re: 2 points about language
by Marcin 'Qrczak' Kowalczyk 24 Aug '01

24 Aug '01

Thu, 23 Aug 2001 15:02:28 +0400, S.D.Mechveliani <mechvel(a)math.botik.ru> pisze: > 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 ...). How the compiler could take advantage of them? -- __("< Marcin Kowalczyk * qrczak(a)knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK

3 2

Re: 2 points on language. Continuing
by cwitty＠newtonlabs.com 24 Aug '01

24 Aug '01

"D. Tweed" <tweed(a)cs.bris.ac.uk> writes: > On a purely pragmatic note ( :-) ) these optimisations can't necessarily > be safely used in three of the four most common cases, namely Int, Float > and Double because of the restricted range of intermediates. While the programmer can't necessarily change ((p-q)+p) to (2*p-q) in the case of Int, the compiler usually can. The compiler can know that on the target machine, Int operations wrap on overflow in the typical way, in which case that's an entirely safe optimization. By the way, are there any Haskell systems where Int does not wrap on overflow? Carl Witty

1 0

Aldor, Cayenne
by S.D.Mechveliani 24 Aug '01

24 Aug '01

To my >> (1) it is desirable to accommodate such features of Aldor language >> as types as values and dependent types Alastair David Reid <reid(a)cs.utah.edu> writes > You should take a look at Lennart Augustsson's Cayenne: > > http://www.cs.chalmers.se/~augustss/cayenne/index.html > > > 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? First, download Aldor. It says it is coming within several weeks, but it is also available (as commercial) from-within Axiom. And try to program in Aldor and in Cayenne the above example with Zmod(n), or similar, compute something for such domain, try other simple mathematical examples, and see, which programs _look more natural_ and which of them fail. Aldor has a large non-standard library - Axiom. Probably, this can be considered as certain guarantee for Aldor fitness. Cayenne has not such confirmation. After I reach Aldor, I could try to provide you with examples - if you ask of this. Year or two ago I dealt with Cayenne. Sent a couple of questions and notes. Then Cayenne people silenced. Probably, got tired to answer to silly newbie's questions (there were 3-4 letters). And I quitted, because was not able to work with this version of program. It behaved so, that I doubted whether it is going to grow into a needed tool. Regards, ----------------- Serge Mechveliani mechvel(a)botik.ru

2 1

2 points on language. Continuing
by S.D.Mechveliani 24 Aug '01

24 Aug '01

To my recent message >> (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 ...). >> [..] >> 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. Dylan Thurston <dpt(a)math.harvard.edu> responds on 23 Aug 2001 > 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? I am skeptical too. Anyway, if a compiler `knows' the word CommutativeRing, knows that by definition, CommutativeRing requires associativity, commutativity ..., observes the instance CommutativeRing T for some type T in some program, sees further expr = (2*a + b) - (a+a) :: T and sees the language version (compiler) flag -fignore-bottom, (something of this sort) then, has it right to convert expr --> b :: T ? To my mind, there is something more in this than intension. In practice, the users do not write explicitly such expressions as expr. But they write them implicitly, by applying functions in special cases, for example, one has f(x,y) and applies f(x,2*x) ... I do not ask compilers to exploit now this possibility. Only noted that a meaningful category organization provides, in principle, room for such optimization. Am I missing something? For I can mistake. Further, to my >> (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 ... >> '' Dylan Thurston <dpt(a)math.harvard.edu> writes > 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. > [..] I believe, Aldor checks some types at run-time. And it has types as values. In fact, the above Zmod is a _function_ that takes values in a type called Ring. Each value Zmod(n) is a domain (abstract data type) of type Ring. Regards, ----------------- Serge Mechveliani mechvel(a)botik.ru

4 3

2 points on language
by S.D.Mechveliani 24 Aug '01

24 Aug '01

To my > Anyway, if a compiler `knows' the word CommutativeRing, > [..] > expr = (2*a + b) - (a+a) :: T > > and sees the language version (compiler) flag -fignore-bottom, > (something of this sort) then, has it right to convert > > expr --> b :: T > ? > [..] D. Tweed <tweed(a)compsci.bristol.ac.uk> writes > On a purely pragmatic note ( :-) ) these optimisations can't necessarily > be safely used in three of the four most common cases, namely Int, Float > and Double because of the restricted range of intermediates. > [..] Int, Float, Double are not supposed to be provided with the CommutativeRing instance. And most common cases are, to my mind, different: Integer, Rational, (Integer, Rational), Polynomial Integer ... Regards, ----------------- Serge Mechveliani mechvel(a)botik.ru

1 0

MTV'02: Call for Papers
by Miroslav Velev 24 Aug '01

24 Aug '01

Microprocessor Test and Verification (MTV'02) January 21-22, 2002, Austin, Texas, USA: http://ece.tamu.edu/MTV/ Deadline for submission of abstracts: October 26, 2001 P.S. Note the special topic on optimizing SAT procedures for application to testing and formal verification.

1 0

RE: ghc on win2k ...
by Simon Peyton-Jones 24 Aug '01

24 Aug '01

| I think you need cygwin to install/run it. | | >Has anyone gotten ghc operative over win2k? I couldnt even get | >the v4.08 | >installshield to work for me (it installed fine but then ghc | >just wouldnt | >do anything, not even an error report). No longer! You don't need cygwin, or indeed *anything*. Just install GHC and away you go. (On the other hand, if you *do* have cygwin, GHC won't intefere with it.) Nevertheless, you have good reason to not know this: it's not on GHC's web page. Only readers of the Haskell list will have seen Reuben's announcement (below). We expect to make a new release of GHC, 5.02, at the end of next week, just before ICFP. It fixes many bugs in the release below -- but none the less, the one below is fine for most purposes. Simon ========================================= I've updated the test Windows InstallShield of GHCi 5.01 available from http://www.haskell.org/ghc/dist/5.00.2/ghc-5-01.exe (There's no link to it on the web site) In case you missed the previous announcement, this is a test release, but seems fairly stable (I use it all the time). It has the following features: * GHCi: now you can use GHC interpretively under Windows. You can just run the InstallShield, and double-click on GHCi to get going. * Complete install: everything you need to use GHC is included; Cygwin is no longer required; also, unlike recent 4.08.2 releases, it doesn't interfere with any Cygwin installation you may already have Changes from the previous test release, "Zarjaz": * Now installs in Program Files by default (supports paths containing spaces). * Installs the profiling libraries and imports (the previous test release included them, but for mysterious reasons they weren't actually installed). Also note that as one user found, the supplied gcc doesn't like identifiers containing top-bit-set characters, so if you want to use them you must use the native code generator.

1 0

2 points about language
by S.D.Mechveliani 23 Aug '01

23 Aug '01

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(a)botik.ru

3 2

RE: ghc on win2k ...
by Konst Sushenko 23 Aug '01

23 Aug '01

I think you need cygwin to install/run it. >-----Original Message----- >From: Amit Garg [mailto:amitji@cs.utexas.edu] >Sent: Thursday, August 23, 2001 1:38 PM >To: haskell(a)haskell.org >Subject: ghc on win2k ... > > >Hi. > >Has anyone gotten ghc operative over win2k? I couldnt even get >the v4.08 >installshield to work for me (it installed fine but then ghc >just wouldnt >do anything, not even an error report). > >Thanks for any help on this. >-Amit. > >------------------------------------------------------------------- >Amit Garg | Office: 3.108 Taylor Hall >Graduate Student | Phone : (512) 232-7869 >Computer Sciences | Res : 2910 Medical Arts #304 >University of Texas at Austin | Phone : (512) 482-8329 > Homepage: http://www.cs.utexas.edu/~amitji >------------------------------------------------------------------- > > > >_______________________________________________ >Haskell mailing list >Haskell(a)haskell.org >http://www.haskell.org/mailman/listinfo/haskell >

1 0