Re: [Haskell-cafe] coding a queue with reactive
One way to think about Reactive's notion of Future is as a single element of an event stream--something that might happen (yielding a value) some time in the future. 'mempty' on futures is a future that never happens, and 'mappend' says to pick the first of two futures to happen. m = k waits for m's future to happen, then passes the result onto k. So my definition of stateMachine says: - Wait for either the future returned by 'run s0' or the first event in the input event stream. - If the future returned by 'run s0' happens first, we have an event instance--return an event whose 'rest of the event stream' is the next state of the state machine - If the future from the input event stream happens first, update the state and continue without spawning an event. - If they happen at the same time, 'run s0' wins (mappend is left-biased) Good luck! -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Vector library
Hi, This is mostly a question for Roman : how do you use your vector library with multi-dimensional arrays ? I mean, the array library from the standard libraries does something more intelligent than the C-like solution with indirections. For instance, it allows you to program a single function that works for any dimensionality of the array. An example where it is useful ? Right : Some time ago I wrote a polynomial system solver for polynomials in Bernstein form. It needs to perform De Casteljau's algorithm to compute the coefficients of the restriction of its argument to a subinterval of [0,1]. The Ix thing (mainly the bounds function) allows for writing only one version of the function for any number of variables (ok, I needed to write another class to tell me there were n variables were when the index was a n-uple, and how to iterate over my data in some dimension between 0 and n-1). I know I could do it with vectors only by wrapping them in another type carrying the bounds information, but isn't there any more elegant way to do it ? Like an optional thing in the vector type, an alternative one, I don't know. Thanks, Pierre Some code example : instance Restrictable (Double,Double,Double,Double,Double,Double,Double,Double) (Int,Int,Int,Int,Int) where restriction (a,b,c,d,e,f,g,h) lower upper= let ((i0,i1,i2,i3,i4),(j0,j1,j2,j3,j4))=bounds lower dd=rangeSize (i4,j4) n0=rangeSize (i0,j0) n1=rangeSize (i1,j1) n2=rangeSize (i2,j2) n3=rangeSize (i3,j3) restr0=restrict 1 (n1*n2*n3) n0 dd a b coefs restr1=restrict n0 (n2*n3) n1 dd c d restr0 restr2=restrict (n0*n1) n3 n2 dd e f restr1 restr3=restrict (n0*n1*n2) 1 n3 dd g h restr2 in something Where restrict is written like : restrict bef aft nv dd a b coefs= let idx i j k d=((i*nv+j)*aft + k)*dd + d in something ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Vector library
On 14 February 2011 10:19, Pierre-Etienne Meunier pierreetienne.meun...@gmail.com wrote: For instance, it allows you to program a single function that works for any dimensionality of the array. I don't know how vector handles it, but you may be interested to look at the repa library (http://hackage.haskell.org/packages/archive/repa/1.1.0.0/doc/html/Data-Array-Repa.html). This lets you write dimensionality-polymorphic functions by using the Shape typeclass: http://hackage.haskell.org/packages/archive/repa/1.1.0.0/doc/html/Data-Array-Repa-Shape.html#t:Shape Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On Sat, 12 Feb 2011 19:38:31 +0530 C K Kashyap ckkash...@gmail.com wrote: Anyway, how can one go about explaining to an imperative programmer with no FP exposure - what aspect of Haskell makes it easy to refactor? Like other people have said, the static type system is a major factor. It's true that Haskell's type system is more advanced than most imperative languages but it's also the often not mentioned that static typing gives a stronger check in a functional language than an imperative ones even in simple cases. This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking. For example, the type signature for a variable swapping procedure in C: void swap(int *a, int *b) This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair: swap :: (Int,Int) - (Int,Int) Now the type checker will reject any implementation that fails to return a pair of results in every case. Of course for a trivial example like swap this is easy to ensure in any imperative language, but for more complex programs it is actually quite common to forget some update some component of the state. BTW, I found this and other interesting reflections on the avantages of FP vs. imperative in Martin Oderski's book Programming in Scala. Best regards, Pedro Vasconcelos ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lhs2tex and line numbers
Hi. How could I convince lhs2tex to add in poly mode line numbers before each code line in code block? A long time ago, I've written some experimental code that achieves line numbering in lhs2tex. I've committed the files to the github repository, so you can have a look at the .fmt file and the demo document in https://github.com/kosmikus/lhs2tex/tree/master/ExtLibrary/lineno HTH, Andres ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Vector library
Pierre-Etienne Meunier wrote: This is mostly a question for Roman : how do you use your vector library with multi-dimensional arrays ? I mean, the array library from the standard libraries does something more intelligent than the C-like solution with indirections. Vector doesn't include any support for multidimensional arrays. This is by design as the library has exactly one purpose: to provide a fast implementation of contiguous, one-dimensional arrays. As you point out, it is well possible to build multidimensional arrays on top of it but that would be a separate library. You might want to take a look at Repa (http://hackage.haskell.org/package/repa) which does exactly that (it sits on top of DPH which sits on top of vector). It also gives you parallelism. FWIW, I don't think we've nailed the right API for multidimensional arrays yet. It's a hard problem. But we are getting there. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is there no splitSeperator function in Data.List
Hi Evan, The reason it's not in Data.List is because there are a bazillion different splits one might want (when I was pondering the issue before Brent released it, I had collected something like 8 different proposed splits), so no agreement could ever be reached. It is curious though that the Python community managed to agree on a single implementation and include that in the standard library… So it is possible :) This is sometimes cited as the advantage of a benevolent dictator-for-life. I remember there was lots of argument when 'join' was added as a string method (vs. should it be a list method). In the end, Guido decided on one and that's what went in. having a dictator is not a necessary prerequisite for the ability to make decisions. It's quite possible to decide controversial matters without a dictator -- say, by letting people vote. Take care, Peter ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is there no splitSeperator function inData.List
On Sun, Feb 13, 2011 at 11:33:16PM -0800, Donn Cave wrote:
It is curious though that the Python community managed to agree on a
single implementation and include that in the standard library
To me, it's more like 2 implementations, overloaded on the same
function name.
Python 2.6.2 (r262:71600, Aug 30 2009, 15:41:32)
[GCC 2.95.3-haiku-090629] on haiku1
Type help, copyright, credits or license for more information.
import string
string.split(' ho ho ')
['ho', 'ho']
string.split(' ho ho ', ' ')
['', 'ho', 'ho', '']
I.e., let the separator parameter default (to whitespace), and you
get what we have with Prelude.words, but specify a split character
and you get a reversible split. It wasn't a new idea, the Bourne
shell for example has a similar dual semantics depending on whether
the separator is white space or not. Somehow doesn't seem right
for Haskell, though.
Agreed, but I don't think that lacking a generic split functionality (as
in reversible split) is also good.
iustin
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
Pedro Vasconcelos wrote: This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking. For example, the type signature for a variable swapping procedure in C: void swap(int *a, int *b) This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair: swap :: (Int,Int) - (Int,Int) This benefit of explicit input and output values can interact nicely with parametric polymorphism: swap :: (a, b) - (b, a) This more general type signature makes sure we are not just returning the input values unswapped. Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On Mon, 14 Feb 2011 12:54:55 +0100 Tillmann Rendel ren...@informatik.uni-marburg.de wrote: This benefit of explicit input and output values can interact nicely with parametric polymorphism: swap :: (a, b) - (b, a) This more general type signature makes sure we are not just returning the input values unswapped. Good point. This is a good reason why it's good practice to look for possiblity of writing more general functions and types even when they end up being used in a single instance. Pedro ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On Mon, Feb 14, 2011 at 12:06 PM, Pedro Vasconcelos p...@dcc.fc.up.pt wrote: On Sat, 12 Feb 2011 19:38:31 +0530 C K Kashyap ckkash...@gmail.com wrote: Anyway, how can one go about explaining to an imperative programmer with no FP exposure - what aspect of Haskell makes it easy to refactor? Like other people have said, the static type system is a major factor. It's true that Haskell's type system is more advanced than most imperative languages but it's also the often not mentioned that static typing gives a stronger check in a functional language than an imperative ones even in simple cases. This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking. For example, the type signature for a variable swapping procedure in C: void swap(int *a, int *b) This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair: swap :: (Int,Int) - (Int,Int) Now the type checker will reject any implementation that fails to return a pair of results in every case. Of course for a trivial example like swap this is easy to ensure in any imperative language, but for more complex programs it is actually quite common to forget some update some component of the state. BTW, I found this and other interesting reflections on the avantages of FP vs. imperative in Martin Oderski's book Programming in Scala. I'm not completely sure, but I suspect another part of it (or maybe I'm just rephrasing what you said?) has to do with the fact that in Haskell, basically everything is an expression. In imperative languages, the code is segragated into statements (which each contain expressions) which are evaluated individually for their side effects. Type checking occurs mainly within statements (in expressions), while between them it is minimal to nonexistent. In Haskell, functions are one big expression -- even imperative code is represented by monadic expressions. If you have a complicated function that transforms lists in some way, and change something, the change has to satisfy the types of not just its immediate environment, or that of the complicated function you're writing, but also everything else in between, with the consequences of the change (and the consequences of the consequences...) being propogated automatically by the type inferencer. (The 'boundaries' so to speak between expressions being defined by where you put explicit type signatures -- calling a function without an explicit signature is similar from the typechecker's point of view to having its contents inlined in the place where it was called. (Modulo things like the monomorphism restriction, it should be equivalent?)) Does this sound roughly correct? Best regards, Pedro Vasconcelos ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Work is punishment for failing to procrastinate effectively. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: FunGEn-0.3 simple 2D game engine released
Hi Andre, good to hear from you. On Feb 13, 2011, at 5:27 PM, Andre Wilson Brotto Furtado wrote: This is great, thanks Simon. I'm currently not involved in any haskell projects anymore, but please do keep the ball rolling for FunGEn. I'm currenty exploring how domain-specific development and software product lines can be streamlined for game development. You can check it out at http://sharpludus.codeplex.com. Volunteers to port such a work to Haskell are welcome. Cool. Thanks, -Simon___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On Mon, 14 Feb 2011 15:07:01 +0100 Gábor Lehel illiss...@gmail.com wrote: I'm not completely sure, but I suspect another part of it (or maybe I'm just rephrasing what you said?) has to do with the fact that in Haskell, basically everything is an expression. Yes, the fact that control statements (e.g. if-then-else) are expressions makes type checking much more effective. However, I think this is somewhat lost when programming imperative code in Haskell using a state or I/O monad (because a monadic type such as IO t does not discriminate what effects might take place, only the result type t). Of course one can use a more specialized monad (such ST for mutable references, etc.). I don't think that my imperative programs are automatically made more correct by writing them as monadic code in Haskell --- only that in Haskell I can opt for the functional style most of the time. BTW (slightly off topic) I found particularly annoying when teaching Python to be forced to use an imperative style (e.g. if-then-else are always statements). Scala is must better in this regard (altought it is not purely functional language); a statement is simply an expression whose return is unit. Pedro ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Unit propagation
This is my last part from a project and I need some help with the following function: If a clause in a propositional formula contains only one literal, then that literal must be true (so that the particular clause can be satisfied). When this happens, we remove the unit clauses (the ones that contain only one literal), all the clauses where the literal appears and also, from the remaining clauses, we delete the negation of the literal (because if P is true, -P will be false). For example, in the formula (P v Q v R) ^ (-P v Q v-R) ^ (P) we have one unit clause (the third clause (P) ). Because this one has to be true for the whole formula to be true we assign True to P and try to find a satisfying assignment for the remaining formula. Finally because -P cannot be true (given the assigned value of P) then the second clause is reduced by eliminating the symbol -P . This simplification results in the revised formula (Q v -R). The resulting simplification can create other unit clauses. For example in the formula (-P v Q) ^ (P) is simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a unit clause which can now also be simplified to give a satisfying assignment to the formula. Your function should apply unit propagation until it can no longer make any further simplifications. Note that if both P and -P are unit clauses then the formula is unsatisfiable. In this case the function type Atom = String type Literal = (Bool,Atom) type Clause = [Literal] type Formula = [Clause] type Model = [(Atom, Bool)] type Node = (Formula, ([Atom], Model)) ropagateUnits :: Formula - Formula propagateUnits = filter.something---here I need help Thanks in advance -- View this message in context: http://haskell.1045720.n5.nabble.com/Unit-propagation-tp3384635p3384635.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why is there no splitSeperator function inData.List
Quoth Peter Simons sim...@cryp.to, ... having a dictator is not a necessary prerequisite for the ability to make decisions. It's quite possible to decide controversial matters without a dictator -- say, by letting people vote. The problem might be slightly miscast here, as an inability to reach a decision in the face of controversy, and overall I don't think you could make much of a case that Python's development is noticeably more decisive. If you really have 8 candidates for the semantics of separator-split, then even if everyone can bring themselves to agree on one, it's still just one, out of 8 missing functions, and it's fairly understandable that this might not be very appealing. Python also - is different in that function semantics can be conveniently overloaded (I forgot the count parameter, I often want that one - split at the first (n - 1) locations and leave the remainder intact) - is different as a general matter of style and niche - doesn't have our division between String and ByteString - makes it harder and more expensive to implement string.split() Anyway, before it gets to the point where the crowds are camping in the city square and demanding a vote, it might be interesting to see where the code comes down on the matter, so I looked at the hackage source I already happen to have at hand, a measly 252 Haskell source files. I found one (1) separator-split implementation. I was surprised at so few, as I've done it myself several times, so maybe I happen to have an unrepresentative sample? Donn ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ghci command line execution
Thomas Davie schrieb: A while ago I remember someone showing me some tool, I *think* ghci that allowed you to pass it a function of type String - String as an input, and have it simply run that function on stdin (presumably using interact) to achieve useful things like this... $ cat myFile.txt | ghci -e 'unlines . zipWith (\x y - show x ++ ++ y) [1..] . lines' Does anyone know what it was that I saw being used here? It must be just 'ghc' not 'ghci' and yes, 'interact' must be called. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Cmdargs and common flags
Hi Magnus, Finally, you can switch to the pure annotations. I will document them shortly and give an example in System.Console.CmdArgs.Implicit, but for now the details can be found at http://hackage.haskell.org/packages/archive/cmdargs/0.6.7/doc/html/System-Console-CmdArgs-Annotate.html I've added more details in: http://hackage.haskell.org/packages/archive/cmdargs/0.6.8/doc/html/System-Console-CmdArgs-Annotate.html http://hackage.haskell.org/packages/archive/cmdargs/0.6.8/doc/html/System-Console-CmdArgs-Implicit.html The first link includes comparisons for pure/impure, and the second gives a set of equivalences for converting between the two forms. Thanks, Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell] Problems with (projects|community).haskell.org
On 10 February 2011 22:03, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote: Also, is there any news yet on a procedure for community members with accounts on projects.haskell.org to get access to them again? My ssh publickey login is no longer being accepted. I had an account mainly for hosting the darcs repo and the website for my project grammar-combinators. The website has been down for a couple of weeks now. Dominique P.S.: This is not a complaint, I'm just hoping for a status update. P.P.S.: Thanks to the people working on fixing this.. Any update on this? Alistair ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On 11-02-12 09:40 PM, Brandon S Allbery KF8NH wrote: Only up to a point. While most of the responses so far focus on the question from one direction, the other is epitomized by a Knuth quote: Beware of bugs in the above code; I have only proved it correct, not tried it. Knuth's definition of proof is of the sketchy kind of the mathematics community, not remotely close to the Coq kind. Even Dijsktra's and Bird's kind offers higher assurance than the traditional mathematician's sketchy kind. There are still gaps, but drastically narrower than Knuth's gaps, and bridgeable with probability arbitrarily close to 1: Possible defects in theorem provers: Use several theorem provers and/or several independent alternative implementations (both alternative software and alternative hardware). Possible deviation of Haskell compilers from your assumed formal semantics of Haskell: Verify the compilers too, or modify the compilers to emit some sort of proof-carrying code. Possible defects in target hardware: The hardware people are way ahead in improving both formal verification and manufacturing processes to reduce defects. When John Harrison ( http://www.cl.cam.ac.uk/~jrh13/ ) has a proof for a floating-point algorithm, I would not dare to apply the Knuth quote on it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unit propagation
On Mon, Feb 14, 2011 at 7:43 AM, PatrickM patrickm7...@yahoo.co.uk wrote: This is my last part from a project and I need some help with the following function: If a clause in a propositional formula contains only one literal, then that literal must be true (so that the particular clause can be satisfied). When this happens, we remove the unit clauses (the ones that contain only one literal), all the clauses where the literal appears and also, from the remaining clauses, we delete the negation of the literal (because if P is true, -P will be false). For example, in the formula (P v Q v R) ^ (-P v Q v-R) ^ (P) we have one unit clause (the third clause (P) ). Because this one has to be true for the whole formula to be true we assign True to P and try to find a satisfying assignment for the remaining formula. Finally because -P cannot be true (given the assigned value of P) then the second clause is reduced by eliminating the symbol -P . This simplification results in the revised formula (Q v -R). The resulting simplification can create other unit clauses. For example in the formula (-P v Q) ^ (P) is simplified to (Q) when the unit clause (P) is propagated. This makes (Q) a unit clause which can now also be simplified to give a satisfying assignment to the formula. Your function should apply unit propagation until it can no longer make any further simplifications. Note that if both P and -P are unit clauses then the formula is unsatisfiable. In this case the function type Atom = String type Literal = (Bool,Atom) type Clause = [Literal] type Formula = [Clause] type Model = [(Atom, Bool)] type Node = (Formula, ([Atom], Model)) ropagateUnits :: Formula - Formula propagateUnits = filter.something---here I need help Thanks in advance Your specification is a bit too much a single pass of filter. You need to collect the atomic clauses, and filter those out of the non-atomic clauses using the semantics you specified: To filter out the atomic clauses, you can use: not_atomic = filter (\not_atomic - (length not_atomic /= 1) But you want to collect the atomics and remove their negations (and other things based on the atomics) from not_atomic, so you need at least two filters: atomic :: [Clause] - [Clause] filter = (\atomic - length atomic == 1) The partition function partition :: (a - Bool) - [a] - ([a], [a]) will construct your list of atomic and non-atomic values for you. At this stage we have removed the unit/atomic clauses. We can now test for unsatisfiability, at least in terms of the atomic clauses:: atomic_satisfaction atoms = empty $ intersect (filter (\literal - (True, literal)) atoms) (filter (\literal - (False, literal)) atoms) You will then want to take the list of atomic values, and apply something like: filter (\(_, atom) - atom `elem` (fmap snd atomic)) to each element of each Clause. (where atomic is either the value I defined above, or the the correct value from an application of partition). The function is defined in terms of my understanding of all the clauses where the literal appears and also, from the remaining clauses, we delete the negation of the literal (because if P is true, -P will be false). Putting all of this stuff together will be challenging, and very slow. ;0) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant. pavel On 14.02.2011, at 22:57, Albert Y. C. Lai wrote: On 11-02-12 09:40 PM, Brandon S Allbery KF8NH wrote: Only up to a point. While most of the responses so far focus on the question from one direction, the other is epitomized by a Knuth quote: Beware of bugs in the above code; I have only proved it correct, not tried it. Knuth's definition of proof is of the sketchy kind of the mathematics community, not remotely close to the Coq kind. Even Dijsktra's and Bird's kind offers higher assurance than the traditional mathematician's sketchy kind. There are still gaps, but drastically narrower than Knuth's gaps, and bridgeable with probability arbitrarily close to 1: Possible defects in theorem provers: Use several theorem provers and/or several independent alternative implementations (both alternative software and alternative hardware). Possible deviation of Haskell compilers from your assumed formal semantics of Haskell: Verify the compilers too, or modify the compilers to emit some sort of proof-carrying code. Possible defects in target hardware: The hardware people are way ahead in improving both formal verification and manufacturing processes to reduce defects. When John Harrison ( http://www.cl.cam.ac.uk/~jrh13/ ) has a proof for a floating-point algorithm, I would not dare to apply the Knuth quote on it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On 11-02-14 03:03 PM, Pavel Perikov wrote: Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant. Who claimed that Haskell is a proof assistant? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
Who claimed that Haskell is a proof assistant? no one sanely will :) Haskell is a beautiful and practical (!) programming language with great infrastructure and community. Sadly, proving inside haskell is hard :) And it doesn't bring me coffee in the morning too (well, it mostly does) pavel. On 14.02.2011, at 23:08, Albert Y. C. Lai wrote: On 11-02-14 03:03 PM, Pavel Perikov wrote: Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sub-optimal
Is this a known bug? (GHC 6.10.x) It's known to happen when optimising shares what shouldn't be shared. Try compiling with -O2 -fno-cse (if that doesn't help, it doesn't necessarily mean it's not unwanted sharing, though). And, please, let us see some code to identify the problem. I tried -O2 -fno-cse. No difference. I also tried -O2 -fno-full-laziness. BIG DIFFERENCE. The program now runs in constant space (like with -O0), but it also runs about 2x faster than -O0. I have no idea what these switches do, but clearly one of these optimisations is actually pessimal for this particular program. I still want to try compiling with a newer version of GHC to see what difference that makes. (And yes, if I had the code on this PC, I could post it. It's kinda long though... In essence, it just calls randomRIO a bazillion times and writes the results into a file using hPutChar.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] rewrite rules to specialize function according to type class?
Hi all,
I am trying to get a GHC rewrite rule that specialises a function
according to the type of the argument of the function. Does anybody know
whether it is possible to do that not with a concrete type but rather a
type class?
Consider the following example:
class A a where
toInt :: a - Int
{-# NOINLINE toInt #-}
class B a where
toInt' :: a - Int
The idea is to use the method of type class A unless the type is also an
instance of type class B. Let's say that Bool is an instance of both A
and B:
instance A Bool where
toInt True = 1
toInt False = 0
instance B Bool where
toInt' True = 0
toInt' False = 1
Now we add a rule that says that if the argument to toInt happens to
be an instance of type class B as well, use the method toInt' instead:
{-# RULES
toInt forall (x :: B a = a) . toInt x = toInt' x
#-}
Unfortunately, this does not work (neither with GHC 6.12 or GHC 7.0).
Expression toInt True gets evaluated to 1. If the rewrite rule is
written with a concrete type it works as expected:
{-# RULES
toInt forall (x :: Bool) . toInt x = toInt' x
#-}
Now toInt True is evaluated to 0.
Am I doing something wrong or is it not possible for GHC to dispatch a
rule according to type class constraints?
Thanks,
Patrick
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On 14.02.2011, at 03:03 PM, Pavel Perikov [peri...@gmail.com] wrote: Sorely, Haskell can't prove logic with it. No predicates on values, guarantee that proof is not _|_. Haskell makes bug free software affordable, that's true. But it's not a proof assistant. Being equivalent to a class of total recursive functions, the EP (Enterprise-Participant) data model can assist users to enter arbitrary and meaningful expressions only. It is a new addition to programming languages. Check out here: http://www.froglingo.com/FroglingoPL.pdf Kevin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] rewrite rules to specialize function according to type class?
On 14 February 2011 21:43, Patrick Bahr pa...@arcor.de wrote: Am I doing something wrong or is it not possible for GHC to dispatch a rule according to type class constraints? As you have discovered this is not possible. You can write the rule for as many *particular* types as you like, but you can't write it in a way that abstracts over the exact type class instance you mean. This is a well known and somewhat tiresome issue. I think the reason that this is not implemented is because it would require the rule matcher to call back into the type checking machinery to do instance lookup. Cheers, Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sub-optimal
On 14 February 2011 21:00, Andrew Coppin andrewcop...@btinternet.com wrote: Is this a known bug? (GHC 6.10.x) It's known to happen when optimising shares what shouldn't be shared. Try compiling with -O2 -fno-cse (if that doesn't help, it doesn't necessarily mean it's not unwanted sharing, though). And, please, let us see some code to identify the problem. I tried -O2 -fno-cse. No difference. I also tried -O2 -fno-full-laziness. BIG DIFFERENCE. See also the very old GHC ticket at http://hackage.haskell.org/trac/ghc/ticket/917 Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] rewrite rules to specialize function according to type class?
On Tue, Feb 15, 2011 at 12:48 AM, Max Bolingbroke batterseapo...@hotmail.com wrote: On 14 February 2011 21:43, Patrick Bahr pa...@arcor.de wrote: Am I doing something wrong or is it not possible for GHC to dispatch a rule according to type class constraints? As you have discovered this is not possible. You can write the rule for as many *particular* types as you like, but you can't write it in a way that abstracts over the exact type class instance you mean. This is a well known and somewhat tiresome issue. I think the reason that this is not implemented is because it would require the rule matcher to call back into the type checking machinery to do instance lookup. This is a semi-related question I've been meaning to ask at some point: I suppose this also means it's not possible to write a class, write some rules for the class, and then have the rules be applied to every instance? (I.e. you'd have to write them separately for each?) Cheers, Max ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Work is punishment for failing to procrastinate effectively. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lhs2tex and line numbers
Hi! On Mon, Feb 14, 2011 at 12:23 PM, Andres Loeh andres.l...@googlemail.com wrote: A long time ago, I've written some experimental code that achieves line numbering in lhs2tex. I've committed the files to the github repository, so you can have a look at the .fmt file and the demo document in Great! Super! This is exactly what I needed. Thanks really a lot! I especially like having the numbers on the right. Mitar ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] ANN: vector-buffer package 0.1
Hi, I have uploaded a small package, vector-buffer, to hackage. It provides a buffer that can be turned into a Data.Vector.Storable. The mapM* functions map from the oldest element, not the first. Similarly for the derived Vector. Feature requests etc. welcome. Vivian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving correctness
On 2/11/11 1:25 PM, Luke Palmer wrote: I would like to see a language that allowed optional verification, but that is a hard balance to make because of the interaction of non-termination and the evaluation that needs to happen when verifying a proof. I believe that ATS (short for Advanced Type System) allows this. Although I haven't actually programmed in it, I read through the documentation and it looks to me like it is a fully dependently-typed language that allows you prove as little or as much about your program as you like. http://www.ats-lang.org/ Cheers, Greg ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: vector-buffer package 0.1
This interface is an outlaw. main = do buf - newBuffer 10 :: IO (Buffer Int) pushNextElement buf 1 let v1 = V.toList (toVector buf) v2 = V.toList (toVector buf) print v1 pushNextElement buf 2 print v2 Despite v1 and v2 being defined to equal the exact same thing, this program prints two distinct lines. toVector depends on the current state of the buffer. If this is to be a law-abiding interface, toVector must return a value in IO: toVector :: (Storable a) = Buffer a - IO (Vector a) Luke On Mon, Feb 14, 2011 at 7:28 PM, Alexander McPhail haskell.vivian.mcph...@gmail.com wrote: Hi, I have uploaded a small package, vector-buffer, to hackage. It provides a buffer that can be turned into a Data.Vector.Storable. The mapM* functions map from the oldest element, not the first. Similarly for the derived Vector. Feature requests etc. welcome. Vivian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: vector-buffer package 0.1
Hi Luke, Apologies, I think I got bitten by unsafePerformIO. The reason it wasn't in the IO monad is that the Vector created from the Buffer is supposed to be immutable. I've changed the API so that: main = do buf - newBuffer 10 :: IO (Buffer Int) pushNextElement buf 1 v1 - toVector buf v2 - toVector buf print $ V.toList v1 pushNextElement buf 2 print $ V.toList v2 does as expected. Thanks, Vivian On 15 February 2011 17:08, Luke Palmer lrpal...@gmail.com wrote: This interface is an outlaw. main = do buf - newBuffer 10 :: IO (Buffer Int) pushNextElement buf 1 let v1 = V.toList (toVector buf) v2 = V.toList (toVector buf) print v1 pushNextElement buf 2 print v2 Despite v1 and v2 being defined to equal the exact same thing, this program prints two distinct lines. toVector depends on the current state of the buffer. If this is to be a law-abiding interface, toVector must return a value in IO: toVector :: (Storable a) = Buffer a - IO (Vector a) Luke On Mon, Feb 14, 2011 at 7:28 PM, Alexander McPhail haskell.vivian.mcph...@gmail.com wrote: Hi, I have uploaded a small package, vector-buffer, to hackage. It provides a buffer that can be turned into a Data.Vector.Storable. The mapM* functions map from the oldest element, not the first. Similarly for the derived Vector. Feature requests etc. welcome. Vivian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- --- yolar et elver. --- DISCLAIMER This transmission contains information that may be confidential. It is intended for the named addressee only. Unless you are the named addressee you may not copy or use it or disclose it to anyone else. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Fwd: ANN: vector-buffer package 0.1
Hi list,
Could someone explain why the error pointed out by Luke occurred?
From: Luke Palmer lrpal...@gmail.com
I think this would be a very good question for the list. Don't worry,
they're nice helpful folks.
On Mon, Feb 14, 2011 at 10:10 PM, Alexander McPhail
haskell.vivian.mcph...@gmail.com wrote:
Hi Roman,
Can you explain why the following code doesn't work? 'unsafePerformIO' is
used all the time in hmatrix. For example, adding two vectors, we create
a
new Vector then use that as the target for an FFI C call.
Is the difference because I'm using mutable Storable Vectors? I would
have
thought that unsafeFreeze (at the end) would make sure the problem
reported
by Luke wouldn't occur.
Is there a problem with laziness in the let binding of Luke's example?
I note that in Data.Vector.Storable there is a pure 'convert' function,
which is essentially what I am trying to emulate.
-- | convert to a vector
toVector :: Storable a = Buffer a - (V.Vector a)
toVector (B o n v) = unsafePerformIO $ do
w - M.new n
i - readIORef o
M.unsafeWith v $ \p -
M.unsafeWith w $ \q - do
let n' = n-i
copyArray q (p `advancePtr` i) n'
if i /= 0
then copyArray (q `advancePtr` n') p i
else return ()
V.unsafeFreeze w
{-# INLINE toVector #-}
Vivian
From: Luke Palmer lrpal...@gmail.com
This interface is an outlaw.
main = do
buf - newBuffer 10 :: IO (Buffer Int)
pushNextElement buf 1
let v1 = V.toList (toVector buf)
v2 = V.toList (toVector buf)
print v1
pushNextElement buf 2
print v2
Despite v1 and v2 being defined to equal the exact same thing, this
program prints two distinct lines.
toVector depends on the current state of the buffer. If this is to be
a law-abiding interface, toVector must return a value in IO:
toVector :: (Storable a) = Buffer a - IO (Vector a)
Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
