- Haskell-Cafe - Haskell.org

Do you trust Wikipedia?
by PR Stanley 19 Oct '07

19 Oct '07

Hi Do you trust mathematical materials on Wikipedia? Paul

22 31

Re: [Haskell] Re: Trying to install binary-0.4
by Simon Marlow 19 Oct '07

19 Oct '07

Udo Stenzel wrote: > Simon Marlow wrote: >> So a package that depends on 'base' (with no upper version bound) *might* >> be broken in GHC 6.8.1, depending on which modules from base it actually >> uses. Let's look at the other options: >> >> - if we rename base, the package will *definitely* be broken >> >> - if the package specified an upper bound on its base dependency, it will >> *definitely* be broken > > - if you provide a 'base' configuration that pulls in the stuff that > used to be in base, the package will work I don't know of a way to do that. The name of the package is baked into the object files at compile time, so you can't use the same compiled module in more than one package. > I hate betting, but I'd like to know if... > > - it is okay to give GHC 6.4/6.6 a castrated configuration of the base > libraries to remove the conflict with recent ByteString? Sure, that's what I suggested before. Moving modules of an existing package from 'exposed-modules' to 'hidden-modules' is safe (I wouldn't recommend removing them entirely). > - when GHC 6.8 comes out containing base-3, will it be possible to > additionally install something calling base-2 with both being > available to packages? In theory yes - the system was designed to allow this. In practice we've never tried it, and base-2 might not compile unmodified with GHC 6.8. > - If so, will existing Cabal packages automatically pick up the > compatible base-2 despite base-3 being available? Only if they specify an upper bound on the base dependency, which most don't, but it's an easy change to make. Cheers, Simon

17 54

Re: [Haskell] Announce: generating free theorems, online and offline
by ajb＠spamcop.net 19 Oct '07

19 Oct '07

[Ccing to haskell-cafe; please direct any replies there instead of haskell] G'day all. First of all, once again well done to Sascha on a great tool. Just a few comments. Quoting Janis Voigtlaender <voigt(a)tcs.inf.tu-dresden.de>: > - support for type classes > (e.g., enter "elem" and note the generated respects-restrictions) This is a great feature, and it'll be even better when constructor classes are done. Some of these respects-restrictions arent as useful as they might be, because they don't take into account easily-predictable invariants. For example, the type: (Eq a) => [a] -> [a] generates the following restriction: g respects Eq if forall x :: t1. forall y :: t1. (==) x y = (==) (g x) (g y) forall x :: t1. forall y :: t1. (/=) x y = (/=) (g x) (g y) Thats correct, but redundant, because (x == y) = (g x == g y) if and only if (x /= y) = (g x /= g y). Crucially, you can work this out from the definition of Eq, because (/=) has a default implementation defined in terms of (==) alone. The type (Monoid a) => [a] -> a gives: forall t1,t2 in TYPES(Monoid), g :: t1 -> t2, g respects Monoid. forall x :: [t1]. g (f x) = f (map g x) The class restriction occurring therein is defined as follows: g respects Monoid if g mempty = mempty forall x :: t1. forall y :: t1. g (mappend x y) = mappend (g x) (g y) forall (x, y) in lift{[]}(g). g (mconcat x) = mconcat y Again, mconcat is redundant. Even more curiously, though, map appears in the theorem, but lift{[]} appears in the class restriction. Cheers, Andrew Bromage

8 21

Re: [Haskell] ANNOUNCE: Lazy SmallCheck 0.1
by Janis Voigtlaender 19 Oct '07

19 Oct '07

That's pretty cool. If you are not yet aware of it, you might want to compare this with the EasyCheck library for Curry. They directly use functional logic programming for test generation, where you use exceptions for simulating logical variables. Here are some slides of a talk I heard recently: http://www.informatik.uni-kiel.de/~jac/data/DarkSecret.pdf (in German, unfortunately) Matthew Naylor wrote: > Announcing Lazy SmallCheck 0.1, a library for exhaustive, > demand-driven testing of Haskell programs. > > Lazy SmallCheck is based on the idea that if a property holds for a > partially-defined input then it must also hold for all fully-defined > instantiations of that input. Compared to `eager' input generation > in SmallCheck, Lazy SmallCheck may require significantly fewer > test-cases to verify a property for all inputs up to a given depth. > > There is a webpage for Lazy SmallCheck: > > http://www-users.cs.york.ac.uk/~mfn/lazysmallcheck/ > > There you'll find a more detailed description, a worked example, a > comparison with SmallCheck on a number of benchmarks, and link to > download the library. > > The library was developed together with Fredrik Lindblad during his > recent visits to York. > > Suggestions, experiences and bug reports are welcome! > > Matthew. > _______________________________________________ > Haskell mailing list > Haskell(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell > -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de

1 0

data Bin = Zero | One
by PR Stanley 19 Oct '07

19 Oct '07

>Hi >data Bin = Zero | One As suggested by someone on this list. It's a really neat idea although I'm wondering how I can apply this to my int to binary function. The Zero or One declaration is saying that Bin is a data type that can hold either a one or a zero. I tried testing this with a very simple Bin -> Bin function and the Integral values 0 and 1 but ran into difficulties. Any ideas what I'm doing wrong here? Incidentally, does the general syntax above come from the old BNF notation? Cheers, Paul

2 1

Functional specification of DFS
by Vimal 19 Oct '07

19 Oct '07

Hello Haskellers, Yesterday, my professor had asked this question in a quiz: "Give a functional description of Depth First Search on a graph G. Use lisp." The first thing I wrote was: Let DFS(G, root) return the list of edges in the dfs spanning tree of G, rooted at root. Let n = |V| in: :) The naive algorithm of keeping a visited 'array' and recursive solution is what came to my mind. But, if we look at DFS as a mapping from G -> List of Spanning trees of G rooted at root, then we have an exponential (n**(n-2) ?) number of them, so, finding the one that satistifies the properties of a DFS spanning tree, might not be tractable. So, if we modify the specification of DFS(G, root) as DFS(G, root, intermediate_path), we get: DFS(G, root, path) = Union ( {(root, v)} U DFS(G, v, path U {root})) ) for all v not in path, and (root, v) exists in G. DFS is invoked as: DFS(G, root, {root}) The problem with this is that changes to "path" must be persistant across calls. i.e., {(root, v)} U DFS(G, v, {v, root} + recursive calls} U {(root, w)} U DFS(G, v, {v, root}, + nodes added in recursive calls}) etc. So, the question is: Is it possible to have a purely functional and tractable description of DFS? I did a Google on "Haskell DFS", and landed up with a paper [1], that also says that Graph Algorithms have been difficult to implement in a purely functional style. They use mutable arrays to achieve the same. I am getting a small idea using foldls and Monads to achieve this. Since, we have to take the return value of the previous instance of the function call, and then pass it on to the next. dfs initial_visited_list >>= \spanning_tree -> dfs (merge spanning_tree initial_visited) >>= \spanning_tree -> etc... I will try to write it down on paper and see if it works out. References: [1]: www.cse.ogi.edu/~jl/Papers/dfs.ps Do you have any thoughts on this? Thanks, -- ~Vimal RLE :) encode = map (length &&& head) . group decode = concatMap (uncurry replicate)

2 3

Tutorial: Curry-Howard Correspondence
by Tim Newsham 18 Oct '07

18 Oct '07

A tutorial on the Curry-Howard Correspondence in Haskell: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ Feedback appreciated. Tim Newsham http://www.thenewsh.com/~newsham/

14 27

Re: [Haskell-cafe] On the verge of ... giving up!
by Andrew Coppin 18 Oct '07

18 Oct '07

Steven Fodstad wrote: > > FWIW, other people feel about Haskell the way you feel about calculus > and the continuation monad, and your opinions of these other powerful, > but difficult, tools is what got you into this mess. On the contrary, other people's misinterpretation of my opinions on these matters is what got me into this mess. I could go into a lengthy explanation, but I'll probably just be misunderstood again. So let's leave it here. > academics don't like hearing that their life's work is useless. > Being positively surrounded by people who think Haskell is pointless, I certainly have I fair idea how that feels...

1 0

Bug in runInteractiveProcess?
by John Goerzen 18 Oct '07

18 Oct '07

Hi everyone, I have been trying to implement a Haskell-like version of shell pipelines using runInteractiveProcess. I am essentially using hGetContents to grab the output from one command, and passing that to (forkIO $ hPutStr) to write to the next. Slow, but this is just an experiment. This works OK to link together two external commands, but deadlocks when linking together three processes. After staring at straces all afternoon, I think I have found the culprit. I observed that when I have three commands linked together, the second never sees EOF on its input. This even though I saw an explicit close on the other end of the pipe from the Haskell side. Why is this, I wondered? I stared at the source for the C runInteractiveProcess function for a bit, but then the answer was right there: this function does not sanitize FDs. What that means is that the write end of the stdin pipe for command 2 was open in the Haskell process. The Haskell process then forked off for command 3 later on. This write end of the stdin pipe for command 2 was never closed in the command 3 child environment. Therefore, closing it in the Haskell thread did not cause command 2 to get an EOF. Does that make sense? Many systems will just try to close *all* FDs except the ones they need after a fork(). Another approach would be to maintain a global list of FDs that the Haskell thread is using, and close all of them except the pipe ends in the child. Without something like this, it is not possible to use runInteractiveProcess more than twice simultaneously in a single program. That renders it almost useless for some tasks. Does this make sense to everyone? If so, I'll submit the bug on GHC. -- John

7 18

Re: [Haskell-cafe] Tutorial: Curry-Howard Correspondence
by Dan Weston 18 Oct '07

18 Oct '07

_|_ does not provide a witness to a theorem in any consistent logic (otherwise everything could be proved from it), yet it inhabits every type in Haskell. If the only invalid type instance is _|_, then a necessary and sufficient test for the C-H correspondence be the existence of a type instance that halts. Non-strict constructors would seem to mess that up. From http://en.wikipedia.org/wiki/Curry%E2%80%93Howard#Types "The problem of finding a ?-expression with a particular type is called the type inhabitation problem. The answer turns out to be remarkable: There is a closed ?-expression with a particular type only if the type corresponds to a theorem of logic, when the ? symbols are re-interpreted as meaning logical implication." By inhabit, they clearly mean no occurrence (recursively) in the type instance of _|_. I think the extra wrinkle you are introducing with constructors like Prop to wrap types is justified only insofar as the boxed and unboxed types are isomorphic, but they are not unless the constructor is strict in all its arguments. Just as _|_ :: a does not qualify as justifying theorem a, so in isomorphism Prop _|_ :: Prop a should also not qualify. If all constructors were strict, Prop _|_ = _|_ and all is fine. I am posting this to the haskell-cafe list because I am not at all sure that my understanding is right, and I don't want you to change your tutorial if it's not. Dan Weston Tim Newsham wrote: >> Also, I was wondering if the constructor and/or function arguments >> should be marked strict. >> >> Otherwise, types can be inhabited by defined arguments. Since Prop is >> not strict in its argument, we could have the (false) theorem >> >> andAlwaysTrue :: forall p q . p :/\ q >> andAlwaysTrue p q = And (Prop undefined) (Prop undefined) >> >> This halts for all p and q since Prop and And are not strict. > > Hmm.. I'm wondering to what degree this would make a difference. > I'm not actually running any of these programs. I'm just compiling > them and relying on the type checker to validate the types (and > check the proofs). If I understand this correctly, adding "!" > wont affect the behavior of the type checking phase. > >> Dan Weston wrote: >>> That is a great tutorial. Thanks! But in the last two sentences of >>> the introduction you say: >>> >>> > We just need to find any program with the given type. >>> > The existence of a program for the type will be a proof >>> > of the corresponding proposition! >>> >>> Maybe you should make explicit that >>> >>> 1) the type is inhabited >>> >>> undefined :: forall p . p >>> >>> does not prove that all propositions are true >>> >>> 2) the function must halt for all defined arguments >>> >>> fix :: forall p . (p -> p) -> p >>> fix f = let x = f x in x >>> >>> does not prove the (false) theorem >>> >>> (p => p) => p >>> >>> even though (fix id) is well-typed and id is certainly not undefined >>> (though fix id is). >>> >>> Tim Newsham wrote: >>>> A tutorial on the Curry-Howard Correspondence in Haskell: >>>> http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ >>>> >>>> Feedback appreciated. >>>> >>>> Tim Newsham >>>> http://www.thenewsh.com/~newsham/ >>>> _______________________________________________ >>>> Haskell-Cafe mailing list >>>> Haskell-Cafe(a)haskell.org >>>> http://www.haskell.org/mailman/listinfo/haskell-cafe >>>> >>>> >>> >>> >> >> > > Tim Newsham > http://www.thenewsh.com/~newsham/ > >

2 1