- Haskell-Cafe - Haskell.org

OSX, ghci, dylib, what is the correct way?
by Jason Dagit 23 Jun '11

23 Jun '11

Hello, I also asked this question on SO: http://stackoverflow.com/questions/6323755/osx-ghci-dylib-what-is-the-corre… I wonder where I'll get more/better answers? Read on for the question. Thanks! Jason I need to build some C code and then reference that C code via the FFI. I would like to use my binding from inside ghci on osx. On of my constraints is that I cannot just hand the C sources to ghc in the .cabal file. This is due to a limitation with ghc/cabal that may be fixed in the next release of ghc (but I want my code to work now and on older releases). See this [bug for details][1]. The gist of that bug is that the C code needs to be compiled with some Objective-C modules and ghc misinterprets those as linker scripts. I've tried many things and building the files myself with a makefile is the only thing that has worked. Really, this shouldn't be an issue though because it should be the same as if I decided to use a external C library that I didn't build myself. For the sake of this issue, let's pretend it's a separate C library that I can easily rebuild with different options. If I build the C library as a .a, then ghci comlains that it cannot open the .dylib. My first question is: Why does ghci need a .dylib and does it really use it? When I build a dylib I get a [segfault when loading the code into ghci][2]. Keep in mind, this binding works already on other platforms, both linux and windows, and the binding works fine on osx when I'm compiling instead of using ghci. This problem specific to the osx/ghci combo. In that trace above, I'm using gdb but it crashes regardless of whether I use gdb. I tracked it down to the lines that cause the crash: void _glfwClearWindowHints( void ) { memset( &_glfwLibrary.hints, 0, sizeof( _glfwLibrary.hints ) ); } The trouble maker is that memset line, well actually the problem is that when running inside ghci writing to the hints structure of `_glfwLibrary` is a memory access violation. The hints struct is simply a bunch of ints. It's very flat and simple, and thus I think the problem is an issue either with how I'm linking things or with the way ghci is loading the code. Here are the bits of my makefile that I use to build the dylib and the .a: GCCFLAGS := $(shell ghc --info | ghc -e "fmap read getContents >>= \ putStrLn . unwords . read . Data.Maybe.fromJust . lookup \ \"Gcc Linker flags\"") FRAMEWORK := -framework Cocoa -framework OpenGL GLFW_FLAG := $(GCCFLAGS) -O2 -fno-common -Iglfw/include -Iglfw/lib \ -Iglfw/lib/cocoa $(CFLAGS) all: $(BUILD_DIR)/static/libglfw.a $(BUILD_DIR)/dynamic/libglfw.dylib $(BUILD_DIR)/dynamic/libglfw.dylib: $(OBJS) $(CC) -dynamiclib -Wl,-single_module -compatibility_version 1 \ -current_version 1 \ $(GLFW_FLAG) -o $@ $(OBJS) $(GLFW_SRC) $(FRAMEWORK) $(BUILD_DIR)/static/libglfw.a: $(OBJS) ar -rcs $@ $(OBJS) Most of the flags are taken straight from the GLFW Makefile so I think they should be correct for that library. The first line looks a bit weird but it's the solution I used for this [problem][3]. Platform details: - OSX 10.6.6 - x86_64 - 4 cores - GHC version 7.0.3 installed via Haskell Platform installer - Source repo: https://github.com/dagit/GLFW-b [1]: http://hackage.haskell.org/trac/ghc/ticket/5025 [2]: http://hpaste.org/47457/segfault_in_ghci [3]: http://stackoverflow.com/questions/6217406/how-can-i-detect-if-ghc-is-set-t…

4 10

Darcs 2.8 beta 1 is available
by Florent Becker 23 Jun '11

23 Jun '11

Hi cafe-dwellers, On behalf of the darcs team, I'm pleased to announce the release of darcs 2.8 beta 1. This new darcs is just one cabal install away from you, as you can install it by: -cabal update -cabal install darcs-beta (note this will create an executable named "darcs", not darcs-beta). You can then come back to your usual darcs if you needby -cabal install --reinstall darcs Alternatively, you can get the source tarball from here: http://hackage.haskell.org/packages/archive/darcs-beta/2.7.98.1/darcs-beta-…. More information on the release is available at http://wiki.darcs.net/Releases/2.8 This is a beta, so bug reports are very welcome. Highlights of this new version of darcs are: - a faster and much more readable annotate. - you can use darcs optimize --http to make darcs get from your repository over http much faster - you can now use darcs obliterate -o bundle.dpatch to save some patches into a bundle while unpulling them. This allows to stash these patches away while you do something else. - rollback now has a --no-record option which allows to undo some changes from a past patch without recording that as a new patch straight away. - end of write support of "old-fashionned" repositories. These repositories are the one darcs-1 used to create, and they have been replaced by the new "hashed" repositories since darcs-2. You can still use get, pull and so on from these repositories, but darcs 2.8 will refuse to write to them. Enjoy your new darcs, The darcs team

1 0

Quickcheck: Help on non trivial test
by jean-christophe mincke 23 Jun '11

23 Jun '11

Hello Café, I am using quicheck for some kind of non trivial tests. The general form of these tesst is summarized by the following code. -- Function to be tested. Given a list of splitting functions, split the given list process :: [a] -> [[a] -> [a]] -> [a] process l splitFuns = List.foldl proc l splitFuns where proc l splitFun = splitFun l -- a split function generator splitFunGen :: Gen ([a] -> [a]) splitFunGen = return $ proc where proc l = let splitPos = List.length l `div` 2 -- Problem I would like splitPos = some random value between [0 and length of l] in fst $ List.splitAt splitPos l splitFunsGen :: Gen [[a] -> [a]] splitFunsGen = vectorOf 20 splitFunGen instance Show a => Show ([a] -> [a]) where show _ = " a split fun " r = quickCheck $ forAll splitFunsGen prop where prop splitFuns = let l = process [1..100] splitFuns in List.length l >= 0 -- dummy test here for the sake of example The process to be tested takes a list that is randomly perturbated (spitFuns). The result of each perturbation is fed into the next perturbation. Ideally I would like the perturbating function to depend on the previous perturbated list (see computation of splitPos in splitFunGen). I am not sure how I could use quickcheck in this case. Has anyone a better idea? Thanks J-C

2 1

Re: [Haskell-cafe] Category theory as a design tool
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/22/11 3:59 PM, Arnaud Bailly wrote: > Hello Greg and Alexander, > Thanks for your replies. Funnily, I happen to own the 3 books you mentionned > :-) My interest in category theory is a long standing affair... > > Note that owning a book, having read (most of) it and knowing a theory (or > at least its principles and main concepts) is really quite a different thing > from being able to apply it. One of the big benefits I see to using category theory for dealing with programming languages comes from using CT as a generalized logic for equational reasoning. In particular, making use of the ideas of (co)limits and adjunctions in order to prove that something must behave in a particular way. This requires a bit of work to contort your thinking into the patterns of CT, but it means that once you can prove that something is a foo, then all the theorems about foos will apply. Just having a diagram and knowing it commutes doesn't tell you a whole lot, it just says that one particular equation holds. The real power comes from looking at diagrams that are parametric (since then proving it holds will mean it holds for all parameter valuations), or looking at diagrams where one of the arrows is (essentially) unique (since then you can show things that look like foos actually are foos). That is, the real power of diagrams comes from the quantifiers, which are explained in the text rather than shown in the diagram itself. As an example of this approach, see my comments in the thread about anonymous sum types. For something to be a product means that a particular diagram commutes: namely, a product is the limit of the two point category (and coproducts are the colimit). One of the many things this tells us is that if we posit that A*A ~ A in a category that "has products", we must infer that the category is a meet-(pre)semilattice[1]. [1] Or a really goofy structure where for every A and B there are at most two A->B, with a canonical way of distinguishing them. Of course, for this to be a category we need to define a composition operator, which will take the four compositions into the two possible arrows, which is where it gets strange. -- Live well, ~wren

3 2

Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/22/11 6:00 PM, Casey McCann wrote: > On Wed, Jun 22, 2011 at 2:19 PM, wren ng thornton<wren(a)freegeek.org> wrote: >>>> [1] modulo the A:+:A ~ A issue. >> >> Oops, I should've said A:*:A there. >> >>> That issue is exactly my concern, though, and it seems a bit too >>> thorny to handwave aside. >> >> Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. > (...) > > Thank you, that clarified my intuitive sense of why it didn't seem to > work. The same argument, with arrows flipped appropriately, would > apply to a hypothetical coproduct where A :+: A ~ A, wouldn't it? It should. But let's make sure... A coproduct of A and B is an object A+B along with morphisms inl :: A -> A+B and inr :: B -> A+B, such that for any object C and morphisms c1 :: A -> C and c2 :: B -> C, there exists a unique c1|||c2 :: A+B -> C such that c1|||c2 . inl = c1 and c1|||c2 . inr = c2. All of this is the straightforward dualizing of products. So, lets assume A ~ A+A. And lets assume we have some functions inl and inr. Now, for every pair of functions f, g :: A -> C we must come up with a unique function h :: A+A -> C such that h . inl = f and h . inr = g. By isomorphism this is the same as coming up with a unique function h' :: A -> C such that h' . iso . inl = f and h' . iso . inr = g. If inl = inr, then it follows that f = g. Consequently there can only be one morphism between any two objects, so the category is a preorder. If the category has all coproducts then it's a join-semilattice--- exactly dual to the meet-semilattice case for products. If we want a category more interesting than a preorder, then we must have that inl and inr are different. We must find two injection functions which keep their images in A+A apart, so that we can define partial functions -|||g and f|||- which don't conflict with each other (so that they can be combined into the total function f|||g). The obvious way to do that is to use tagged/disjoint unions, but we can't do that since we've assumed A ~ A+A. Basically, the type A+A isn't big enough (whereas before, the values of type A*A weren't big/informative enough). I'm playing a bit fast and loose with the notion of "big/informative enough". Perhaps someone more familiar with large ordinals can come up with a counter example. But if they do, I'm sure it wouldn't be a very intuitive place to program in. -- Live well, ~wren

1 0

Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/21/11 10:48 PM, Casey McCann wrote: > On Tue, Jun 21, 2011 at 9:51 PM, wren ng thornton<wren(a)freegeek.org> wrote: >> I don't think there are any problems[1]. > (...) >> [1] modulo the A:+:A ~ A issue. Oops, I should've said A:*:A there. > That issue is exactly my concern, though, and it seems a bit too > thorny to handwave aside. Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. The reasoning is as follows. An object A*B with morphisms fst :: A*B->A and snd :: A*B->B is a product iff for all objects P with morphisms p1 :: P -> A and p2 :: P -> B, there is a unique morphism p1&&&p2 :: P -> A*B, such that p1 = fst . p1&&&p2 and p2 = snd . p1&&&p2. Given the definition, if we further say that A*A ~ A, then it's clear that we can't come up with any satisfactory definitions of fst and snd which obey the laws--- unless there can be only one morphism between any two objects, in which case we know that p1 = p2 and so it's okay for fst = snd; or unless there can be only two morphisms between any two objects and we have a canonical property for distinguishing them so that we can correlate p1 with fst and p2 with snd. In all other cases, there are simply too many possible choices of p1 and p2, and there's no way for fst and snd to carry enough information to make the equations hold. What that means then is that the category which tries to use :*: to make products would only have products in the cases where the first and second component are different; which would be a strange category indeed. Alternatively, it could always have products but would only allow one morphism between objects; in which case the category is just a meet-semilattice (actually, the preorder generalization thereof). > In contrast, ordered pairs and disjoint unions are tidy, simple, and obvious. Disjoint pairs are sufficient; they needn't be ordered. All we need is that they are "tagged" in the same way that disjoint unions are, so that we can distinguish the components of A*A. -- Live well, ~wren

5 5

Graph diagram tools?
by Dmitri O.Kondratiev 23 Jun '11

23 Jun '11

Hi, I am looking for Haskell library to create graph diagrams in png or similar formats. Thanks!

4 3

Re: [Haskell-cafe] category theory as a design tool
by Brett Giles 22 Jun '11

22 Jun '11

Hi Arnaud, you may want to look at http://mathcs.mta.ca/research/rosebrugh/Easik/ This is a java tool which allows entity design using various cat theory constraints such as sum, product and pullbacks. Brett Giles Sent from my iPhone > Message: 14 > Date: Wed, 22 Jun 2011 14:06:21 -0500 > From: Gregg Reynolds <dev(a)mobileink.com> > Subject: Re: [Haskell-cafe] Category theory as a design tool > To: Arnaud Bailly <arnaud.oqube(a)gmail.com> > Cc: Haskell Cafe <haskell-cafe(a)haskell.org> > Message-ID: <BANLkTingApLo7ysYGgg1DUxbW5iK1kLmrQ(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > On Tue, Jun 21, 2011 at 11:30 PM, Arnaud Bailly <arnaud.oqube(a)gmail.com> > wrote: >> (2nd try, took my gloves off...) >> Hello Caf?, >> I have been fascinated by Cat. theory for quite a few years now, as >> most people who get close to it I think. >> >> I am a developer, working mostly in Java for my living and dabbling >> with haskell and scala in my spare time and assuming the frustration >> of having to live in an imperative word. More often than not, I find >> myself trying to use constructs from FP in my code, mostly simple >> closures and typical data types (eg. Maybe, Either...). I have read >> with a lot of interest FPS (http://homepages.mcs.vuw.ac.nz/~tk/fps/) >> which exposes a number of OO patterns inspired by FP. >> >> Are there works/thesis/books/articles/blogs that try to use Cat. >> theory explicitly as a tool/language for designing software (not as an >> underlying formalisation or semantics)? Is the question even >> meaningful? > > You might try: Category Theory for Computing > Science<http://www.cwru.edu/artsci/math/wells/pub/ctcs.html> (Barr > and Wells) > > and Conceptual Mathematics: a first introduction to > categories<http://books.google.com/books/about/Conceptual_mathematics.html?id=o1tHw4W5…> > (Lawvere) > > "Kinship and Mathematical Categories" (by Lawvere) is also interesting. > > -Gregg > >> >> Thanks in advance, >> Arnaud >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe(a)haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >

1 0

Homework help - calculator function
by SM Design 22 Jun '11

22 Jun '11

I have a homework which is very important to be done but I can't complete the task at all. The program i should write is: Make calculator- function in Haskell. The function argument is a list of strings and also form such list, as each string of the argument made definite action. • If the string has the form of an arithmetic expression - calculate this expression. The string result becomes part of the list- result. If the expression contains a variable which is not assigned value, the result is displayed "undefined". • If the string has the form Name = value calculated from the last expression is assigned to the variable with the corresponding name in the list, and in the result list is formed a string with type name = ... where the site stands blank corresponding value. If there is not a calculated expression to be assigned to form a string "no value". • If the string is non-blank, but there is a species different from the above two case, form the string "error". • If the string is empty, incl. when it contains only spaces, in the result there is not form a string. Expressions consist of integers without sign variables, operations + (Addition), - (subtraction), * (multiplication) and / (divide) and parentheses. Where no brackets, the operations are performed from left to right, but * and / precede the + and -. Implementation of any operation gives integer; in the division rejected the fractional part , if any . Variables have names of one letter - from the Latin small letter . In the beginning, end or between the elements of each row can have spaces - they are irrelevant to its correctness. Example: the list-argument ["3 +7 / 2" "2 + x", "= s", "2 * s +4", "", "2 + +4 / 5] function should provide a result-list ["6", "undefined", "s = 6", "16", "error"]. Thank you an advance!

4 3

Verifying Haskell programs vs. generating verified Haskell programs
by Uli Kastlunger 22 Jun '11

22 Jun '11

Hello Haskell fellows, recently there has been a huge progress in generating real programs by specifying them in interactive theorems prover like Isabelle or Coq, in particular a verified C Compiler has been generated out of a specification in Coq [0]. Furthermore it is often stated, that it is easier to reason about functional languages. So in my opinion there are two approaches building verified software (e.g. in case of compilers: verify that the semantics of a high-level language maps correctly to the semantics of a low-level language). (0) Programming in any language and then verifying it with an external theorem prover (1) Specifying the program in a proof language and then generating program code out of it (like in the CompCert project) I think both ideas have their (dis)advantages. The question is, which concept will be used more frequently? In particular how hard would it be to build something like CompCert the other way around (in this case writing a C compiler in SML and proving its correctness?) Best regards, Uli Kastlunger [0] http://compcert.inria.fr/

4 5