- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] On the verge of ... giving up! [OT]
by Brandon S. Allbery KF8NH 15 Oct '07

15 Oct '07

On Oct 15, 2007, at 7:01 , Yitzchak Gale wrote: > But I think we are still at the stage where a programmer > who wants practical results is better off starting out > by learning how to use monads in practice, not by > delving into category theory. No argument from a Haskell standpoint. Still, when people here or on #haskell start tossing CT around, it'd be nice to have more than a very vague and probably incorrect notion of what they're saying. :) -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery(a)kf8nh.com system administrator [openafs,heimdal,too many hats] allbery(a)ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

1 0

Let's do ListT right, finally
by Yitzchak Gale 15 Oct '07

15 Oct '07

Hi Ian, thanks for responding to my plea! I am renaming this thread and moving it to libraries. Please respond there. I wrote: >> http://haskell.org/haskellwiki/ListT_done_right >> and not the broken implementation that comes with mtl. >> (Finally fixed in 6.8? Please?) Ian Lynagh wrote: > If you want to propose that mtl switches to a different definition of > ListT then please see > http://www.haskell.org/haskellwiki/Library_submissions OK, then. This is a major rewrite of this module. So let me open up the topic for discussion even before posting a submission. Do we need to worry about breaking code? Not very much, I suspect. That "monad" really is broken - it's not a monad at all. The problem and its solution have been well known for years. I personally tried using the "standard" ListT for a while, just because it's the standard. Until I ran into enough problems that I finally slapped my forehead and said "forget it". But just in case: Is there anyone reading this who would be hurt by this change and opposes it? Should we provide a more gradual deprecation path (what is it)? Thanks, Yitz

4 4

Re: [Haskell-cafe] haskell-curry, classical logic, excluded middle
by Tim Newsham 15 Oct '07

15 Oct '07

On Sun, 14 Oct 2007, Roberto Zunino wrote: > (Warning: wild guess follows, I can not completely follow CPS ;-)) > Adding a couple of forall's makes it compile: > propCC :: ((forall q . p -> Prop r q) -> Prop r p) -> Prop r p > func1 :: (forall q . Or r p (Not r p) -> Prop r q) > -> Prop r (Or r p (Not r p)) Yup! That did it, thanks! Now that that works, one more question. Is it possible to hide the "r" that is attached to every single type? For example to do something like this (which doesn't compile): data Prop p = Prop (forall r. (p -> r) -> r) run :: Prop p -> (p -> r) -> r run (Prop f) k = f k propCC :: ((forall q. p -> Prop q) -> Prop p) -> Prop p propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k) > Zun. Tim Newsham http://www.thenewsh.com/~newsham/

2 2

haskell-curry, classical logic, excluded middle
by Tim Newsham 15 Oct '07

15 Oct '07

I've been struggling with this for the last day and a half. I'm trying to get some exercise with the type system and with logic by playing with the curry-howard correspondence. I got stuck on the excluded-middle, and I think now I got it almost all the way there, but its still not quite right. Is this error I'm getting (inline at the end) easily fixed, and what exactly is going on? ---- code --- {-# OPTIONS_GHC -fglasgow-exts #-} module Classic where {- Classic logic. (See Intuit.hs first). In this system propositions all take a continuation. This allows us to define the law of the excluded middle. -} import Control.Monad -- propositions are functions taking a continuation. data Prop r p = Prop ((p -> r) -> r) run :: Prop r p -> (p -> r) -> r run (Prop f) k = f k propCC :: ((p -> Prop r q) -> Prop r p) -> Prop r p propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k) instance Monad (Prop r) where return p = Prop (\c -> c p) p >>= mkq = Prop (\c -> run p (\r -> run (mkq r) c)) data TRUTH = TRUTH type FALSE r = Not r TRUTH data And r p q = And (Prop r p) (Prop r q) data Or r p q = OrL (Prop r p) | OrR (Prop r q) data Imp r p q = Imp (Prop r p -> Prop r q) data Equiv r p q = Equiv (Prop r p -> Prop r q) (Prop r q -> Prop r p) data Not r p = Not (forall q. (Prop r p -> Prop r q)) -- Truth truth :: Prop r TRUTH truth = return TRUTH -- And-Injection -- P, Q |- P /\ Q andInj :: Prop r p -> Prop r q -> Prop r (And r p q) andInj p q = return (And p q) -- And-Elimination, left and Right -- P /\ Q |- P andElimL :: Prop r (And r p q) -> Prop r p andElimL pq = pq >>= \(And p q) -> p -- P /\ Q |- Q andElimR :: Prop r (And r p q) -> Prop r q andElimR pq = pq >>= \(And p q) -> q -- Or-Injection, left and right -- P |- P \/ Q orInjL :: Prop r p -> Prop r (Or r p q) orInjL p = return (OrL p) -- Q |- P \/ Q orInjR :: Prop r q -> Prop r (Or r p q) orInjR q = return (OrR q) -- Or-Elimination. -- P \/ Q, P -> R, Q -> R |- R orElim :: Prop r (Or r p q) -> (Prop r p -> Prop r s) -> (Prop r q -> Prop r s) -> Prop r s orElim pORq p2r q2r = pORq >>= byCases where byCases (OrL p) = p2r p byCases (OrR q) = q2r q -- Implication-Injection -- (P |- Q) |- P -> Q impInj :: (Prop r p -> Prop r q) -> Prop r (Imp r p q) impInj p2q = return (Imp p2q) -- Implication-elimination (modus ponen) -- P, P -> Q |- Q impElim :: Prop r p -> Prop r (Imp r p q) -> Prop r q impElim p pIMPq = pIMPq >>= \(Imp p2q) -> p2q p -- Equivalence-Injection -- P -> Q, Q -> P |- P = Q equivInj :: Prop r (Imp r p q) -> Prop r (Imp r q p) -> Prop r (Equiv r p q) equivInj pIMPq qIMPp = do (Imp p2q) <- pIMPq (Imp q2p) <- qIMPp return (Equiv p2q q2p) -- Equivalence-Elimination, Left and Right -- P = Q |- P -> Q equivElimL :: Prop r (Equiv r p q) -> Prop r (Imp r p q) equivElimL pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp p2q) equivElimR :: Prop r (Equiv r p q) -> Prop r (Imp r q p) equivElimR pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp q2p) -- Absurdity -- False |- P absurd :: Prop r (FALSE r) -> Prop r p absurd false = false >>= \(Not true2p) -> true2p truth -- Not-Inj -- (P |- False) |- ~P notInj :: forall r p. (Prop r p -> Prop r (FALSE r)) -> Prop r (Not r p) notInj p2false = return (Not p2any) where p2any :: forall q. Prop r p -> Prop r q p2any assumep = absurd (p2false assumep) -- Not-Elimination -- P, ~P |- Q notElim :: Prop r p -> Prop r (Not r p) -> Prop r q notElim p np = np >>= \(Not p2any) -> p2any p -- Excluded-Middle -- P \/ ~P exclMiddle :: forall r p. Prop r (Or r p (Not r p)) exclMiddle = propCC func1 where func1 :: (Or r p (Not r p) -> Prop r q) -> Prop r (Or r p (Not r p)) -- k :: Or r p (Not r p) -> Prop r q func1 k = return (OrR (return (Not func2))) where func2 :: Prop r p -> Prop r q func2 k' = k (OrL k') {- http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf -- A \/ ~A excmid :: Either a (a -> b) excmid = callcc (\k. Right (\a.k (Left a))) -} {- Classic2.hs:114:27: Couldn't match expected type `q' (a rigid variable) against inferred type `q1' (a rigid variable) `q' is bound by the type signature for `func2' at Classic2.hs:113:44 `q1' is bound by the type signature for `func1' at Classic2.hs:110:45 Expected type: Prop r q Inferred type: Prop r q1 In the expression: k (OrL k') In the definition of `func2': func2 k' = k (OrL k') -} -- False-Elimination -- (~P |- False) |- P Tim Newsham http://www.thenewsh.com/~newsham/

4 3

Categories in base
by Jean-Philippe Bernardy 15 Oct '07

15 Oct '07

Hello folks, Prompted by Ashley's proposal for Category class, I came up with the following module, which gives a summary of the overloading situation in the base package. Maybe it can help people find their way through all the available names... Failing that it surely was fun to come up with. :) -- JP {-# OPTIONS -fallow-undecidable-instances #-} import Prelude () class Functor f where (<$>) :: (a -> b) -> f a -> f b -- a.k.a: fmap, map, liftM class Functor f => Applicative f where return :: a -> f a -- a.k.a: Control.Applicative.pure (<*>) :: f (a -> b) -> f a -> f b -- a.k.a: ap -- f <$> g = return f <*> g class Applicative m => Monad m where (=<<) :: (a -> m b) -> m a -> m b -- a.k.a: flip (>>=) -- f <*> g = (\h -> (return . h) =<< g) =<< f class Category c where id :: c a a (.) :: c y z -> c x y -> c x z -- a.k.a: (<<<), flip (>>>) class Category a => Arrow a where pure :: (b -> c) -> a b c first :: a b c -> a (b, d) (c, d) instance Arrow a => Functor (a r) where -- (not defined as such in base, but ad-hoc) f <$> g = pure f . g -- instances for (->) instance Category (->) where id = \x -> x f . g = \x -> f (g x) instance Arrow (->) where pure = id first f = \(b, d) -> (f b, d)

2 1

Re: [Haskell-cafe] Let's do ListT right, finally
by Dan Piponi 15 Oct '07

15 Oct '07

On 10/14/07, Yitzchak Gale <gale(a)sefer.org> wrote: > Interesting. What do you mean by a "commutative monad"? > It can't be a monad with some sort of additional commutative > law, because the old ListT doesn't even satisfy the monad > laws. Or does it in some sense? If m is a commutative monad, then ListT m is a fully paid up monad, not just "in some sense". On a brief definition of commutative monads, and for some examples indicating how common they are, see SPJ's http://research.microsoft.com/~simonpj/papers/haskell-retrospective/Haskell… > OK, do you propose that we keep it and change its name? +1, dump the old one completely because you can't express what kind of thing the old ListT is in Haskell. I just want to make sure it gets a good epitaph. If someone answers SPJ's challenge #2 maybe it'll come back. -- Dan

1 0

Is this a known problem?
by ok 14 Oct '07

14 Oct '07

UltraSPARC II, Solaris 2.10, gcc 4.0.4 (gccfss), Haskell GHC 6.6.1 binary release. Trying to compile a simple file gives me oodles of errors because ghc is generating something that makes gcc generate lots of these: sethi %hi(<<some register>>),<<another register>> For people unfamiliar with SPARC assembly code, the %hi(...) operation returns the top bits of a *literal* address, it makes absolutely no sense to give it a register. I have tried this version of gccfss with lots of C code and have been unable to make it generate this construction; it's only ghc's .hc files that do it. Running gcc by hand on the .hc file produces 8 warnings ...lib/ghc-6.6.1/include/Regs.h: ###: warning: call-clobbered register used for global register variable -DNO_GLOBAL_REG_DECLS eliminated that. Comparing the .s file produced using 'ghc -S' with the .s file produced by gcc'ing the .hc produced some illumination: .section ".text",#slloc,#execinstr,#progbits .align 4 #if GHC .text .align 4 #endif s4AK_ret: save %sp,-96,%sp #if GHC sethi %hi(%l1),%i2 add %i2,%lo(%l1),%i5 ld [%i2+%lo(%l1)],%i2 ld [%i2],%l7 lduh [%l7-2],%l6 ... #else sethi %hi(MainCapability),%i5 add %i5,%lo(MainCapability),%i2 ld [%i2+8],%i5 ld [%i5],%i4 lduh [%i4-2],%i3 ... #endif What with one thing and another, I'm not really sure that it's gcc's fault.

2 1

do
by PR Stanley 14 Oct '07

14 Oct '07

Hi "do", what's its role? I know a few uses for it but can't quite understand the semantics - e.g. do putStrLn "bla bla" So, what does do, do? Thanks, Paul

4 4

more functions to evaluate
by PR Stanley 14 Oct '07

14 Oct '07

Hi folks Any comments and/or criticisms no matter how trivial on the following please: wordSize :: [Int] -> Int wordSize xs = head (dropWhile (<(length xs)) $ iterate (*2) 8) intToBinWord :: Int -> [Int] intToBinWord n = reverse (take elements (xs ++ repeat 0)) where xs = reverse (intToBin n) elements = wordSize xs Thanks, Paul

8 11

Can every monad can be implemented with Cont? (was: New slogan for haskell.org)
by apfelmus 14 Oct '07

14 Oct '07

Don Stewart wrote: > allbery: > >> Didn't someone already prove all monads can be implemented in terms >> of Cont? >> > > Cont and StateT, wasn't it? > And the schemers have no choice about running in StateT :) You sure? I want to see the proof :) Last time I stumbled upon something like this, the "proof" was to embed every monad m in the type type Cont m a = forall b . (a -> m b) -> m b with an instance Monad (Cont m) where ... _independent_ of whether m is a monad or not. The problem I see with it is that we didn't really encode m with it since we're still dependent on return and (>>=) via project :: Monad m => Cont m a -> m a project f = f return and inject :: Monad m => m a -> Cont m a inject x = (x >>=) I mean, the starting point for a concrete monad M are some primitive operations like get :: M s put :: s -> M () and a function observe :: M a -> (S -> (a,S)) together with laws for the primitive operations (= operational semantics) observe (put s >>= x) = \_ -> observe (x ()) s observe (get >>= x) = \s -> observe (x s ) s and for return observe (return a) = \s -> (a,s) Now, implementing a monad means to come up with a type M and functions (>>=) and return that fulfill the monad laws. (In general, the result type of observe is _not_ M a !) This can be done with the standard trick of implementing stuff as constructors (see Unimo for details http://web.cecs.pdx.edu/~cklin/papers/unimo-143.pdf) But - and that's the problem - I don't see how it can be done with Cont in all cases. It works for the above state monad (*) but what about primitives like mplus :: m a -> m a -> m a callcc :: ((a -> m r) -> m r) -> m a that have monadic arguments in a contravariant position (possibly even universally quantified)? Regards, apfelmus *: Here you go: type Observe s a = s -> (a,s) type State s a = Cont (Observe s) a get = \x -> (\s -> observe (x s ) s) -- law for get put s = \x -> (\_ -> observe (x ()) s) -- law for put observe f = f $ \a -> (\s -> (a,s)) -- law for observe (return a)

4 3