- Haskell-Cafe - Haskell.org

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 26 Mar '13

26 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

Parsec community and up-to-date documentation
by Konstantine Rybnikov 25 Mar '13

25 Mar '13

Hi! I've been busy with (trying to) learning/using parsec lately and as a beginner had a lot of headache starting from outdated documentation in various places, lack of more tutorials, confusion between Text.Parsec and Text.ParseCombinator modules and so on. While I solved most of my problems via googling / reading stackoverflow / reading source code (of outdated version first, btw, the one I got from Daan's homepage :), I still had a feeling all the time that I'm doing something wrong and that I can't find place where "party is going on". So I wondered, what can I do to create a community around Parsec, to get issue tracking, pull-requests, up-to-date comprehensive documentation and tutorials etc.? Parsec seems like a perfect candidate for something like this. Thank you.

3 5

Re: [Haskell-cafe] Haskell-Cafe Digest, Vol 115, Issue 37
by Luc TAESCH 25 Mar '13

25 Mar '13

Le dimanche 24 mars 2013, a écrit : > Send Haskell-Cafe mailing list submissions to > haskell-cafe(a)haskell.org <javascript:;> > > To subscribe or unsubscribe via the World Wide Web, visit > http://www.haskell.org/mailman/listinfo/haskell-cafe > or, via email, send a message with subject or body 'help' to > haskell-cafe-request(a)haskell.org <javascript:;> > > You can reach the person managing the list at > haskell-cafe-owner(a)haskell.org <javascript:;> > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Haskell-Cafe digest..." >

1 0

Data.StorableVector vs Data.Vector.Storable
by Roman Cheplyaka 24 Mar '13

24 Mar '13

What is the relationship between these two modules? Do we really need both? (Data.Vector.Storable is part of vector, Data.StorableVector is from a separate package, storablevector.) Roman

2 1

Need some advice around lazy IO
by C K Kashyap 24 Mar '13

24 Mar '13

Hi, I am working on an automation that periodically fetches bug data from our bug tracking system and creates static HTML reports. Things worked fine when the bugs were in the order of 200 or so. Now I am trying to run it against 3000 bugs and suddenly I see things like - too many open handles, out of memory etc ... Here's the code snippet - http://hpaste.org/84197 It's a small snippet and I've put in the comments stating how I run into "out of file handles" or simply file not getting read due to lazy IO. I realize that putting ($!) using a trial/error approach is going to be futile. I'd appreciate some pointers into the tools I could use to get some idea of which expressions are building up huge thunks. Regards, Kashyap

9 17