August 2009 - Haskell-Cafe

Suggestion: define a standard keyboard codes library?
by Peter Verswyvelen 26 Aug '09

26 Aug '09

Several libraries define their own codes for they keyboard (GLFW, GTK, GLUT, etc) Maybe it would be nice to agree on a standard datatype for keys? This might also include digital buttons on a joystick, etc... The Windows API has virtual key codes for this.

3 5

Is it possible to prove type *non*-equality in Haskell?
by Ryan Ingram 26 Aug '09

26 Aug '09

Short version: How can I get from (Z ~ S n) to a useful contradiction? Type equality coercions[1] let us write proofs in Haskell that two types are equal: > {-# LANGUAGE GADTs, RankNTypes, TypeFamilies #-} > {-# OPTIONS_GHC -Wall #-} > module TEq where > data TEq a b = (a ~ b) => TEq This provides all the expected properties for equality: > refl :: TEq a a > refl = TEq > symm :: TEq a b -> TEq b a > symm TEq = TEq > trans :: TEq a b -> TEq b c -> TEq a c > trans TEq TEq = TEq Here's an example use: > data Z = Z > newtype S n = S n > data Nat a where > Nz :: Nat Z > Ns :: Nat x -> Nat (S x) > proveEq :: Nat a -> Nat b -> Maybe (TEq a b) > proveEq Nz Nz = return TEq > proveEq (Ns a) (Ns b) = do > TEq <- proveEq a b > return TEq > proveEq _ _ = Nothing But if you get "Nothing" back, there's no proof that the two types are in fact non-equal. You can use "_|_ as negation": > newtype Not p = Contr { contradiction :: forall a. p -> a } > > nsymm :: Not (TEq a b) -> Not (TEq b a) > nsymm pf = Contr (contradiction pf . symm) We know by parametricity that "contradiction n p" isn't inhabited as its type is (forall a. a) But I can't figure out a way to write this without "error": > notZeqS :: forall n. Not (TEq Z (S n)) > notZeqS = Contr (\x -> x `seq` error "impossible") As a first step, I'd like to write this: > -- notZeqS = Contr (\TEq -> error "impossible") but the compiler complains immediately about the pattern match being unsound: TEq.lhs:39:20: Couldn't match expected type `S n' against inferred type `Z' In the pattern: TEq In the first argument of `Contr', namely `(\ TEq -> error "impossible")' In the expression: Contr (\ TEq -> error "impossible") Is there any way to use the obvious unsoundness we get from (Z ~ S n) to generate a contradiction? Ideally I'd like to be able to implement ] natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b)) as follows: > predEq :: TEq (f a) (f b) -> TEq a b > predEq TEq = TEq > natEqDec :: Nat a -> Nat b -> Either (TEq a b) (Not (TEq a b)) > natEqDec Nz Nz = Left TEq > natEqDec (Ns a) (Ns b) = case natEqDec a b of > Left TEq -> Left TEq > Right pf -> Right $ Contr $ \eq -> contradiction pf (predEq eq) > natEqDec Nz (Ns _) = Right notZeqS > natEqDec (Ns _) Nz = Right (nsymm notZeqS) Which compiles successfully, but the "error" call in "notZeqS" is a big wart. Is there a better implementation of "Not" that allows us to avoid this wart? -- ryan [1] http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/

3 3

Re: [Haskell-cafe] How to calculate de number of digits of an integer? (was: Is logBase right?)
by George Pollard 26 Aug '09

26 Aug '09

2009/8/26 Lennart Augustsson <lennart.augustsson(a)gmail.com>: > Try 10^1000 Cheat :)

1 0

oauth in haskell - reviewers?
by Diego Souza 26 Aug '09

26 Aug '09

Hi all, I wrote a small library in haskell do deal with oauth authentication. It turns out it is my first library in haskell as well. As I'm beginner in haskell, I'm asking for a review of someone more experienced/proficient before even daring to create a cabal pkg and dist it to hackage. :-) Any help/comments on this will be highly welcome. http://projects.bitforest.org/hoauth/ $ darcs get http://projects.bitforest.org/hoauth/ # should do the trick Thanks in advance, -- ~dsouza yahoo!im: paravinicius gpg key fingerprint: 71B8 CE21 3A6E F894 5B1B 9ECE F88E 067F E891 651E

5 10

FFI link failing due to no main?
by phil＠beadling.co.uk 26 Aug '09

26 Aug '09

Hi, After creating my stub objects etc using GHC, I'm trying to create a library with a C interface to some Haskell functions. I'm explicitly passing in -no-hs-main yet the linker still fails due to missing main? I'm sure I've had this working before with a slightly simpler example, but can't work out what is wrong here. If I give it a main (to humor it - it's not a solution), then it links and produces an executable - so it looks to me like I'm not telling the linker what I want correctly? Any ideas? Cheers, Phil. ghc -O2 --make -no-hs-main -package mtl -package array -optl '- shared' FFI/Octave/MyInterface.c FFI/Octave/OptionInterface_stub.o FFI/ Octave/OptionInterface.o ./FrameworkInterface.o ./Maths/Prime.o ./ MonteCarlo/DataStructures.o ./MonteCarlo/European.o ./MonteCarlo/ Framework.o ./MonteCarlo/Interface.o ./MonteCarlo/Lookback.o ./Normal/ Acklam.o ./Normal/BoxMuller.o ./Normal/Framework.o ./Normal/ Interface.o ./Random/Framework.o ./Random/Halton.o ./Random/ Interface.o ./Random/Ranq1.o -o FFI/Octave/libMyInterface.so Linking FFI/Octave/libMyInterface.so ... Undefined symbols: "___stginit_ZCMain", referenced from: ___stginit_ZCMain$non_lazy_ptr in libHSrts.a(Main.o) "_ZCMain_main_closure", referenced from: _ZCMain_main_closure$non_lazy_ptr in libHSrts.a(Main.o) ld: symbol(s) not found collect2: ld returned 1 exit status

1 0

How to convert a list to a vector encoding its length in its type?
by Bas van Dijk 25 Aug '09

25 Aug '09

Hello, We're working on a Haskell binding to levmar[1] a C implementation of the Levenberg-Marquardt optimization algorithm. The Levenberg-Marquardt algorithm is an iterative technique that finds a local minimum of a function that is expressed as the sum of squares of nonlinear functions. It has become a standard technique for nonlinear least-squares problems. It's for example ideal for curve fitting. The binding is nearly finished and consists of two layers: a low-level layer that directly exports the C bindings and a medium-level layer that wraps the lower-level functions and provides a more Haskell friendly interface. The Medium-Level (ML) layer has a function which is similar to: > levmarML :: (a -> [Double] -> Double) > -> [Double] > -> [(a, Double)] > -> [Double] > levmarML model initParams samples = ... So you give it a model function, an initial guess of the parameters and some input samples. levmarML than tries to find the parameters that best describe the input samples. Of course, the real function has more arguments and return values but this simple version will do for this discussion. Al-dough this medium-level layer is more Haskell friendly than the low-level layer it still has some issues. For example a model function is represented as a function that takes a list of parameters. For example: > \x [p1, p2, p3] -> p1*x^2 + p2*x + p3 You have to ensure that the length of the initial guess of parameters is exactly 3. Otherwise you get run-time pattern-match failures. So I would like to create a new High-Level (HL) layer that overcomes this problem. First of all I need the following language extensions: > {-# LANGUAGE EmptyDataDecls #-} > {-# LANGUAGE UndecidableInstances #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE GADTs #-} I want to represent the model function as a normal Haskell function. So instead of passing the parameters as a list I want to pass them as arguments: > \x p1 p2 p3 -> p1*x^2 + p2*x + p3 Because we would like to be able to use model functions of different arity it means the levmarHL function needs to be polymorphic in the model function: > levmarHL :: (ModelFunc f, Arity f ~ n, Arg f ~ Double) > => (a -> f) > -> Vector Double n > -> [(a, Double)] > -> Vector Double n > levmarHL model initParams samples = > fromList $ levmarML (\x params -> model x $* fromList params) > (toList initParams) > samples You can see that the initial parameters and the result are passed as Vectors that encode their length 'n' in their type. This length must equal the arity of the model function: 'Arity f ~ n'. The arity of the model function and the length of the vectors are represented as type level naturals: > data Z > data S n Lets look at the implementation of ModelFunc: > class ModelFunc f where > type Arg f :: * > type Arity f :: * > > ($*) :: f -> Vector (Arg f) (Arity f) -> Arg f $* is similar to $ but instead of applying a function to a single argument it applies it to a vector of multiple arguments. > instance (ModelFunc f, Arg f ~ b) => ModelFunc (b -> f) where > type Arg (b -> f) = b > type Arity (b -> f) = S (Arity f) > > f $* (x :*: xs) = f x $* xs You can see that we restrict the arguments of module functions to have the same type: 'Arg f ~ b'. This is the base case: > instance ModelFunc Double where > type Arg Double = Double > type Arity Double = Z > > d $* Nil = d We represent Vectors using a GADT: > data Vector a n where > Nil :: Vector a Z > (:*:) :: a -> Vector a n -> Vector a (S n) > infixr :*: Converting a Vector to a list is easy: > toList :: Vector b n -> [b] > toList Nil = [] > toList (x :*: xs) = x : toList xs My single question is: how can I convert a list to a Vector??? > fromList :: [b] -> Vector b n > fromList = ? regards, Roel and Bas van Dijk [1] http://www.ics.forth.gr/~lourakis/levmar/

9 21

ANN: gitit 0.6.1
by John MacFarlane 25 Aug '09

25 Aug '09

I'm pleased to announce the release of gitit 0.6.1. Gitit is a wiki program that runs on happstack, the Haskell web application server stack, and stores pages and other content in a git or darcs filestore. The wiki can be updated either directly through the VCS or through gitit's web interface. Pages can be written in (extended) markdown, reStructuredText, HTML, or LaTeX, and exported in ten different formats. TeX math is rendered using MathML by default, and syntax highlighting is provided for over fifty languages. demo: http://gitit.johnmacfarlane.net manual: http://gitit.johnmacfarlane.net/README api: http://hackage.haskell.org/package/gitit-0.6.1 code: http://github.com/jgm/gitit bugs: http://code.google.com/p/gitit/issues/list group: http://groups.google.com/group/gitit-discuss Here is how you can install and run gitit. You'll need GHC and cabal-install. If you don't have these, install the Haskell Platform <http://hackage.haskell.org/platform/>. Then: cabal update cabal install gitit mkdir mywiki cd mywiki gitit # now browse to http://localhost:5001 Or, if you want to change the defaults (say, reStructuredText instead of markdown, or darcs instead of git): gitit --print-default-config > gitit.conf # edit gitit.conf, which is self-documenting gitit -f gitit.conf The whole code base has been overhauled since the last release. Gitit is now faster, more memory efficient, more modular, and more secure. It also has many new features, including - page metadata and categories - atom feeds (sitewide and per-page) - support for literate Haskell - a better configuration system - an improved caching system - a Haskell library exporting happstack wiki handlers - a plugin system The last two items are the most exciting and deserve special comment. First, in addition to providing an executable, gitit now provides a library, Network.Gitit, which makes it easy to include a gitit wiki (or many of them) in any happstack application. It is even possible to use the containing application's authentication system for the wiki. Second, gitit can now be extended through plugins, short Haskell programs that are loaded dynamically when the server starts. For examples of the things that can be done with plugins, see the plugins directory, which contains (among other things) a plugin for adding graphviz diagrams to pages and a plugin for adding interwiki links. For a full description of the plugin system, see the haddock documentation for Network.Gitit.Interface. Full changes from version 0.5.3, as well as upgrade instructions, are available in the file CHANGES. Thanks are due to - the happstack team, for big improvements in happstack-server that make it much easier to work with, - the darcs team, for using gitit/darcsit for <http://wiki.darcs.net>, giving gitit a real-world test, - Gwern Branwen, who helped to optimize gitit, wrote the InterwikiPlugin, and wrote the guts of the Feed module, - Simon Michael, who contributed several patches, - Henry Laxen, who added support for password resets and helped with the apache proxy instructions, - Anton van Straaten, who made the process of page generation more modular by adding Gitit.ContentTransformer, - Robin Green, who helped improve the plugin API and interface, fixed a security problem with the reset password code, and made saving of the user's file more robust, - Thomas Hartman, who helped improve the index page, making directory browsing persistent, - Kohei Ozaki, who contributed the ImgTexPlugin, - mightybyte, who suggested making gitit available as a library, and contributed a patch to the authentication system, - and everyone else who contributed suggestions and bug reports.

4 3

ANN: epoll bindings 0.1.1
by Toralf Wittner 25 Aug '09

25 Aug '09

Hi, I am pleased to announce the release of epoll bindings 0.1.1 available from: http://hackage.haskell.org/package/epoll Epoll is an I/O event notification facility for Linux similar to poll but with good scaling characteristics. Currently the bindings are fairly low level and close to the C API. In the future I hope to add some buffer or stream abstraction on top. Eventually, when GHC can make use of epoll/kqueue etc. in addition to select, this library will not be needed anymore. Until then it might be useful for applications which monitor large numbers of file descriptors. -Toralf

1 0

Is logBase right?
by Roberto 25 Aug '09

25 Aug '09

Hi, There is a mistake is logBase: $ ghci GHCi, version 6.10.4: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. Prelude> logBase 10 10 1.0 Prelude> logBase 10 100 2.0 Prelude> logBase 10 1000 2.9999999999999996 <--- eeeerrgghhhh! Prelude> logBase 10 10000 4.0 My host is a Debian GNU/Linux 5.0.2 (lenny) with the following GHC packages: ii ghc6 6.10.4-1 ii ghc6-doc 6.10.4-1 ii libghc6-mtl-dev 1.1.0.2-7+b1 ii libghc6-utf8-string-dev 0.3.5-1+b1 ii libghc6-x11-dev 1.4.5-6 rc libghc6-x11-doc 1.4.2-1 ii libghc6-x11-xft-dev 0.3-3+b3 ii libghc6-xmonad-contrib-dev 0.8.1-3+b3 rc libghc6-xmonad-contrib-doc 0.8-2 ii libghc6-xmonad-dev 0.8.1-5 Regards!

10 10

Re: Converting typeset mathematics into Haskell ?
by Bernd Brassel 25 Aug '09

25 Aug '09

Sometimes the synchronicity of events is eery. Incidentally I have just written a proposal for just such a project. You can have a look at it at http://www-ps.informatik.uni-kiel.de/~bbr/WebOfProofs.html Although not directly mentioned in the proposal, there will be a lot of "Converting typeset mathematics into Haskell" going on. Kind regards Bernd PS: And just in case I did it wrong again; this is the message I wanted to reply to http://www.haskell.org/pipermail/haskell-cafe/2009-August/065572.html

2 1