- Haskell-Cafe - Haskell.org

building a patched ghc
by braver 28 Jun '10

28 Jun '10

How do I get the latest 6.12 source and cherry-pick selected patches from the trunk, e.g. Simon's GC fixes? The wiki says that you get the head with darcs get --lazy http://darcs.haskell.org/ghc and the 6.12 with darcs get --lazy http://darcs.haskell.org/ghc-6.12/ghc Since the trunk is big enough, I wonder if 6.12 a subset of it and can be obtained from it? The tags are not informative. If I get the branch, how will I be able to get the patches from the head, once they're separate repos? -- Alexy

2 2

The mother of all functors/monads/categories
by Max Bolingbroke 28 Jun '10

28 Jun '10

I'm wondering if someone can cast some light on a pattern I've come across, which I'm calling the "mother of all X" pattern after Dan Piponi's blog post (http://blog.sigfpe.com/2008/12/mother-of-all-monads.html) Edward Kmett has also explored these ideas here: http://www.mail-archive.com/haskell-cafe@haskell.org/msg57738.html Preliminaries === Q: What is the "mother of all X", where X is some type class? A: It is a data type D such that: 1. There exist total functions: > lift :: X d => d a -> D a > lower :: X d => D a -> d a 2. And you can write a valid instance: > instance X D With *no superclass constraints*. 3. (We may also add the constraint that D is somehow the "smallest such" data type, but I don't know in exactly what sense I mean this). So the "mother of all X" is a data type that somehow encodes all of the functions that the X type class gives you. An example is in order! Example 1: Yoneda is the mother of all Functors === The code in this example and the next one is shamelessly stolen from the category-extras package (thanks Edward!). Here is the data type: > -- flip fmap :: forall a. f a -> (forall b. (a -> b) -> f b) > newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } And the injections. As it turns out, we don't need the Functor constraint on the lowerYoneda call: > liftYoneda :: Functor f => f a -> Yoneda f a > liftYoneda f = Yoneda (flip fmap f) > > lowerYoneda :: Yoneda f a -> f a > lowerYoneda f = runYoneda f id Finally, we can write the Functor instance. Notice that we don't need to make use of the Functor instance for f: all of the methods of Functor f have been somehow encoded into the Yoneda data type! > instance Functor (Yoneda f) where > fmap f m = Yoneda (\k -> runYoneda m (k . f)) Note that we can also write an instance (Y f => Y (Yoneda f)) for any Functor subclass Y. But (Yoneda f) is not the mother of all Y, because we will need the Y f constraint to do so. Here is an example: > instance Applicative f => Applicative (Yoneda f) where > pure = liftYoneda . pure > mf <*> mx = liftYoneda (lowerYoneda mf <*> lowerYoneda mx) Why is (Yoneda f) interesting? Because if I take some expression whose type is quantified over any superclass of Functor, and we want to run it with Functor instantiated to some F, if we instead run it with Functor instantiated to (Yoneda f) and then use lowerYoneda, we will automatically get guaranteed fmap fusion. Example 2: Codensity is the mother of all Monads === Data type: > -- (>>=) :: forall a. m a -> (forall b. (a -> m b) -> m b) > newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b } Isomorphism. We need Monad constraints on both ends now: > liftCodensity :: Monad m => m a -> Codensity m a > liftCodensity m = Codensity ((>>=) m) > > lowerCodensity :: Monad m => Codensity m a -> m a > lowerCodensity m = runCodensity m return Instances: > instance Functor (Codensity f) where > fmap f m = Codensity (\k -> runCodensity m (k . f)) > > instance Applicative (Codensity f) where > pure x = Codensity (\k -> k x) > mf <*> mx = Codensity (\k -> runCodensity mf (\f -> runCodensity mx (\x -> k (f x)))) > > instance Monad (Codensity f) where > return = pure > m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c)) Again, using (Codensity m) where you used m before can yield a performance improvement, notably in the case of free monads. See http://haskell.org/haskellwiki/Performance/Monads or http://wwwtcs.inf.tu-dresden.de/~voigt/mpc08.pdf. Example 3: Wotsit is the mother of all Categories === I don't actually know what the right name for this data type is, I just invented it and it seems to work: > -- (>>>) :: forall a b. t a b -> (forall c. t b c -> t a c) > newtype Wotsit t a b = Wotsit { runWotsit :: forall c. t b c -> t a c } Isomorphism: > liftWotsit :: Category t => t a b -> Wotsit t a b > liftWotsit t = Wotsit ((>>>) t) > > lowerWotsit :: Category t => Wotsit t a b -> t a b > lowerWotsit t = runWotsit t id And finally the instance: > instance Category (Wotsit t) where > id = Wotsit id > t1 . t2 = Wotsit (runWotsit t2 . runWotsit t1) This is *strongly* reminiscent of normalisation-by-evaluation for monoids (reassociation realised by assocativity of function application), which is not surprising because Category is just a monoid. There is probably some connection between NBE and Yoneda (e.g. "Normalization and the Yoneda embedding", but I can't get access to this paper electronically). Conclusion === So I have a lot of questions about this stuff: 1. Is there a way to mechanically derive the "mother of all X" from the signature of X? Are these all instances of a single categorical framework? 2. Is there a mother of all idioms? By analogy with the previous three examples, I tried this: > -- (<**>) :: forall a. i a -> (forall b. i (a -> b) -> i b) > newtype Thingy i a = Thingy { runThingy :: forall b. i (a -> b) -> i b } But I can't see how to write either pure or <*> with that data type. This version seems to work slightly better: > newtype Thingy i a = Thingy { runThingy :: forall b. Yoneda i (a -> b) -> i b } Because you can write pure (pure x = Thingy (\k -> lowerYoneda (fmap ($ x) k))). But <*> still eludes me! 3. Since (Codensity m) enforces >>= associativity, perhaps it can be used to define correct-by-construction monads in the style of operational or MonadPrompt? Any insight offered would be much appreciated :-) Cheers, Max

8 17

ANN: bitspeak 0.0.1
by Maurício CA 27 Jun '10

27 Jun '10

Hi, all, bitspeak is a small proof of concept application that allows writing text using only two commands (yes/no, 1/2, top/down etc.). It is intended to show how people with disabilities similar to Stephen Hawking's (i.e., good cognitive hability, but very few movements) can write text. http://hackage.haskell.org/package/bitspeak http://bitbucket.org/mauricio/bitspeak/wiki/Home Best, Maurício

15 19

A little jewel on sigfpe's blog
by Günther Schmidt 27 Jun '10

27 Jun '10

Hello, I just discovered this little jewel on Dan Piponi's blog. http://blog.sigfpe.com/2010/03/partial-ordering-of-some-category.html I'm just posting the link so that it doesn't get overlooked, would be a real shame. Günther

1 0

Core packages and locale support
by Roman Cheplyaka 27 Jun '10

27 Jun '10

While ghc 6.12 finally has proper locale support, core packages (such as unix) still use withCString and therefore work incorrectly when argument (e.g. file path) is not ASCII. Is someone already working on this? If it's just a matter of time and manpower I can help but I need some guidance from authority. -- Roman I. Cheplyaka :: http://ro-che.info/ "Don't let school get in the way of your education." - Mark Twain

7 36

Emacs script to align Haskell import list
by Christopher Done 26 Jun '10

26 Jun '10

I whipped up a little Emacs script to align the import lines in the current buffer. I am using it in my projects and have experienced no problems. It's good at keeping within 80 columns. http://gist.github.com/453933 I've pasted it as a gist on Github so that anyone can edit it, gists also provide a simple revision history and comment support. Please feel free to contribute some tweaks and fixes. I'll then see about merging this into haskell-mode in some fashion. It doesn't handle multiple line explicit imports as I have a personal rule that any explicit import list with more than a few symbols should be changed to an "as X" import, as an addition to tibbe's style guide.[1] I haven't decided on a recommended keybinding. I'm considering a context-dependent binding of C-c C-. that indents the import list when you are on an import line. [1]: http://github.com/tibbe/haskell-style-guide

1 1

Re: [Haskell-cafe] Huffman Codes in Haskell
by John Lato 26 Jun '10

26 Jun '10

> From: Max Rabkin <max.rabkin(a)gmail.com> > > This seems like an example of list-chauvinism -- what Chris Okasaki > calls a communal blind spot of the FP community in Breadth-First > Numbering: Lessons from a Small Exercise in Algorithm Design -- > http://www.eecs.usma.edu/webs/people/okasaki/icfp00.ps > Thanks for sharing; this was an interesting (and short!) read. I would like to see other Haskeller's responses to this problem. I'll restate it here hoping to get replies from those who haven't read the paper yet: Assume you have a type of labeled binary trees: data Tree a = E | T a (Tree a) (Tree a) and you are to produce a function bfnum :: Tree a -> Tree Int that performs a breadth-first numbering of the tree (starting with 1), preserving the tree structure. How would you implement bfnum? (If you've already read the paper, what was your first answer?) For the record, my solution doesn't rely on any other data structures or laziness AFAICT, and I think it would fit into the Level-Oriented category of solutions. John

6 9

Haskell Web Framework for newbies?
by Giuseppe Luigi Punzi 26 Jun '10

26 Jun '10

Hi all, At the moment, I'm learning haskell and I would like to use the things I'm learning under web. I would like to mount a local web server, but I would like to test some things in my VPS in 1&1 with CentOs 5, but this, in a near future. For the moment, my doubt is, wich is the haskell web framework more easy to learn for newbies? Cheers.

1 0

Re: [Haskell-cafe] Manual Type-Checking to provide Read instances for GADTs. (was Re: [Haskell-cafe] Read instance for GATD)
by Edward Kmett 26 Jun '10

26 Jun '10

I've obtained permission to repost Gershom's slides on how to deserialize GADTs by typechecking them yourself, which are actually a literate haskell source file, that he was rendering to slides. Consequently, I've just pasted the content below as a literate email. -Edward Kmett - Deserializing strongly typed values (four easy pieces about typechecking) Gershom Bazerman - prior art: Oleg (of course) http://okmij.org/ftp/tagless-final/course/course.html ...but also Stephanie Weirich http://www.comlab.ox.ac.uk/projects/gip/school/tc.hs = Ahem... \begin{code} {-# LANGUAGE DeriveDataTypeable, ExistentialQuantification, FlexibleContexts, FlexibleInstances, FunctionalDependencies, GADTs, RankNTypes, ScopedTypeVariables #-} \end{code} = ahem. \begin{code} import Data.Typeable import Data.Maybe import Control.Monad.Error import Control.Applicative import qualified Data.Map as M import Unsafe.Coerce \end{code} = A simple ADT. \begin{code} data SimpleExpr = SOpBi String SimpleExpr SimpleExpr | SOpUn String SimpleExpr | SDbl Double | SBool Bool deriving (Read, Show, Typeable) \end{code} Yawn. = An awesome GADT! \begin{code} data Expr a where EDbl :: Double -> Expr Double EBool :: Bool -> Expr Bool EBoolOpBi :: BoolOpBi -> Expr Bool -> Expr Bool -> Expr Bool ENumOpBi :: NumOpBi -> Expr Double -> Expr Double -> Expr Double ENumOpUn :: NumOpUn -> Expr Double -> Expr Double deriving Typeable data NumOpBi = Add | Sub deriving (Eq, Show) data NumOpUn = Log | Exp deriving (Eq, Show) data BoolOpBi = And | Or deriving (Eq, Show) \end{code} The GADT is well typed. It cannot go wrong. - It also cannot derive show. = But we can write show... \begin{code} showIt :: Expr a -> String showIt (EDbl d) = show d showIt (EBool b) = show b showIt (EBoolOpBi op x y) = "(" ++ show op ++ " " ++ showIt x ++ " " ++ showIt y ++ ")" showIt (ENumOpBi op x y) = "(" ++ show op ++ " " ++ showIt x ++ " " ++ showIt y ++ ")" showIt (ENumOpUn op x) = show op ++ "(" ++ showIt x ++ ")" \end{code} = And eval is *much nicer*. It cannot go wrong --> no runtime typechecks. \begin{code} evalIt :: Expr a -> a evalIt (EDbl x) = x evalIt (EBool x) = x evalIt (EBoolOpBi op expr1 expr2) | op == And = evalIt expr1 && evalIt expr2 | op == Or = evalIt expr2 || evalIt expr2 evalIt (ENumOpBi op expr1 expr2) | op == Add = evalIt expr1 + evalIt expr2 | op == Sub = evalIt expr1 - evalIt expr2 \end{code} = But how do we write read!? read "EBool False" = Expr Bool read "EDbl 12" = Expr Double The type being read depends on the content of the string. Even worse, we want to read not from a string that looks obvious to Haskell (i.e. a standard showlike instance) but from something that looks pretty to the user -- we want to *parse*. So we parse into our simple ADT. Then we turn our simple ADT into our nice GADT. - But how? How do we go from untyped... to typed? [And in general -- not just into an arbitrary GADT, but an arbitrary inhabitant of a typeclass.] [i.e. tagless final, etc] = Take 1: Even if we do not know what type we are creating, we eventually will do something with it. So we paramaterize our typechecking function over an arbitrary continuation. \begin{code} mkExpr :: (forall a. (Show a, Typeable a) => Expr a -> r) -> SimpleExpr -> r mkExpr k expr = case expr of SDbl d -> k $ EDbl d SBool b -> k $ EBool b SOpUn op expr1 -> case op of "log" -> k $ mkExpr' (ENumOpUn Log) expr1 "exp" -> k $ mkExpr' (ENumOpUn Exp) expr1 _ -> error "bad unary op" SOpBi op expr1 expr2 -> case op of "add" -> k $ mkExprBi (ENumOpBi Add) expr1 expr2 "sub" -> k $ mkExprBi (ENumOpBi Sub) expr1 expr2 \end{code} = Where's the typechecking? \begin{code} mkExpr' k expr = mkExpr (appCast $ k) expr mkExprBi k expr1 expr2 = mkExpr' (mkExpr' k expr1) expr2 appCast :: forall a b c r. (Typeable a, Typeable b) => (c a -> r) -> c b -> r appCast f x = maybe err f $ gcast x where err = error $ "Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} ... We let Haskell do all the work! = Hmmm... the continuation can be anything. So let's just make it an existential constructor. \begin{code} data ExprBox = forall a. Typeable a => ExprBox (Expr a) appExprBox :: (forall a. Expr a -> res) -> ExprBox -> res appExprBox f (ExprBox x) = f x tcCast :: forall a b c. (Typeable a, Typeable b) => Expr a -> Either String (Expr b) tcCast x = maybe err Right $ gcast x where err = Left $ "Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} Now we can delay deciding what to apply until later. Typecheck once, execute repeatedly! = One more trick -- monadic notation lets us extend the context of unpacked existentials to the end of the do block \begin{code} retBox x = return (ExprBox $ x, typeOf x) typeCheck :: SimpleExpr -> Either String (ExprBox, TypeRep) typeCheck (SDbl d) = retBox (EDbl d) typeCheck (SBool b) = retBox (EBool b) typeCheck (SOpBi op s1 s2) = case op of "add" -> tcBiOp (ENumOpBi Add) "sub" -> tcBiOp (ENumOpBi Sub) "and" -> tcBiOp (EBoolOpBi And) "or" -> tcBiOp (EBoolOpBi Or) where tcBiOp constr = do (ExprBox e1, _) <- typeCheck s1 (ExprBox e2, _) <- typeCheck s2 e1' <- tcCast e1 e2' <- tcCast e2 retBox $ constr e1' e2' \end{code} = So that's fine for *very* simple expressions. How does it work for interesting GADTs? (like, for example, HOAS)? (The prior art doesn't demonstrate HOAS -- it uses DeBruijn.) = Our simple world \begin{code} type Ident = String type TypeStr = String data STerm = SNum Double | SApp STerm STerm | SVar Ident | SLam Ident TypeRep STerm \end{code} Note.. terms are Church style -- each var introduced has a definite type. Determining this type is left as an exercise. = Over the rainbow in well-typed land. \begin{code} data Term a where TNum :: Double -> Term Double TApp :: Term (a -> b) -> Term a -> Term b TLam :: Typeable a => (Term a -> Term b) -> Term (a -> b) TVar :: Typeable a => Int -> Term a deriving Typeable \end{code} Wait! DeBrujin (TVar) *and* HOAS (TLam)! The worst of both worlds. Don't worry. In the final product all TVars are eliminated by construction. Exercise to audience: rewrite the code so that TVar can be eliminated from the Term type. = Show and eval... \begin{code} showT :: Int -> Term a -> String showT c (TNum d) = show d showT c (TApp f x) = "App (" ++ showT c f ++ ") (" ++ showT c x ++ ")" showT c (TLam f) = "Lam " ++ ("a"++show c) ++ " -> " ++ (showT (succ c) $ f (TVar c)) showT c (TVar i) = "a"++show i runT :: Term a -> Term a runT (TNum d) = (TNum d) runT (TLam f) = (TLam f) runT (TApp f x) = case runT f of TLam f' -> runT (f' x) runT (TVar i) = error (show i) \end{code} = The existential \begin{code} data TermBox = forall a. Typeable a => TermBox (Term a) appTermBox :: (forall a. Typeable a => Term a -> res) -> TermBox -> res appTermBox f (TermBox x) = f x \end{code} = The typechecker returns a box *and* a typeRep. Cast is the usual trick. \begin{code} retTBox :: Typeable a => Term a -> Either String (TermBox, TypeRep) retTBox x = return (TermBox $ x, typeOf x) type Env = M.Map Ident (TermBox, TypeRep) trmCast :: forall a b c. (Typeable a, Typeable b) => Term a -> Either String (Term b) trmCast x = maybe err Right $ gcast x where err = Left $ "Type error. Expected: " ++ show (typeOf (undefined::a)) ++ ", Inferred: " ++ show (typeOf (undefined::b)) \end{code} = \begin{code} typeCheck' :: STerm -> Env -> Either String (TermBox, TypeRep) typeCheck' t env = go t env 0 where go (SNum d) _ idx = retTBox (TNum d) go (SVar i) env idx = do (TermBox t, _) <- maybe (fail $ "not in scope: " ++ i) return $ M.lookup i env retTBox $ t \end{code} Nums and vars are easy. = App and Lam... less so. \begin{code} go (SApp s1 s2) env idx = do (TermBox e1, tr1) <- go s1 env idx (TermBox e2, _) <- go s2 env idx TermBox rt <- return $ mkTerm $ head $ tail $ typeRepArgs $ head $ typeRepArgs $ tr1 -- TypeReps have their... drawbacks. e1' <- trmCast e1 retTBox $ TApp e1' e2 `asTypeOf` rt go (SLam i tr s) env idx = do TermBox et <- return $ mkTerm tr (TermBox e, _) <- go s (M.insert i (TermBox (TVar idx `asTypeOf` et),tr) env ) (idx + 1) retTBox $ TLam (\x -> subst (x `asTypeOf` et) idx e) \end{code} = How does mkTerm work? \begin{code} mkTerm :: TypeRep -> TermBox mkTerm tr = go tr TermBox where go :: TypeRep -> (forall a. (Typeable a) => Term a -> res) -> res go tr k | tr == typeOf (0::Double) = k (TNum 0) | typeRepTyCon tr == arrCon = go (head $ typeRepArgs tr) $ \xt -> go (head $ tail $ typeRepArgs tr) $ \y -> k (TLam $ \x -> const y (x `asTypeOf` xt)) arrCon = typeRepTyCon $ typeOf (undefined::Int -> String) \end{code} Same principle -- but can build arrows directly. Doing so requires staying cps... I think. = And this is how we get rid of the DeBruijn terms. \begin{code} subst :: (Typeable a) => Term a -> Int -> Term b -> Term b subst t i trm = go trm where go :: Term c -> Term c go (TNum d) = (TNum d) go (TApp f x) = TApp (go f) (go x) go (TLam f) = TLam (\a -> go (f a)) go (TVar i') | i == i' = either error id $ trmCast t | otherwise = (TVar i') \end{code} Q: Now you see why DeBruijn is handy -- substitution is otherwise a pain. = But note -- all functions must be monotyped. This is the simply typed lambda calculus. How do we represent TLam (\a -> a)? The masses demand HM polymorphism. - Take 4: A damn dirty hack. = All hacks begin with Nats. \begin{code} data Z = Z deriving (Show, Typeable) data S a = S a deriving (Show, Typeable) \end{code} = typeCheck is almost the same. \begin{code} typeCheck'' :: STerm -> Env -> Either String (TermBox, TypeRep) typeCheck'' t env = go t env 0 where go :: STerm -> Env -> Int -> Either String (TermBox, TypeRep) go (SNum d) _ idx = retTBox (TNum d) go (SVar i) env idx = do (TermBox t, _) <- maybe (fail $ "not in scope: " ++ i) return $ M.lookup i env retTBox $ t \end{code} = \begin{code} go (SApp s1 s2) env idx = do (TermBox e1, tr1) <- go s1 env idx (TermBox e2, _) <- go s2 env idx TermBox rt <- unifyAppRet e1 e2 e1' <- unifyAppFun e1 e2 retTBox $ TApp e1' e2 `asTypeOf` rt go (SLam i tr s) env idx = do TermBox et <- return $ mkTerm' $ tr (TermBox e, _) <- go s (M.insert i (TermBox (TVar idx `asTypeOf` et),tr) env) (idx + 1) retTBox $ TLam (\x -> subst (x `asTypeOf` et) idx e) \end{code} It looks like we just factored on the nasty arrow code. = mkTerm is almost the same... we just extended it to deal with Nats. \begin{code} mkTerm' :: TypeRep -> TermBox mkTerm' tr = go tr TermBox where go :: TypeRep -> (forall a. (Typeable a) => Term a -> res) -> res go tr k | tr == typeOf (0::Double) = k (TNum 0) | tr == typeOf Z = k (TVar 0 :: Term Z) | typeRepTyCon tr == succCon = go (head $ typeRepArgs tr) $ \t -> k $ succTerm t | isArr tr = go (head $ typeRepArgs tr) $ \xt -> go (head $ tail $ typeRepArgs tr) $ \y -> k (TLam $ \x -> const y (x `asTypeOf` xt)) | otherwise = error $ show tr succCon = typeRepTyCon $ typeOf (S Z) succTerm :: Typeable b => Term b -> Term (S b) succTerm _ = TVar 0 \end{code} = Some utilities \begin{code} isArr :: TypeRep -> Bool isArr x = typeRepTyCon x == (typeRepTyCon $ typeOf (undefined::Int -> String)) splitArrCon :: TypeRep -> Either String (TypeRep, TypeRep) splitArrCon x | isArr x = case typeRepArgs x of [a,b] -> Right (a,b) _ -> Left $ "Expected function, inferred: " ++ show x | otherwise = Left $ "Expected function, inferred: " ++ show x \end{code} = Give an arrow term we unify it with its argument... and return a witness. \begin{code} unifyAppRet :: forall a b. (Typeable a, Typeable b) => Term a -> Term b -> Either String TermBox unifyAppRet x y = do tr <- unifyAppTyps (head $ typeRepArgs $ typeOf x) (head $ typeRepArgs $ typeOf y) return $ mkTerm' tr \end{code} = Yes. Actual unification. (although this is unification of a type template, so at least it is local) \begin{code} unifyAppTyps :: TypeRep -> TypeRep -> Either String TypeRep unifyAppTyps trf trx = do (fl,fr) <- splitArrCon trf env <- go M.empty fl trx subIt env fr where -- go yields a substitution environment. go :: M.Map String TypeRep -> TypeRep -> TypeRep -> Either String (M.Map String TypeRep) go env x y | isFree x = case M.lookup (show x) env of Just x' -> if x' == y then return env else Left (error "a") Nothing -> return $ M.insert (show x) y env | isArr x = do (lh,rh) <- splitArrCon x (lh',rh') <- splitArrCon y env' <- go env lh lh' go env' rh rh' | otherwise = if x == y then return env else Left (error "b") \end{code} = \begin{code} -- subIt applies it subIt :: M.Map String TypeRep -> TypeRep -> Either String TypeRep subIt env x | isFree x = case M.lookup (show x) env of Just x' -> return x' Nothing -> Left (error "c") | isArr x = do (lh,rh) <- splitArrCon x lh' <- subIt env lh rh' <- subIt env rh return $ mkTyConApp arrCon [lh',rh'] | otherwise = return x succCon = typeRepTyCon $ typeOf (S Z) zCon = typeRepTyCon $ typeOf Z isFree x = typeRepTyCon x `elem` [zCon, succCon] arrCon = (typeRepTyCon $ typeOf (undefined::Int -> String)) \end{code} = And now, we just have to convince GHC that they unify! \begin{code} unifyAppFun :: forall a b c. (Typeable a, Typeable b, Typeable c) => Term a -> Term b -> Either String (Term c) unifyAppFun x y = do unifyAppTyps (head $ typeRepArgs $ typeOf x) (head $ typeRepArgs $ typeOf y) return $ unsafeCoerce x \end{code} = Problem solved. On Fri, Jun 25, 2010 at 2:03 PM, Edward Kmett <ekmett(a)gmail.com> wrote: > It turns out that defining Read is somewhat tricky to do for a GADT. > > Gershom Bazerman has some very nice slides on how to survive the process by > manual typechecking (much in the spirit of Oleg's meta-typechecking code > referenced by Stephen's follow up below) > > He presented them at hac-phi this time around. > > I will check with him to see if I can get permission to host them somewhere > and post a link to them here. > > -Edward Kmett > > > On Fri, Jun 25, 2010 at 5:04 AM, <corentin.dupont(a)ext.mpsa.com> wrote: > >> >> Hello Haskellers, >> >> I'm having trouble writing a Read Instance for my GATD. >> Arg this GATD!! It causes me more problems that it solves ;) >> Especially with no automatic deriving, it adds a lot of burden to my code. >> >> >data Obs a where >> > ProposedBy :: Obs Int -- The player that proposed the tested >> rule >> > Turn :: Obs Turn -- The current turn >> > Official :: Obs Bool -- whereas the tested rule is official >> > Equ :: (Eq a, Show a, Typeable a) => Obs a -> Obs a -> Obs >> Bool >> > Plus :: (Num a) => Obs a -> Obs a -> Obs a >> > Time :: (Num a) => Obs a -> Obs a -> Obs a >> > Minus :: (Num a) => Obs a -> Obs a -> Obs a >> > And :: Obs Bool -> Obs Bool -> Obs Bool >> > Or :: Obs Bool -> Obs Bool -> Obs Bool >> > Not :: Obs Bool -> Obs Bool >> > Konst :: a -> Obs a >> >> >> > instance Read a => Read (Obs a) where >> > readPrec = (prec 10 $ do >> > Ident "ProposedBy" <- lexP >> > return (ProposedBy)) >> > +++ >> > (prec 10 $ do >> > Ident "Official" <- lexP >> > return (Official)) >> > (etc...) >> >> Observable.lhs:120:8: >> Couldn't match expected type `Int' against inferred type `Bool' >> Expected type: ReadPrec (Obs Int) >> Inferred type: ReadPrec (Obs Bool) >> >> >> Indeed "ProposedBy" does not have the same type that "Official". >> Mmh how to make it all gently mix altogether? >> >> >> Best, >> Corentin >> >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe(a)haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > >

2 1

Why my program runs out of memory?
by Vladimir Ch. 25 Jun '10

25 Jun '10

I'm trying to solve this problem: http://projecteuler.net/index.php?section=problems&id=44, and my program runs out of memory. I was wondering where I have a space leak, I thought that this program doesn't accumulate any data structures (i.e. should use constant memory): CODE BEGINS -- returns list of pairs (i, j) of indices, for which differences (gen j - gen i) -- increase, provided that gen has the following property: -- gen (i+1) - gen i > gen i - gen (i - 1) incDiffPairs gen = iterate next (0, 1) where next (i, j) = if (i == 0) || gen (j+1) - gen j < gen j - gen (i - 1) then (j, j + 1) else (i - 1, j) -- returns ith pentagonal number pentagonal i = let n = i + 1 in n * (3 * n - 1) `div` 2 -- tests if a number is pentagonal isPentagonal x = let d = 24 * x + 1 in isSquare d && (1 + sqrti d) `mod` 6 == 0 result44 = head [(pentagonal j - pentagonal i, (i, j)) | (i, j) <- incDiffPairs pentagonal, isPentagonal (pentagonal j - pentagonal i), isPentagonal (pentagonal j + pentagonal i)] CODE ENDS

2 2