March 2013 - Haskell-Cafe

Re: [Haskell-cafe] Pattern matching with singletons
by Richard Eisenberg 27 Mar '13

27 Mar '13

Hello Paul, > ----- Forwarded message from Paul Brauner <polux2001(a)gmail.com> ----- <snip> > - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC, > SLeft, ... (in which case GHC could infer it but for some reason can't) > - or are these pattern + definitions not sufficient to prove that a > ~ ('CC ('Left 'CA)) no matter what? The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh variable (b :: TA), but it can't yet take the next step and decide that, because TA has only one constructor, b must in fact be 'CA. In type-theory lingo, this deduction is called eta-expansion. There have been on-and-off debates about how best to add this sort of eta-expansion into GHC, but all seem to agree that it's not totally straightforward. For example, see GHC bug #7259. There's a non-negligible chance I will be taking a closer look into this at some point, but not for a few months, so don't hold your breath. I'm not aware of anyone else currently focusing on this problem either, I'm afraid. I'm glad you're finding use in the singletons package! Let me know if I can be of further help. Richard

2 1

my take at knucleotide
by Branimir Maksimovic 27 Mar '13

27 Mar '13

Hi, I have tried to implement knucleotide benchmark program this time:http://benchmarksgame.alioth.debian.org/u64q/performance.php?test=knuc… Implementation is shorter (uses hashtable from hashtables package),but two time slower then current Haskell entry ( which is too low levelfor my taste :)).What is interesting is that if I try to place Int64 as a key tohash table, performance is even slower.Strange that dropping and taking from bytestring would befaster than packing string in 64 bit int and directly indexing. If someone can see something that can bring performance on parwith current haskell entry , I would post it , otherwise no point,except that program is shorter and not low level. {-# Language BangPatterns #-}---- The Computer Language Benchmarks Game-- http://benchmarksgame.alioth.debian.org/---- Contributed by Branimir Maksimovic--import Data.Charimport Data.Listimport Data.IORefimport qualified Data.HashTable.IO as Himport qualified Data.ByteString.Char8 as Simport Control.Concurrentimport Text.Printf main = do s <- S.getContents let content = (S.map toUpper . S.concat . tail . dropWhile (\l->not $ S.isPrefixOf (S.pack ">THREE") l) . S.lines) s mapM_ (execute content) actions data Actions = I Int | S Stringactions = [I 1,I 2, S "GGT",S "GGTA",S "GGTATT",S "GGTATTTTAATT",S "GGTATTTTAATTTATAGT"]execute content (I i) = writeFrequencies content iexecute content (S s) = writeCount content s writeFrequencies input size = do ht <- tcalculate input size lst <- H.foldM (\lst (k,v)->do v' <- readIORef v return $ insertBy (\(_,x) (_,y)->y `compare` x) (k,v') lst) [] ht let sum = fromIntegral ((S.length input) + 1 - size) mapM_ (\(k,v)-> do printf "%s %.3f\n" (S.unpack k) ((100 * (fromIntegral v)/sum)::Double)) lst putChar '\n' writeCount input string = do let size = length string ht <- tcalculate input size res <- H.lookup ht (S.pack string) case res of Nothing -> putStrLn $ string ++ " not found..." Just v -> do r <- readIORef v printf "%d\t%s\n" r (string::String) tcalculate input size = do let l = [0..7] actions = map (\i -> (calculate input i size (length l))) l vars <- mapM (\action -> do var <- newEmptyMVar forkIO $ do answer <- action putMVar var answer return var) actions result <- newTable results <- mapM takeMVar vars mapM_ (\ht -> H.foldM (\lst (k,v) -> do res <- H.lookup lst k case res of Nothing -> do r1 <- readIORef v r2 <- newIORef r1 H.insert lst k r2 Just v1 -> do r1 <- readIORef v1 r2 <- readIORef v writeIORef v1 (r1+r2) return lst) result ht) results return result calculate input beg size incr = do ht <- newTable let calculate' :: S.ByteString -> Int -> IO HashTable calculate' str i | i >= ((S.length input)+1 - size) = return ht | otherwise = do res <- H.lookup ht k case res of Nothing -> do !r <- newIORef 1 H.insert ht k r Just v -> do !r <- readIORef v writeIORef v (r+1) calculate' (S.drop incr str) (i+incr) where k = S.take size str calculate' (S.drop beg input) beg type HashTable = H.BasicHashTable S.ByteString (IORef Int) newTable :: IO HashTablenewTable = H.new

2 4

Word8 literals in ByteString haddock?
by Niklas Hambüchen 27 Mar '13

27 Mar '13

Hey, according to http://hackage.haskell.org/packages/archive/bytestring/0.10.2.0/doc/html/Da… I can write: split '\n' "a\nb\nd\ne" Can I really do that? I don't know of a way to make a '\n' literal be a Word8, so maybe these Haddocks are wrong? I guess they would apply for Data.ByteString.Char8, but this is Data.ByteString. Or is there a way? Niklas

2 1

Future of MonadCatchIO
by Arie Peterson 26 Mar '13

26 Mar '13

Hi all, The function 'block' and 'unblock' (from Control.Exception) have been deprecated for some time, and are apparantly now being removed (in favour of 'mask'). Generalisations of these functions are (part of) the interface of MonadCatchIO-transformers (the 'MonadCatchIO' class has methods 'block' and 'unblock'). So, the interface would have to change to keep up with base. I'm inclined to deprecate MonadCatchIO-transformers itself, in favour of monad-control. I suspect that most clients do not use 'block' or 'unblock' directly, but use only derived functions, like 'bracket'. (I have partly confirmed this, by inspecting some reverse dependencies on hackage.) This allow an easy transition to monad-control: in many cases, only imports will need to be changed. In the minority of cases where 'block' and 'unblock' are used and/or instances of MonadCatchIO are defined, code will need to be updated. There is a difference in functionality between MonadCatchIO and monad-control. In the former, 'bracket' will not perform the final action if the main action is an ErrorT that throws an error (in contrast with exceptions in the underlying IO monad). In monad-control, 'bracket' will perform the final action in this case. (See this discussion for background: <http://www.haskell.org/pipermail/haskell-cafe/2010-October/084890.html>.) Probably, in most use cases the behaviour of monad-control is preferred. This seems to be the case also for snap, which uses MonadCatchIO-transformers, but defines its own variant of 'bracket' to get the right behaviour. Would anyone have a problem with a deprecation of MonadCatchIO-transformers, and a failure to update it to work with a base without 'block' and 'unblock'? Regards, Arie

5 7

Make a DSL serializable
by Corentin Dupont 26 Mar '13

26 Mar '13

Hi Café, I have a DSL like this: data Exp where OnEvent :: EventName -> (Int -> Exp) -> Exp (...) The "OnEvent" element carries a function (the handler to be called when the event happens), and that makes my DSL non showable/serializable. How could I fix that? This is a real handicap not to be able to serialize the state of my whole application because of that :) Thanks, Corentin

6 18

typed final-tagless HOAS interpreter for linear lambda calculus
by jeff p 26 Mar '13

26 Mar '13

{- This message presents a typed final-tagless HOAS interpreter for linear lambda calculus (LLC), which makes use of type families and datatype promotion. This code is inspired by Oleg's LLC interpreter using deBruijn indices (http://okmij.org/ftp/tagless-final/course/LinearLC.hs) The basic technique used here, and in Oleg's representation, comes from work on linear logic programming (see http://www.cs.cmu.edu/~fp/papers/erm97.pdf for details). An explicit presentation of LLC using these ideas can be found here http://www.cs.cmu.edu/~fp/courses/15816-f01/handouts/linfp.pdf [0]. While only the two arrow types and ints are included in this message; it is straightforward to extend this interpreter to cover all types of LLC. Attached to this message is an interpreter for full LLC (including additives and units) which is a direct transcription of the typing rules previously mentioned in [0]. The code for full LLC is written using MPTC and functional dependencies, instead of type families, but it is easily translatable to type families. -} {-# LANGUAGE DataKinds, KindSignatures, RankNTypes, TypeFamilies, TypeOperators, UndecidableInstances #-} {- The basic idea is to label each linear variable with a number and keep track of the linear context in the type of the representation. Thus our representation type looks like: repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> * repr vid hi ho a where vid is the next variable label to use, hi is the input linear hypotheses, ho is the output linear hypotheses, and a is the type of the term. -} -- Type-level Nat -- data Nat = Z | S Nat -- Type-level equality for Nat -- type family EqNat (x::Nat) (y::Nat) :: Bool type instance EqNat Z Z = True type instance EqNat (S x) (S y) = EqNat x y type instance EqNat Z (S y) = False type instance EqNat (S x) Z = False {- The key to enforcing linearity, is to have the type system consume (mark as used) linear variables as they are used. We use promoted [Maybe Nat] to represent a linear context. -} -- Type-level function to consume a given resource (a Maybe Nat) form a list. -- type family Consume (vid::Nat) (i::[Maybe Nat]) :: [Maybe Nat] type family Consume1 (b::Bool) (vid::Nat) (v::Nat) (vs::[Maybe Nat]) :: [Maybe Nat] type instance Consume vid (Nothing ': vs) = (Nothing ': Consume vid vs) type instance Consume vid (Just v ': vs) = Consume1 (EqNat vid v) vid v vs type instance Consume1 True vid v vs = Nothing ': vs type instance Consume1 False vid v vs = Just v ': Consume vid vs {- HOAS boils down to having the obect langauge (LLC) directly use the meta language (Haskell) variable and substitution machinery. So a typical HOAS representation of an object level function looks something like: lam :: (repr a -> repr b) -> repr (a -> b) The key to making HOAS work with our representation, is to have our object level variables make use of the Consume function above. Toward this end, we can create a general linear variable type. -} type VarTp (repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> *) vid a = forall v i o . repr v i (Consume vid i) a {- We can now write the representation of the LLC terms. Note that the type of each LLC term constructor (each member of class Lin) is a transcription of a typing rule for LLC. -} -- a type to distinguish linear functions from regular functions -- newtype a -<> b = Lolli {unLolli :: a -> b} -- the "Symantics" of LLC -- class Lin (repr :: Nat -> [Maybe Nat] -> [Maybe Nat] -> * -> *) where -- a base type int :: Int -> repr vid hi hi Int add :: repr vid hi h Int -> repr vid h ho Int -> repr vid hi ho Int -- linear lambda llam :: (VarTp repr vid a -> repr (S vid) (Just vid ': hi) (Nothing ': ho) b) -> repr vid hi ho (a -<> b) (<^>) :: repr vid hi h (a -<> b) -> repr vid h ho a -> repr vid hi ho b -- non-linear lambda lam :: ((forall v h . repr v h h a) -> repr vid hi ho b) -> repr vid hi ho (a -> b) (<$>) :: repr vid hi ho (a -> b) -> repr vid ho ho a -> repr vid hi ho b {- An evaluator which takes a LLC term of type a to a Haskell value of type a. -} newtype R (vid::Nat) (i::[Maybe Nat]) (o::[Maybe Nat]) a = R {unR :: a} instance Lin R where int = R add x y = R $ unR x + unR y llam f = R $ Lolli $ \x -> unR (f (R x)) f <^> x = R $ unLolli (unR f) (unR x) lam f = R $ \x -> unR (f (R x)) f <$> x = R $ unR f (unR x) eval :: R Z '[] '[] a -> a eval = unR {- Some examples: *Main> :t eval $ llam $ \x -> x eval $ llam $ \x -> x :: b -<> b *Main> :t eval $ llam $ \x -> add x (int 1) eval $ llam $ \x -> add x (int 1) :: Int -<> Int *Main> eval $ (llam $ \x -> add x (int 1)) <^> int 2 3 A non-linear uses of linear variables fail to type check: *Main> :t eval $ llam $ \x -> add x x <interactive>:1:27: Couldn't match type `Consume 'Z ('[] (Maybe Nat))' with '[] (Maybe Nat) Expected type: R ('S 'Z) ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))) ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))) Int Actual type: R ('S 'Z) ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat))) (Consume 'Z ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat)))) Int In the second argument of `add', namely `x' In the expression: add x x In the second argument of `($)', namely `\ x -> add x x' *Main> :t eval $ llam $ \x -> llam $ \y -> add x (int 1) <interactive>:1:38: Couldn't match type 'Just Nat ('S 'Z) with 'Nothing Nat Expected type: R ('S ('S 'Z)) ((':) (Maybe Nat) ('Just Nat ('S 'Z)) ((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat)))) ((':) (Maybe Nat) ('Nothing Nat) ((':) (Maybe Nat) ('Nothing Nat) ('[] (Maybe Nat)))) Int Actual type: R ('S ('S 'Z)) ((':) (Maybe Nat) ('Just Nat ('S 'Z)) ((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat)))) (Consume 'Z ((':) (Maybe Nat) ('Just Nat ('S 'Z)) ((':) (Maybe Nat) ('Just Nat 'Z) ('[] (Maybe Nat))))) Int In the first argument of `add', namely `x' In the expression: add x (int 1) In the second argument of `($)', namely `\ y -> add x (int 1)' But non-linear uses of regular variables are fine: *Main> :t eval $ lam $ \x -> add x x eval $ lam $ \x -> add x x :: Int -> Int *Main> eval $ (lam $ \x -> add x x) <$> int 1 2 *Main> :t eval $ lam $ \x -> lam $ \y -> add x (int 1) eval $ lam $ \x -> lam $ \y -> add x (int 1) :: Int -> a -> Int *Main> eval $ (lam $ \x -> lam $ \y -> add x (int 1)) <$> int 1 <$> int 2 2 -} {- We can also easily have an evaluator which produces a String. -} -- For convenience, we name linear variables x0, x1, ... and regular variables y0, y1, ... -- newtype Str (vid::Nat) (gi::[Maybe Nat]) (go::[Maybe Nat]) a = Str {unStr :: Int -> Int -> String} instance Lin Str where int x = Str $ \_ _ -> show x add x y = Str $ \uv lv -> "(" ++ unStr x uv lv ++ " + " ++ unStr y uv lv ++ ")" llam f = Str $ \uv lv -> let v = "x"++show lv in "\\" ++ v ++ " -<> " ++ unStr (f $ Str (\_ _ -> v)) uv (lv + 1) f <^> x = Str $ \uv lv -> "(" ++ unStr f uv lv ++ " ^ " ++ unStr x uv lv ++ ")" lam f = Str $ \uv lv -> let v = "y"++show uv in "\\" ++ v ++ " -> " ++ unStr (f $ Str (\_ _ -> v)) (uv + 1) lv f <$> x = Str $ \uv lv -> "(" ++ unStr f uv lv ++ " " ++ unStr x uv lv ++ ")" showLin :: Str Z '[] '[] a -> String showLin x = unStr x 0 0 {- An example: *Main> showLin $ (llam $ \x -> llam $ \y -> add x y) <^> int 1 "(\\x0 -<> \\x1 -<> (x0 + x1) ^ 1)" -}

1 0

Enumerating functions at runtime
by Luke Evans 25 Mar '13

25 Mar '13

I'm curious about using Haskell for metaprogramming. It looks like I can dynamically compile, load and run some Haskell with the plugins package. Actually I've briefly tried this and it seems to work for some simple cases at least. Now I would like to be able to enumerate precompiled public functions in modules that I might use as building blocks in such dynamic compilation. So far I'm not seeing anything that does this directly. Can anyone provide some pointers? If it's just not possible to introspect on compiled modules, then I suppose I could use external metadata of my own, or even perhaps haddock info if it exists, to attempt to generate this info. Clearly though, that's nowhere near as good as extracting the info from something the compiler built directly.

5 4

A Thought: Backus, FP, and Brute Force Learning
by OWP 25 Mar '13

25 Mar '13

This thought isn't really related to Haskell specifically but it's more towards FP ideal in general. I'm new to the FP world and to get me started, I began reading a few papers. One paper is by John Backus called "Can Programming Be Liberated from the von Neumann Style? A Functional Style and It's Algebra of Programs". While I like the premise which notes the limitation of the von Neumann Architecture, his solution to this problem makes me feel queasy when I read it. For me personally, one thing I enjoy about a typical procedural program is that it allows me to "Brute Force Learn". This means I stare at a particular section of the code for a while until I figure out what it does. I may not know the reasoning behind it but I can have a pretty decent idea of what it does. If I'm lucky, later on someone may tell me "oh, that just did a gradient of such and such matrix". In a way, I feel happy I learned something highly complex without knowing I learned something highly complex. Backus seems to throw that out the window. He introduces major new terms which require me to break out the math book which then requires me to break out a few other books to figure out which bases things using archaic symbols which then requires me to break out the pen and paper to mentally expand what in the world that does. It makes me feel CISCish except without a definition book nearby. It's nice if I already knew what a "gradient of such and such matrix" is but what happens if I don't? For the most part, I like the idea that I have the option of Brute Force Learning my way towards something. I also like the declarative aspect of languages such as SQL which let's me asks the computer of things once I know the meaning of what I'm asking. I like the ability to play and learn but I also like the ability to declare this or that once I do learn. From Backus paper, if his world comes to a reality, it seems like I should know what I'm doing before I even start. The ability to learn while coding seems to have disappeared. In a way, if the von Neumann bottleneck wasn't there, I'm not sure programming would be as popular as it is today. Unfortunately, I'm still very new and quite ignorant about Haskell so I do not know how much of Backus is incorporated in Haskell but so far, in the start of my FP learning adventure, this is how things seem to be seen. If I may generously ask, where am I wrong and where am I right with this thought? Thank you for any explanation P.S. If anyone knows of a better place I can ask this question, please feel free to show me the way.

5 8

Pattern matching with singletons
by Paul Brauner 25 Mar '13

25 Mar '13

Hello, the following programs seems to hit either some limitation of GHC or maybe I'm just missing something and it behaves the intended way. {-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds, GADTs #-} module Test where import Data.Singletons data TA = CA data TB = CB data TC = CC (Either TA TB) $(genSingletons [''TA, ''TB, ''TC]) type family Output (x :: TC) :: * type instance Output ('CC ('Left 'CA)) = Int type instance Output ('CC ('Right 'CB)) = String f :: Sing (a :: TC) -> Output a f (SCC (SLeft SCA)) = 1 g :: Sing (a :: TC) -> Output a g (SCC (SLeft _)) = 1 Function f typechecks as expected. Function g fails to typecheck with the following error. Could not deduce (Num (Output ('CC ('Left TA TB n0)))) arising from the literal `1' from the context (a ~ 'CC n, SingRep (Either TA TB) n) bound by a pattern with constructor SCC :: forall (a_a37R :: TC) (n_a37S :: Either TA TB). (a_a37R ~ 'CC n_a37S, SingRep (Either TA TB) n_a37S) => Sing (Either TA TB) n_a37S -> Sing TC a_a37R, in an equation for `g' at Test.hs:21:4-16 or from (n ~ 'Left TA TB n0, SingRep TA n0, SingKind TA ('KindParam TA)) bound by a pattern with constructor SLeft :: forall (a0 :: BOX) (b0 :: BOX) (a1 :: Either a0 b0) (n0 :: a0). (a1 ~ 'Left a0 b0 n0, SingRep a0 n0, SingKind a0 ('KindParam a0)) => Sing a0 n0 -> Sing (Either a0 b0) a1, in an equation for `g' at Test.hs:21:9-15 Possible fix: add an instance declaration for (Num (Output ('CC ('Left TA TB n0)))) In the expression: 1 In an equation for `g': g (SCC (SLeft _)) = 1 I would expect that a ~ ('CC ('Left 'CA)) in the right hand-side of g (SCC (SLeft _)) = 1 since SLeft's argument is necessarily of type STA, whose sole inhabitant is SA. Now I understand (looking at -ddump-slices, the singletons' library paper and the error message) that the definition of SCC and SLeft don't immediately imply what I just wrote above. So my question is: in the right hand-side of g (SCC (SLeft _)) = 1, - is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC, SLeft, ... (in which case GHC could infer it but for some reason can't) - or are these pattern + definitions not sufficient to prove that a ~ ('CC ('Left 'CA)) no matter what? Cheers, Paul

1 0

Munich Haskell Meeting
by Heinrich Hördegen 25 Mar '13

25 Mar '13

Dear all, tomorrow, 25th of March, will be our monthly Haskell Meeting in Munich. If you want to join, please go to http://www.haskell-munich.de/dates and click the button. Sorry for the late announcement! I wish everyone of you a nice and successful week, Heinrich

1 1