Re: [Haskell-cafe] [Cabal-devel] Cabal license combinations

2011-02-11 Thread Ketil Malde
Chris Smith cdsm...@gmail.com writes:

 actually matter.  The instant anyone actually compiles an application
 that uses your library, however indirectly, they are bound by the terms

There are other uses for code than compilation.  Let's say I wrote a
wrapper for a proprietary library that connects to Oracle databases.
Any program using this would likely be undistributable.  Still, having
the wrapper free would allow porting it to a free database back end or
using it for teaching, so there's always added value in added freedom.

 So this may be a problem for distributions, which ship compiled and
 linked binaries.  But generally not for authors, darcs repositories or
 Hackage, which only ship source code.

 Of course it is a concern for authors!

I don't think you are contradicting me here.  My point is that authors
are not likely to be liable or bound by other's licenses - whether they
are concerned or not, is up to them.

 The reasonable expectation in Haskell is that they'll probably
 statically link; and you should read licenses of your dependencies,
 and carefully choose dependencies, accordingly.

I think usability goes way beyond redistributability, but I
guess we should just agree to disagree on this.

IMO, the important thing is that cabal avoids imposing legal
straightjackets on authors, and that it avoids making legal
interpretations.  Echoing facts from cabal files is okay, but drawing
legal conclusions based on these facts should be the responsibility
(i.e. both obligation and liability) of the individual user.

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Proving correctness

2011-02-11 Thread C K Kashyap
Hi Folks,

I've come across this a few times - In Haskell, once can prove the
correctness of the code - Is this true?

I know that static typing and strong typing of Haskell eliminate a whole
class of problems - is that related to the proving correctness?
Is it about Quickcheck - if so, how is it different from having test sutites
in projects using mainstream languages?


Regards,
Kashyap
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Ivan Lazar Miljenovic
On 11 February 2011 22:06, C K Kashyap ckkash...@gmail.com wrote:
 Hi Folks,
 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?

I'm not quite sure where you got that...

But since Haskell is pure, we can also do equational reasoning, etc.
to help prove correctness.  Admittedly, I don't know how many people
actually do so...

 I know that static typing and strong typing of Haskell eliminate a whole
 class of problems - is that related to the proving correctness?
 Is it about Quickcheck - if so, how is it different from having test sutites
 in projects using mainstream languages?

QuickCheck doesn't prove correctness: I had a bug that survived
several releases tested regularly during development with a QC-based
testsuite before it arose (as it required a specific condition to be
satisfied for the bug to happen).  As far as I know, a testsuite - no
matter what language or what tools/methodologies are used - for a
non-trivial piece of work just provides reasonable degree of assurance
of correctness; after all, there could be a bug/problem you hadn't
thought of!

-- 
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Markus Läll
I think one thing it means, is that, with the typesystem, you just can't do
random things where-ever you want. Like, in the pure world if you want to
transform values from one type to another, you always need to have
implementations of functions available to do that. (You can't just take a
pure value, get its mem location and interpret it as something else, without
being explicid about it.) So when lining up your code (composing functions),
you can be sure, that at least as far as types are concerned, everything is
correct -- that such a program, that you wrote, can actually exist == that
all the apropriate functions exist.

And it is correct only that far -- the value-level coding is still up to
you, so no mind-reading...


--
Markus Läll

On Fri, Feb 11, 2011 at 1:16 PM, Ivan Lazar Miljenovic 
ivan.miljeno...@gmail.com wrote:

 On 11 February 2011 22:06, C K Kashyap ckkash...@gmail.com wrote:
  Hi Folks,
  I've come across this a few times - In Haskell, once can prove the
  correctness of the code - Is this true?

 I'm not quite sure where you got that...

 But since Haskell is pure, we can also do equational reasoning, etc.
 to help prove correctness.  Admittedly, I don't know how many people
 actually do so...

  I know that static typing and strong typing of Haskell eliminate a whole
  class of problems - is that related to the proving correctness?
  Is it about Quickcheck - if so, how is it different from having test
 sutites
  in projects using mainstream languages?

 QuickCheck doesn't prove correctness: I had a bug that survived
 several releases tested regularly during development with a QC-based
 testsuite before it arose (as it required a specific condition to be
 satisfied for the bug to happen).  As far as I know, a testsuite - no
 matter what language or what tools/methodologies are used - for a
 non-trivial piece of work just provides reasonable degree of assurance
 of correctness; after all, there could be a bug/problem you hadn't
 thought of!

 --
 Ivan Lazar Miljenovic
 ivan.miljeno...@gmail.com
 IvanMiljenovic.wordpress.com

 ___
 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

2011-02-11 Thread Steffen Schuldenzucker

On 02/11/2011 12:06 PM, C K Kashyap wrote:

[...]
I know that static typing and strong typing of Haskell eliminate a 
whole class of problems - is that related to the proving correctness?

[...]
You might have read about free theorems arising from types. They are a 
method to derive certain properties about a value that must hold, only 
looking at its type. For example, a value


 x :: a

can't be anything else than bottom, a function

 f :: [a] - [a]

must commute with 'map', etc. For more information you may be interested 
in Theorems for free[1] by Philip Wadler.


[1] http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Daniel Fischer
On Friday 11 February 2011 12:06:58, C K Kashyap wrote:
 Hi Folks,

 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?

One can also prove the correctness of the code in other languages.
What makes these proofs much easier in Haskell than in many other languages 
is purity and immutability. Also the use of higher order combinators (you 
need prove foldr, map, ... correct only once, not everytime you use them).
Thus, proving correctness of the code is feasible for more complicated 
programmes in Haskell than in many other languages.
Nevertheless, for sufficiently complicated programmes, proving correctness 
is unfeasible in Haskell too.


 I know that static typing and strong typing of Haskell eliminate a whole
 class of problems - is that related to the proving correctness?

Yes, strong static typing (and the free theorems mentioned by Steffen) give 
you a stronger foundation upon which to build the proof.

 Is it about Quickcheck - if so, how is it different from having test
 sutites in projects using mainstream languages?

Testing can only prove code incorrect, it can never prove code correct 
(except for extremely simple cases where testing all possible inputs can be 
done; but guaranteeing that QuickCheck generates all possible inputs is 
generally harder than a proof without testing in those cases).



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Sebastian Fischer

 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?


One way to prove the correctness of a program is to calculate it from its
specification. If the specification is also a Haskell program, equational
reasoning can be used to transform a (often inefficient) specification into
an equivalent (but usually faster) implementation. Richard Bird describes
many examples of this approach, one in his functional pearl on a program to
solve Sudoku [1]. Jeremy Gibbons gives an introduction to calculating
functional programs in his lecture notes  of the Summer School on Algebraic
and Coalgebraic Methods in the Mathematics of Program Construction [2].

Sebastian

[1]: http://www.cs.tufts.edu/~nr/comp150fp/archive/richard-bird/sudoku.pdf
[2]:
http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Christian Maeder
Am 11.02.2011 13:48, schrieb Daniel Fischer:
[...] +1
 Testing can only prove code incorrect, it can never prove code correct 
 (except for extremely simple cases where testing all possible inputs can be 
 done; but guaranteeing that QuickCheck generates all possible inputs is 
 generally harder than a proof without testing in those cases).

Maybe smallcheck is better than QuickCheck for such (finite and simple)
cases.
http://hackage.haskell.org/package/smallcheck

C.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Dominique Devriese
Kashyap,

2011/2/11 C K Kashyap ckkash...@gmail.com:
 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?
 I know that static typing and strong typing of Haskell eliminate a whole
 class of problems - is that related to the proving correctness?
 Is it about Quickcheck - if so, how is it different from having test sutites
 in projects using mainstream languages?

You may be confusing Haskell with dependently typed programming languages such
as Coq or Agda, where formal proofs of correctness properties of
programs can be verified by the type checker.

Dominique

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Haskell Help

2011-02-11 Thread Patrick M
I'm
 writting a function that will remove tautologies from a fomula.The 
basic idea is that if in a clause, a literal and its negation are found,
 it means that the clause will be true, regardless of the value finally 
assigned to that propositional variable.My appoach is to create a 
function that will remove this but for a clause and map it to the 
fomula.Of course I have to remove duplicates at the beginning.

    module Algorithm where

    import System.Random
    import Data.Maybe
    import Data.List

    type Atom = String
    type Literal = (Bool,Atom)
    type Clause = [Literal]
    type Formula = [Clause]
    type Model = [(Atom, Bool)]
    type Node = (Formula, ([Atom],
 Model))
    removeTautologies :: Formula - Formula
    removeTautologies = map tC.map head.group.sort
  where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest
  | otherwise = (vx, x) : rt ((vy, y) : 
clauses)
Now
 I have problems  when I try to give it a formula (for example (A v B v 
-A) ^ (B v C v A)).Considering that example the first clause contains 
the literals A and -A. This means that the clause will always be true, 
in which case it can be simplify the whole set to simply (B v C v A) . 
But I get the following

    Loading package old-locale-1.0.0.2 ... linking ... done.
    Loading
 package time-1.1.4 ... linking ... done.
    Loading package random-1.0.0.2 ... linking ... done.
    [[(True,A),(True,B)*** Exception: Assignment.hs:(165,11)-(166,83): 
Non-exhaustive patterns in function rt

What should I do?


  ___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Haskell Help

2011-02-11 Thread PatrickM

I'm writting a function that will remove tautologies from a fomula.The basic
idea is that if in a clause, a literal and its negation are found, it means
that the clause will be true, regardless of the value finally assigned to
that propositional variable.My appoach is to create a function that will
remove this but for a clause and map it to the fomula.Of course I have to
remove duplicates at the beginning.

module Algorithm where

import System.Random
import Data.Maybe
import Data.List

type Atom = String
type Literal = (Bool,Atom)
type Clause = [Literal]
type Formula = [Clause]
type Model = [(Atom, Bool)]
type Node = (Formula, ([Atom], Model))
removeTautologies :: Formula - Formula
removeTautologies = map tC.map head.group.sort
  where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest
  | otherwise = (vx, x) : rt ((vy,
y) : clauses)
Now I have problems  when I try to give it a formula (for example (A v B v
-A) ^ (B v C v A)).Considering that example the first clause contains the
literals A and -A. This means that the clause will always be true, in which
case it can be simplify the whole set to simply (B v C v A) . But I get the
following

Loading package old-locale-1.0.0.2 ... linking ... done.
Loading package time-1.1.4 ... linking ... done.
Loading package random-1.0.0.2 ... linking ... done.
[[(True,A),(True,B)*** Exception: Assignment.hs:(165,11)-(166,83):
Non-exhaustive patterns in function rt

What should I do?
-- 
View this message in context: 
http://haskell.1045720.n5.nabble.com/Haskell-Help-tp3381647p3381647.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] Haskell Help

2011-02-11 Thread Daniel Fischer
On Friday 11 February 2011 18:25:24, PatrickM wrote:
 I'm writting a function that will remove tautologies from a fomula.The
 basic idea is that if in a clause, a literal and its negation are found,
 it means that the clause will be true, regardless of the value finally
 assigned to that propositional variable.My appoach is to create a
 function that will remove this but for a clause and map it to the
 fomula.Of course I have to remove duplicates at the beginning.

Tip: write a function

isTautology :: Clause - Bool

for that, the function partition from Data.List might be useful.
Then removeTautologies becomes a simple filter.


 module Algorithm where

 import System.Random
 import Data.Maybe
 import Data.List

 type Atom = String
 type Literal = (Bool,Atom)
 type Clause = [Literal]
 type Formula = [Clause]
 type Model = [(Atom, Bool)]
 type Node = (Formula, ([Atom], Model))
 removeTautologies :: Formula - Formula
 removeTautologies = map tC.map head.group.sort
   where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest

   | otherwise = (vx, x) : rt
   | ((vy,

 y) : clauses)
 Now I have problems  when I try to give it a formula (for example (A v B
 v -A) ^ (B v C v A)).Considering that example the first clause contains
 the literals A and -A. This means that the clause will always be true,
 in which case it can be simplify the whole set to simply (B v C v A) .
 But I get the following

 Loading package old-locale-1.0.0.2 ... linking ... done.
 Loading package time-1.1.4 ... linking ... done.
 Loading package random-1.0.0.2 ... linking ... done.
 [[(True,A),(True,B)*** Exception:
 Assignment.hs:(165,11)-(166,83): Non-exhaustive patterns in function rt

 What should I do?

You have to treat the cases of lists with zero or one entries in rt.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] Is Show special? Of course not but...

2011-02-11 Thread Cristiano Paris
Hi cafè,

given the following toy code:

---
module Main where

class Dumb p where
dumb :: p - String

newtype Branded a b = Branded b

unbrand :: Branded a b - b
unbrand (Branded x) = x

wrong :: Dumb a = b - Branded a b
wrong = Branded

right :: Show a = b - Branded a b
right = Branded
---

Why:

---
quarry:Haskell paris$ ghci -O1
GHCi, version 6.12.3: http://www.haskell.org/ghc/  :? for help
*Main unbrand $ right True
True
*Main unbrand $ right Foo
Foo
---

but:

---
*Main unbrand $ wrong True

interactive:1:10:
Ambiguous type variable `a' in the constraint:
  `Dumb a' arising from a use of `wrong' at interactive:1:10-19
Probable fix: add a type signature that fixes these type variable(s)
---

?

Maybe it's a dumb question but... thank you for any explanation...

-- 
Cristiano

GPG Key: 4096R/C17E53C6 2010-02-22
Fingerprint = 4575 4FB5 DC8E 7641 D3D8  8EBE DF59 B4E9 C17E 53C6

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Is Show special? Of course not but...

2011-02-11 Thread Daniel Fischer
On Friday 11 February 2011 19:33:27, Cristiano Paris wrote:
 Hi cafè,

 given the following toy code:

 ---
 module Main where

 class Dumb p where
   dumb :: p - String

 newtype Branded a b = Branded b

 unbrand :: Branded a b - b
 unbrand (Branded x) = x

 wrong :: Dumb a = b - Branded a b
 wrong = Branded

 right :: Show a = b - Branded a b
 right = Branded
 ---

 Why:

 ---
 quarry:Haskell paris$ ghci -O1
 GHCi, version 6.12.3: http://www.haskell.org/ghc/  :? for help
 *Main unbrand $ right True
 True
 *Main unbrand $ right Foo
 Foo
 ---

 but:

 ---
 *Main unbrand $ wrong True

 interactive:1:10:
 Ambiguous type variable `a' in the constraint:
   `Dumb a' arising from a use of `wrong' at interactive:1:10-19
 Probable fix: add a type signature that fixes these type variable(s)
 ---

 ?

 Maybe it's a dumb question but... thank you for any explanation...

It's because there's no way to determine the type variable a (in either 
wrong or right).
In such cases, under some circumstances, the type variable gets defaulted 
(the ambiguous contexts all must have the form (C a), at least one numeric 
class [Num, Integral, Fractional, ...] is involved, all involved classes 
come from the Prelude or the standard libraries) as specified in the report 
(section 4.3, iirc).

These conditions are not met by your 'right' function, but ghci uses 
extended default rules, a type variable a with a Show constraint [and no 
other] gets defaulted to (). But ghci has no rule how to default your Dumb 
class, so it reports the ambiguous type variable there.
[Without extended defaulting rules, ambiguous type variable errors would be 
too frequent at the ghci prompt.]

If you try to compile the module, both should raise an ambiguous type 
variable error, since the compiler follows the standard defaulting rules 
(unless you enable -XExtendedDefaultRules).

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Is Show special? Of course not but...

2011-02-11 Thread Cristiano Paris
On Fri, Feb 11, 2011 at 20:00, Daniel Fischer
daniel.is.fisc...@googlemail.com wrote:
 ...
 It's because there's no way to determine the type variable a (in either
 wrong or right).

That's what I thought when I wrote the code at first but then I was
surprised to see it working with the Show type-class.

 In such cases, under some circumstances, the type variable gets defaulted
 (the ambiguous contexts all must have the form (C a), at least one numeric
 class [Num, Integral, Fractional, ...] is involved, all involved classes
 come from the Prelude or the standard libraries) as specified in the report
 (section 4.3, iirc).

I'm reading it right now.

 ...
 These conditions are not met by your 'right' function, but ghci uses
 extended default rules, a type variable a with a Show constraint [and no
 other] gets defaulted to (). But ghci has no rule how to default your Dumb
 class, so it reports the ambiguous type variable there.
 [Without extended defaulting rules, ambiguous type variable errors would be
 too frequent at the ghci prompt.]

God! It seems like I'm reading the small-character lines of a contract :)

Seriously, now it makes sense...

Thank you.

-- 
Cristiano

GPG Key: 4096R/C17E53C6 2010-02-22
Fingerprint = 4575 4FB5 DC8E 7641 D3D8  8EBE DF59 B4E9 C17E 53C6

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] unicode filenames advice

2011-02-11 Thread Joey Hess
I've been trying to deal with how my haskell program handles unicode
filenames. Been dealing with problems like those described here:

http://hackage.haskell.org/trac/ghc/ticket/3307

Or, simply demonstrated by feeding unicode to getLine = readFile

My approach currently is to carefully identify any point where
a FilePath is output, and run it through a filePathToString (which
varies by OS), as suggested in the above bug report.

Is there a less tedious and error-prone way? What is the best approach
to use now, assuming that these issues will be dealt with in some way
in Haskell, eventually?

-- 
see shy jo


signature.asc
Description: Digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] hledger: mtl vs transformers

2011-02-11 Thread Simon Michael

On Feb 11, 2011, at 11:20 AM, Peter Simons wrote:
If hledger offers optional features by means of Cabal flags, then  
users
of the library need the ability to depend on hledger with a specific  
set

of features (flags) enabled or disabled, but unfortunately Cabal can't
do that.

The new approach remedies that problem by placing optional features in
separate packages. That creates a different problem, however, because
users may now install hledger and hledger-web separately, which --  
as we

know -- may create all kinds of version conflicts that are non-trivial
to resolve.

This is the problem you're now trying to solve by over-specifying the
dependencies of hledger. Arguably, though, Cabal should solve that
problem for the user, i.e. by offering to re-compile hledger to  
resolve

the conflict etc., but unfortunately Cabal can't do that either.


Hi Peter.. thanks for the follow-up. In case it wasn't clear, I do  
realise now that attempts to over-specify depedencies to avoid  
practical cabal install issues can backfire, and a package author  
should just accept that cabal install can't be made 100% reliable  
installation method for non-experts (for now - I know many people are  
thinking about this).


And, I've fixed/relaxed the process dependency in hledger head, and  
only laziness/business has prevented that from being released to  
hackage. I'll do that asap.


Cheers - Simon

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Alexander Solla
On Fri, Feb 11, 2011 at 3:06 AM, C K Kashyap ckkash...@gmail.com wrote:

 Hi Folks,

 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?

 I know that static typing and strong typing of Haskell eliminate a whole
 class of problems - is that related to the proving correctness?
 Is it about Quickcheck - if so, how is it different from having test
 sutites in projects using mainstream languages?


Let's interpret a type as a partial specification of a value.  If we can
express this partial specification completely enough so that one (and only
one, at least ignoring values like bottom) value is a member of the type,
then any expression of that value must be formally correct.

There are a couple of issues:  the type system is strong, but it still has
limitations.  There are types we might like to express, but can't.  We might
be able to express supersets of the type we really want, and the type
inference engine will ensure that a value in the type meets at least this
partial specification, but it cannot check to see if it is the right value
in the type.  That is up to us.  Some of Haskell's properties, like
referential transparency, equational reasoning, etc. make this easier than
in other languages.

A related difficulty is that encoding specifications is a programming task
in itself.  Even if you correctly compile requirements, and are able to
completely encode them in the type system, you might still introduce a logic
mistake in this encoding.  A similar issue is that logic mistakes can creep
into the requirements compiling phase of a project.  In either of these
cases, your values would dutifully and correctly compute the wrong things.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Proving correctness

2011-02-11 Thread Luke Palmer
On Fri, Feb 11, 2011 at 4:06 AM, C K Kashyap ckkash...@gmail.com wrote:
 Hi Folks,
 I've come across this a few times - In Haskell, once can prove the
 correctness of the code - Is this true?

You can prove the correctness of code for any language that has
precise semantics.  Which is basically none of them (I believe a
dialect of ML has one).  But many languages come very close, and
Haskell is one of them.  In particular, Haskell's laziness allows very
liberal use of equational reasoning, which is much more approachable
as a technique for correctness proofs than operational semantics.

The compiler is not able to verify your proofs, as Coq and Agda can,
except in very simple cases.  On the other hand, real-world
programmers the advantage of not being forced to prove the correctness
of their code because proofs are hard (technically Coq and Agda only
require you to prove termination, but many times termination proofs
require knowing most properties of your program so you have to
essentially prove correctness anyway).  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 have proved the correctness of Haskell code before.  Mostly I prove
that monads I define satisfy the monad laws when I am not sure whether
they will.  It is usually a pretty detailed process, and I only do it
when I am feeling adventurous.  I am not at home and I don't believe
I've published any of my proofs, so you'll have to take my word for it
:-P

There is recent research on automatically proving (not just checking
like QuickCheck, but formal proofs) stated properties in Haskell
programs.  It's very cool. http://www.doc.ic.ac.uk/~ws506/tryzeno/

I would not characterize provable code as an essential defining
property of Haskell, though it is easier than in imperative and in
strict functional languages.  Again, Agda and Coq are really the ones
that stand out in the provable code arena.  And certainly I have an
easier time mentally informally verifying the correctness of Haskell
code than in other languages, because referential transparency removes
many of the subtleties encountered in the process.  I am often 100%
sure of the correctness of my refactors.

Luke

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] coding a queue with reactive

2011-02-11 Thread Ryan Ingram
Hi Sam.  I don't know much about the performance problems you are
seeing, but I think your solution is more cleanly implemented just
under the event level with futures.

I think the reactive function you want has a type like this:

stateMachine :: s - (a - s - s) - (s - Future (b, s)) - Event a - Event b

I don't think that function currently exists in Reactive, but the semantics are:

stateMachine initialState updateState runner input
  | runner initialState - (b, nextState) happens before the first
event in input = output the b, then stateMachine nextState
updateState runner input
  | input - (Stepper a input') happens first = let nextState =
updateState a nextState, then stateMachine nextState updateState
runner input'

Here's my thoughts on an implementation:

stateMachineF s0 upd run (Event inp) = do
x - mappend (Left $ run s0) (Right $ inp)
case x of
Left (b,sNext) - return (Stepper b (stateMachineF sNext upd run inp))
Right (Stepper a inpNext) - stateMachineF (upd a s0) upd run inpNext

stateMachine s0 upd run inp = Event $ stateMachineF s0 upd run inp

Then we can do something like

queue delay = stateMachine Nothing upd run . withTimeE where
run Nothing = mempty
run (Just (t, a, q)) = future t (a, sNext) where
sNext = fmap (\(a', q') - (t + delay, a', q')) (viewQ q)
upd (time, x) Nothing = Just (time + delay, x, emptyQ)
upd (time, x) (Just (t, a, q)) = Just (t, a, pushQ x q)

given these queue functions:

emptyQ :: Queue a
viewQ :: Queue a - Maybe (a, Queue a)
pushQ :: a - Queue a - Queue a

which can be pretty easily implemented on the standard functional
queue structure

data Queue a = Q [a] [a]
emptyQ = Q [] []
pushQ a (Q fs bs) = Q fs (a:bs)
viewQ (Q [] []) = Nothing
viewQ (Q (a:fs) bs) = Just (a, Q fs bs)
viewQ (Q [] bs) = viewQ (Q (reverse bs) [])


On Wed, Feb 9, 2011 at 1:26 PM,  sam.roberts.1...@gmail.com wrote:
 Hi all,

 I hope someone is interested in helping me out with the reactive library.
 I am trying to implement a function queue in reactive:

 queue :: Double - Event a - Event a

 This is a simple queue: events from the event stream coming into the queue,
 queue up waiting to be processed one by one. Processing an event takes a
 constant amount of time for every event. The output of the queue function
 is the stream of processed events.

 My current (deficient) implementation of the queue function is:

 queue dt eventsIn =
 do
 (a,exitT) - withExitTime eventsIn
 _ - atTime exitT
 return a
 where
 withExitTime = scanlE calcExitTime (undefined, -1/0) . withTimeE
 calcExitTime (_,prevExitT) (a,inT) = (a, (max inT prevExitT) + dt)

 I am having three problems.

 1 - I find my implementation of the queue is less clear then an imperative
 description of a queue.

 2 - I rely on being able to calculate the exit time of an event when it
 first arrives at the queue, whereas an imperative queue would simply store
 the event in queue and only need to calculate the output time once the event
 was popped off the queue. If I want to do something similar with my
 function,
 I think I need to make some sort of recursive definition of a queue which
 responds to it's own exit events. I've tried to code this up, but have not
 managed to wrap my brain around the concept.

 3 - The code performs horribly! I am guessing that this is because I have
 not
 told reactive that the exit events preserve the ordering of the input
 events,
 but I'm not sure how to encode that relationship in reactive.

 (It's worth noting here that I actually have a fourth problem too: I get
 linker errors while trying to compile a profiling version of the program ...
 but that's a separate topic.)

 It's also worth noting, from a performance point of view, that a much
 simpler
 delay function with similar use of the bind function performs badly as
 well:

 delay :: Double - Event a - Event a
 delay dt es = do (e,t) - withTimeE es
 _ - atTime (t+dt)
 return e

 I'd appreciate any light that anyone could shed on any of these problems.
 If there's a better way of structuring my queue function, or if there's a
 better way of changing event times in reactive, I am open to all
 suggestions.

 Many thanks,
 Sam
 ___
 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] Compiling network-bytestring with ghc7+hp2011

2011-02-11 Thread Magnus Therning
On Fri, Feb 11, 2011 at 04:48:28PM -0800, Johan Tibell wrote:
 Hi Magnus,
 
 network-2.3 supersedes network-bytestring as the modules provided by
 the latter were merged into network. network-2.3 and later cannot be
 used together with network-bytestring, in one package, as both
 expose the same modules. Libraries that use network-bytestring
 should eventually migrate to network-2.3.

Excellent, I wasn't aware of this.

I suggest that the Hackage entry for network-bytestring is modified to
let users know this.  I noticed that monads-fd has been marked as
obsolete on Hackage, with a pointer to mtl, maybe it's possible to do
something similar with network-bytestring?

/M

-- 
Magnus Therning  OpenPGP: 0xAB4DFBA4 
email: mag...@therning.org   jabber: mag...@therning.org
twitter: magthe   http://therning.org/magnus


pgpOKKDFbawde.pgp
Description: PGP signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe