July 2014 - Haskell-Cafe

Doctest, quickcheck and typeclass
by Gautier DI FOLCO 14 Jul '14

14 Jul '14

Hi all, Is there a way, with doctest and quickcheck, to declare test at typeclass level (such as laws) and play them automatically at instance level? For example: -- | Convert from/to a List to/from an arbitrary data structure -- -- >>> prop > fromList . toList == id class Listable d where fromList :: [a] -> d a toList :: d a -> [a] And this test will be played for each instance. Thanks in advance for your help.

2 2

how to get ghci to load compiled modules in 7.8?
by Evan Laforge 14 Jul '14

14 Jul '14

I recently upgraded to 7.8.2 and I have a silly question. How do you get ghci to load compiled modules? When I try this: % cat >T.hs module T where x :: Int x = 42 % ghc -c -dynamic-too T.hs % s T.dyn_hi T.dyn_o T.hi T.hs T.o % ghci GHCi, version 7.8.2: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Loading package filepath-1.3.0.2 ... linking ... done. Prelude> :l T [1 of 1] Compiling T ( T.hs, interpreted ) Ok, modules loaded: T. *T> It still loads the file interpreted, even though there is a .dyn_o present. What am I doing wrong? This is on x86-64 OS X.

1 1

How to walk under binders "for free" in 'bound'?
by Christiaan Baaij 14 Jul '14

14 Jul '14

Dear list, I'm trying to implement a small dependently typed language (based on [1]) using the generalised De Bruijn indices from the 'bound' library [2]. My main two datatypes are: > data Binder n a > = Lam {binder :: Name n a} > | Pi {binder :: Name n a} Representing my two types of binders, and: > data Term n a > = Var !a > | Universe Integer > | App !(Term n a) !(Term n a) > | Bind !(Binder n (Term n a)) !(Scope (Name n ()) (Term n) a) Representing terms. My problem lies with implementing type-inference for lambda-binders. Originally I started with: > inferType1 :: Eq a > => (a -> Term n a) -- ^ Context > -> Term n a -- ^ Term > -> Term n a -- ^ Inferred type > inferType1 ctx (Var a) = ctx a > inferType1 ctx (Bind (Lam b) s) = Bind (Pi b) s' > where > s' = toScope . inferType1 ctx' . fromScope $ s > ctx' = unvar bCtx fCtx > bCtx _ = fmap F $ extract b > fCtx = fmap F . ctx Where `toScope . inferType1 ctx' . fromScope` entails doing three subsequent traversals: - `fromScope` traverses the term in `s`, which quotients placements of 'F' distributing them to the leaves - `inferType ctx'` then traverses the result of `fromScope` to infer the type - `toScope` transforms the inferred type to a generalised De Bruijn form, requiring a full tree traversal. Also, the new context, `ctx'`, is defined in term of a traversal (fmap). Also note that, for every Scope I walk under, `ctx'` gets an additional traversal. Doing so many traversals seems/is expensive, so after some thinking I improved `inferType2` to: > inferType2 ctx (Bind (Lam b) s) = Bind (Pi b) s' > where > s' = Scope . inferType2 ctx' . unscope $ s > ctx' = unvar bCtx fCtx > bCtx _ = fmap (F . Var) . extract $ b > fCtx = fmap (F . Var) . inferType2 ctx Where the only traversal needed to get `s'` is done by `inferType ctx'`. However, the new context, `ctx'`, remains defined in terms of traversals (fmap). Again, note that, for every Scope I walk under, `ctx'` gets an additional traversal. I could get rid of the remaining traversals in `ctx'` by implementing `inferType3` as: > inferType3 ctx (Bind (Lam b) s) = Bind (Pi b) s' > where > s' = Scope . inferType3 ctx' . unscope $ s > ctx' = unvar bCtx fCtx > bCtx _ = Var . F . extract $ b > fCtx = Var . F . inferType3 ctx But if I do that I start running into problems elsewhere, because the context is now returning lifted expressions. These problems arise for example in `inferPi`, which checks if the type of a term is a pi-binder: > inferPi :: Eq a > => (Term n a -> Term n a) -- ^ Type inference function > -> Term n a > -> (n,Term n a,Scope (Name n ()) (Term n) a) > inferPi inferTy tm = case inferTy tm of > Bind (Pi b) s -> (name b, extract b, s) > t -> error "Function expected" Let's assume that I'm doing type inference for the term: > \(a:*).\(b:*).\(f:(pi(_:a).b).\(x:a).f x Where `*` is `Universe 0`. In the application `f x`, I need to determine if `f` has a pi-type. When using either `inferType` or `inferType2`, I will see that `f` has the shape: > Bind (Pi {binder = Name "_" (Var (F (Var (F (Var (F (Var (B (Name "a" ())))))))))}) > (Scope (Var (F (Var (F (Var (F (Var (B (Name "b" ())))))))))) And so, `inferPi` will have no problems seeing that `f` has a pi-type. However, when using `inferType3`, where the context, `ctx`, returns lifted expressions , `f` has the shape: > Var (F (Var (F (Bind (Pi {binder = Name "_" (Var (F (Var (B (Name "a" ())))))}) > (Scope (Var (F (Var (B (Name "b" ())))))))))) Now `inferPi` will have problems seeing that `f` has a pi-type, it will need to quotient out and distribute the (Var . F) first. The (non-)solution is to quotient and distribute on demand, by defining `inferType4`: > inferType4 :: Eq a > => (a -> Term n a) -- ^ Context > -> (Term n a -> Term n a) -- Quotient and distribute (Var . F) > -> Term n a -- ^ Term > -> Term n a -- ^ Inferred type > inferType4 ctx dist (Var a) = dist (ctx a) > inferType4 ctx dist (Bind (Lam b) s) = Bind (Pi b) s' > where > s' = Scope . inferType4 ctx' dist' . unscope $ s > ctx' = unvar bCtx fCtx > bCtx _ = Var . F . extract $ b > fCtx = Var . F . inferType4 ctx dist > > dist' (Var (F a)) = fmap (F . Var) . dist $ a > dist' e = e However, `inferType4` simply moves the traversal from one place to the other, giving us no improvement over `inferType2`. What we do however see is that, after having descended two Scopes, we would get a `dist'` function that does: > fmap (F . Var) . fmap (F . Var) . dist This gives me hope that instead of having to do two traversals using `fmap`, we could get one traversal of the form: > fmap (F . Var . F . Var) . dist According to the Functor law. I have absolutely no idea how to achieve this single traversal solution though. This leads me to have several, quite general, questions: - Is there a way to get a `dist` function, as defined in `inferType4`, that does a single traversal? - Would it be possible to even get rid of the traversal for the context `ctx`? Perhaps by approaching the `inferType` function completely differently? - Or is there simply no way to implement `inferType` for free (without traversals) using generalised De Bruijn indices? The complete code can be found at: https://gist.github.com/christiaanb/4e0fd1777aee927999aa Cheers, Christiaan Baaij [1] http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ [2] http://hackage.haskell.org/package/bound-1.0.3

1 0

ANN: HacBerlin - Haskell Hackathon in Berlin, 26-28 Sep 2014
by Stefan Wehr 14 Jul '14

14 Jul '14

Dear Haskellers, another Haskell Hackathon is waiting for you! Where: Berlin, Germany When: Fri 26 - Sun 28 September 2014 Meet in Berlin, discuss, hack together and improve the Haskell infrastructure. We welcome all programmers interested in Haskell, beginners and experts! For all details, visit our wiki page (http://www.haskell.org/haskellwiki/HacBerlin2014) and make sure to register early. By the way: we are currently looking for one or two keynote talks. If you feel qualified, please let us know. Happy hacking, Stefan

1 0

book "Haskell Data Analysis Cookbook" by Nishant Shukla
by Vasili I. Galchin 14 Jul '14

14 Jul '14

I believe there is a non-thread safe code fragment in Chapter 1(page 15): import System.Directory (doesFileExist) ..... exist <- doesFileExist filename -- these two lines are non-thread safe .. yes?? to be thread-safe the above line and the following line would have to be together atomic .... input <- if exists then readFile filename else return "" ........... Vasili

3 4

What is the state of the art in testing code generation?
by Tom Ellis 14 Jul '14

14 Jul '14

I am implementing an EDSL that compiles to SQL and I am wondering what is the state of the art in testing code generation. All the Haskell libraries I could find that deal with SQL generation are tested by implementing multiple one-off adhoc queries and checking that when either compiled to SQL or run against a database they give the expected, prespecified result. * https://github.com/prowdsponsor/esqueleto/blob/master/test/Test.hs * https://github.com/m4dc4p/haskelldb/blob/master/test/TestCases.hs * https://github.com/yesodweb/persistent/blob/master/persistent-test/SumTypeT… I couldn't find any tests for groundhog. * https://github.com/lykahb/groundhog I also had a look at Javascript generators. They take a similar adhoc, one-off approach. * https://github.com/valderman/haste-compiler/tree/master/Tests * https://github.com/faylang/fay/tree/master/tests Is this the best we can do in Haskell? Certainly it seems hard to use a QuickCheck/SmallCheck approach for this purpose. Is there any way this kind of testing can be automated or made more robust? Thanks, Tom

6 10

Diony Rosa - 7/14/2014 2:14:04 AM
by Diony Rosa 13 Jul '14

13 Jul '14

http://butikpastalar.net/rhad/cfttllmcrlpibdgdyufrzbhvsd.aucahicfstvtogdrs

1 0

[ANN] cabal-bounds 0.7: update bounds by haskell platform release
by Daniel Trstenjak 13 Jul '14

13 Jul '14

Hi cafe, cabal-bounds[1] is a command line program for managing the bounds/versions of the dependencies in a cabal file. cabal-bounds 0.7 adds the feature to set the bounds of dependencies to the library versions used by a haskell platform[2] release. For further details please consult the README[3]. Greetings, Daniel [1] https://github.com/dan-t/cabal-bounds [2] https://www.haskell.org/platform/ [3] https://github.com/dan-t/cabal-bounds/blob/master/README.md

1 0

Re: [Haskell-cafe] book "Haskell Data Analysis Cookbook" by Nishant Shukla
by Vasili I. Galchin 12 Jul '14

12 Jul '14

well .. if my memory is correct .. a previous example was based on using an exemption to make the code safe (.. found it on pg. 14) ..... i was just being lazy(my total bad) .. not being stupid .. ... in any case, aren't books refereed ....not impugning the author .. hey I make mistakes .. e.g. working too fast .. too much booze the night before ... :-)

1 0

[ANNOUNCE] New release of SBV (v3.1)
by Levent Erkok 12 Jul '14

12 Jul '14

I'm pleased to announce v3.1 release of SBV, a library for integrating SMT solvers into Haskell. This release coincides with GHC 7.8.3: A a prior bug in the 7.8 series caused SBV to crash under heavy load. GHC 7.8.3 fixes this bug; so if you're an SBV user, please upgrade to both GHC 7.8.3 and your version of SBV. Also new in this release are two oft-requested features: - Parallel solving capabilities: Using multiple SMT solvers at the same time to get the fastest result (speed), or get all results (to make sure they all behave the same way, safety). - A variant of symbolic if-then-else (called sBranch) that can call the external solver during simulation before it symbolically simulates "then" and "else" branches. This is useful for programming with recursive functions where termination depends on symbolic values. Full release notes: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md SBV web page: http://leventerkok.github.io/sbv/ As usual, bug reports and feedback are most welcome! -Levent.

1 0