tag:blogger.com,1999:blog-11295132.post5798722270156006834..comments2016-05-15T21:44:34.495-07:00Comments on A Neighborhood of Infinity: Beyond MonadsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger25125tag:blogger.com,1999:blog-11295132.post-43985033987251302752010-05-22T20:38:16.449-07:002010-05-22T20:38:16.449-07:00Yair,
This does not represent the value of the s...Yair, <br /><br />This does not represent the value of the state variable inside the type system; rather it allows the type of state variable to vary over the course of the computation.<br /><br />If you can imagine an example where you want to store two possible types, say either an integer or a string, in the state variable, then one way to do it is to use <i>State (Either Integer String) a</i>. If you know whether the state variable is a string or an integer based solely on where you are in the computation, you can use the parameterized state monad in this post, and avoid the use of <i>Either</i>.Leon Smithhttp://www.blogger.com/profile/06462854866941248768noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-2211819261185938652010-05-22T07:21:58.831-07:002010-05-22T07:21:58.831-07:00Cool. I guess this can be described as a type-leve...Cool. I guess this can be described as a type-level-state monad?Yairhttp://www.blogger.com/profile/03938694674587025243noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-51328940573074762752009-02-26T17:06:00.000-08:002009-02-26T17:06:00.000-08:00mike,I still haven't got around to thinking for my...mike,<BR/><BR/>I still haven't got around to thinking for myself about what this construction is from a category theoretical perspective. End(C) was just a guess based on ordinary monads being monoids. I'll have to return to this when I have a moment.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-83948683755770422712009-02-26T16:46:00.000-08:002009-02-26T16:46:00.000-08:00sigfpe,In a normal monad, bind has type m a ->...sigfpe,<BR/><BR/>In a normal monad, bind has type<BR/> m a -> ( a -> m b ) -> m b<BR/>where m:C -> C is a functor and a,b in C.<BR/><BR/>Your bind has type<BR/> ( m s1 s2 ) a -> <BR/> ( a -> (m s1 s2) b ) -> ( m s1 s2 ) b,<BR/>where <BR/> a,b in C, <BR/> s1, s2 in S, <BR/>and (ostensibly) <BR/> m(s1, s2):C -> C.<BR/><BR/>So you have a different functor from C to C for each pair (s1, s2) in S. However, you also forbid composition of such functors unless the types match, so the functors aren't really from C to C, they're from s1 x C to s2 x C. <BR/><BR/>This means you can't possibly be describing a category object in End(C). You have a 2-category whose objects are copies of C indexed by elements of S, functors between the categories, and natural morphisms between the functors.<BR/><BR/>It's a lovely construction, and well illustrated, just not the one you might have thought you were getting.mikehttp://www.blogger.com/profile/03408641732412584050noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-47234372484140120112009-02-24T03:23:00.000-08:002009-02-24T03:23:00.000-08:00Better late than never :Phttp://groups.google.com/...Better late than never :P<BR/><BR/>http://groups.google.com/group/comp.lang.haskell/browse_thread/thread/98384971db91201e/44a51f58ebb6c6ad#44a51f58ebb6c6adDanhttp://www.blogger.com/profile/02467793406608705828noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30938055880749689942009-02-18T12:04:00.000-08:002009-02-18T12:04:00.000-08:00mike,Haven't digested all of your comment yet. But...mike,<BR/><BR/>Haven't digested all of your comment yet. But briefly, a category object in End(C) is exactly what I'm thinking of. But I haven't expanded out the full definition myself to ensure all of the maps are exactly what they need to be.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-48850427222089502362009-02-18T11:35:00.000-08:002009-02-18T11:35:00.000-08:00A category object in Set consists of:- two sets O ...A category object in Set consists of:<BR/>- two sets O and M (objects and morphisms)<BR/>- a function i:O -> M (picks out the identity morphism)<BR/>- two functions s,t:M -> O (source and target)<BR/>- a function o:X -> M (composition), where X is a set equipped with two functions i,j:X -> M such that s o i = t o j (that is, it's the set of composable pairs and i,j pick out the first or second element)<BR/>such that the usual relations hold.<BR/><BR/>Category objects can be defined in any category with pairwise pullbacks:<BR/><BR/>A category object in C consists of<BR/>- two objects O, M<BR/>- a morphism i:O -> M<BR/>- two morphisms s, t:M -> O<BR/>- a morphism o:X -> M where X is equipped with two morphisms i,j:X -> M s.t. s o i = t o j<BR/>such that the usual relations hold.<BR/><BR/>The generalization you describe is as follows:<BR/><BR/>A "parametrized monad" consists of<BR/>- two sets O, M (where the elements of O are categories and the elements of M are functors between them)<BR/>- a function i:O -> M (picking out the identity functor on each category)<BR/>- two functions s,t:M -> O (source and target of the functors)<BR/>- a function o:X -> M (composition of functors)<BR/><BR/>But this is just a subcategory of Cat! What's going on? Just as a monoid is a one-object category, a monoidal category is a one-object 2-category. The generalization you describe moves from the monoidal category End(C) to a 2-category with more objects. So the real term you want isn't "parameterized monad", it's "sub-2-category of Cat". <BR/><BR/>A different generalization would be to consider a category object in End(C):<BR/><BR/>A category object in End(C) consists of<BR/>- two functors O, M<BR/>- a natural transformation i:O -> M<BR/>- two natural transformations s, t:M -> O<BR/>- a natural transformation o:X -> M where the functor X is equipped with two natural transformations i,j:X -> M s.t. s o i = t o j<BR/>such that the usual relations hold.<BR/><BR/>Can you come up with a use case for this one?mikehttp://www.blogger.com/profile/03408641732412584050noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-26244643123465001632009-02-17T17:50:00.000-08:002009-02-17T17:50:00.000-08:00Ryan,I think "Indexed monad" and IxMonad are much ...Ryan,<BR/><BR/>I think "Indexed monad" and IxMonad are much better names. I'll check out Tov's session types paper.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-87586842016431772402009-02-17T17:31:00.000-08:002009-02-17T17:31:00.000-08:00Parametrized monads were also used in a Haskell Wo...Parametrized monads were also used in a Haskell Workshop 2008 paper with the name "class Monadish".<BR/><BR/>An implementation of the concept is available at http://hackage.haskell.org/cgi-bin/hackage-scripts/package/CoroutineRyan Ingramnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-42034892472327928512009-02-15T11:22:00.000-08:002009-02-15T11:22:00.000-08:00I've been mucking about with functors between ...I've been mucking about with functors between slice categories. Er, um,<BR/><BR/>type x :->: y = forall i. x i -> y i<BR/><BR/>class IFunctor (t :: (* -> *) -> * -> *) where<BR/> imap :: (x :->: y) -> (t x :->: t y)<BR/><BR/>To me this suggests.<BR/><BR/>class IMonad (t :: (* -> *) -> * -> *) where<BR/> iret :: x :->: t x<BR/> ibind :: (x :->: t y) -> (t x :->: t y)<BR/><BR/>Can we get back these domino-style parametrized monads?<BR/><BR/>Seems so.<BR/><BR/>data ILike :: * -> * -> * -> * where<BR/> ILike :: x -> ILike x i i<BR/><BR/>type Domino t i j x = t (ILike x j) i<BR/><BR/>dret :: IMonad t => x -> Domino t i i x<BR/>dret = iret . ILike<BR/><BR/>iTweak :: (x -> Domino t j k y) -> (ILike x j :->: t (ILike y k))<BR/>iTweak f (ILike x) = f x<BR/><BR/>dbind :: IMonad t => (x -> Domino t j k y) -> Domino t i j x -> Domino t i k y<BR/>dbind f b = ibind (iTweak f) b<BR/><BR/>Not sure where I'm going with this. Just thought I'd mention it. I detect traces of Dr Hancock...Conorhttp://strictlypositive.orgnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-44595271594381804102009-02-15T08:49:00.000-08:002009-02-15T08:49:00.000-08:00augustss,It'd be easy to test to see what many of ...augustss,<BR/><BR/>It'd be easy to test to see what many of the consequences might be: try recompiling a non-trivial body of code with a parameterised monad library.<BR/><BR/>My main concern is with monad transformers. The types of the parameterised version will carry a lot of information. We could start getting some pretty big signatures.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-14829809018169944552009-02-15T08:26:00.000-08:002009-02-15T08:26:00.000-08:00Augustss: My experience has been both. Sometim...Augustss: My experience has been both. Sometimes you do get impenetrable error messages; often because some definition you got wrong a page or two of code ago actually does typecheck, whereas it wouldn't have previously.<BR/><BR/>I quickly learned to frequently use ghci to infer the most general type of new definitions. If the type appeared to be right, I'd copy and paste it into my code, if it was obviously wrong, I'd try again. When problems arose, sometimes it took a fair bit of mental effort to figure out exactly what they were. <BR/><BR/>There is definitely higher type overhead, at least in the short run. But it puts the type system to better work _for you_, among other compelling advantages.Leon Smithhttp://www.blogger.com/profile/06462854866941248768noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-47051480610445047332009-02-15T05:58:00.000-08:002009-02-15T05:58:00.000-08:00GHC supports do-notation for parameterized monads ...GHC supports do-notation for parameterized monads just fine, as it turns out.<BR/><BR/>I tried to write some code here to show you how to do it but Blogger doesn't allow me to use the proper tags when commenting so it will just look like crap. Instead here is a link to <A HREF="http://computationalthoughts.blogspot.com/2009/02/comment-on-parameterized-monads.html" REL="nofollow">my blog</A> which shows how to do it.Josefhttp://www.blogger.com/profile/13272830598221833253noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-89093125596818127362009-02-15T05:27:00.000-08:002009-02-15T05:27:00.000-08:00GHC does support do-notation for parameterised mon...GHC <B>does</B> support do-notation for parameterised monads. With GHC 6.10 (at least) you merely need to use {-# LANGUAGE NoImplicitPrelude #-}<BR/>and GHC will resolve do-notation to use whatever is in scope for (>>=), (>>) and "return". Parameterised monads are also used in Oleg et al's lightweight static resources paper.Thomas Schillinghttp://www.blogger.com/profile/04274984206279511399noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-87880709848657204772009-02-15T05:20:00.000-08:002009-02-15T05:20:00.000-08:00"At the very least, do-notation needs to be a..."At the very least, do-notation needs to be adapted to support ParameterisedMonad. "<BR/><BR/>This is already possible in Ghc using -XNoImplicitPrelude or the corresponding LANGUAGE pragma.<BR/><BR/>---<BR/><BR/>Just for fun, let me try to continue with your idea. Instead of taking (>>=) as a primitive, I prefer fmap, join and Applicative stuff. So:<BR/><BR/>> class ParameterisedFunctor m where<BR/>> fmap :: (a -> b) -> (m s s a) -> (m s s b)<BR/>> <BR/>> class ParameterisedFunctor m => ParameterisedPointed m where<BR/>> pure :: a -> m s s a<BR/>> <BR/>> class ParameterisedPointed m => ParameterisedApplicative m where<BR/>> (<*>) :: m s1 s2 (a -> b) -> m s2 s3 a -> m s1 s3 b<BR/>> <BR/>> class ParameterisedApplicative m => ParameterisedMonad m where<BR/>> join :: m s1 s2 (m s2 s3 a) -> m s1 s3 a<BR/><BR/>Now take the ParameterisedApplicative class. For normal Applicatives there is a Dual instance that reverses the order of effects, i.e.:<BR/><BR/>> (<**>) :: m a -> m (a -> b) -> m b<BR/><BR/>Here the reversed ordering is not clear from the type. However, with ParameterizedApplicative:<BR/><BR/>> (<**>) :: m s1 s2 a -> m s2 s3 (a -> b) -> m s1 s3 b<BR/><BR/>We <I>do</I> see the ordering of effects in the type.<BR/><BR/>---<BR/><BR/>Also, the type "m s1 s2 a" reminds me a lot of the types of Control.Category. Is there something equivalent to the Kleisli wrapper?<BR/><BR/>> newtype Kleisli m a b = Kleisli <BR/>(a -> m b)Twan van Laarhovenhttp://www.blogger.com/profile/18138442561179666544noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-37955056420458425672009-02-15T03:51:00.000-08:002009-02-15T03:51:00.000-08:00MIND = BLOWNThis is awesome stuff!MIND = BLOWN<BR/><BR/>This is awesome stuff!Bonushttp://www.blogger.com/profile/02725486955962218311noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-10645091153067911272009-02-15T03:45:00.000-08:002009-02-15T03:45:00.000-08:00Just to note that some Haskell programmers were us...Just to note that some Haskell programmers were using this extended notion of ParametrisedMonad even before the do-notation was standardised. For instance, back in 1994-5, Niklas Röjemo used this idiom extensively inside the nhc12 and nhc13 compilers. See <A HREF="http://darcs.haskell.org/york-compiler98/State.hs" REL="nofollow">here</A> for evidence.malcolmhttp://www.blogger.com/profile/08863672971675777868noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-81379145644663003692009-02-15T03:36:00.000-08:002009-02-15T03:36:00.000-08:00I agree. I always wanted monads to be more flexibl...I agree. I always wanted monads to be more flexible, but as not so experienced Haskell programmer I thought it is something wrong with me since hackers of Haskell would have seen it a long time ago, wouldn't they? I feel relieved (a little bit ^^). Thank you sigfpe!dtldareknoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-42645090955167537702009-02-15T03:17:00.000-08:002009-02-15T03:17:00.000-08:00Dan, have you tried to use do-notation with this d...Dan, have you tried to use do-notation with this definition of Parameterised Monads ? If so, what was the problem? Since GHC supports rebindable syntax, do-notation should just work when throwing in a NoImplicitPrelude pragma.<BR/><BR/>This is related to a (wilder) notion of parameterised monads that Edward Kmett <A HREF="http://comonad.com/reader/2007/parameterized-monads-in-haskell/" REL="nofollow">gave</A> some time ago.Pepe Iborrahttp://www.blogger.com/profile/07317126950309336541noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-5515970047264405192009-02-15T02:52:00.000-08:002009-02-15T02:52:00.000-08:00ParametrizedMonad is indeed a very useful abstract...ParametrizedMonad is indeed a very useful abstraction. But it makes me wonder what happens to type inference and to error messages. I just don't know the answer.<BR/><BR/>Can the extra flexibility cause ambiguities?<BR/><BR/>What happens when one makes an error? Might it still type check? Or give an even stranger type error?augustsshttp://www.blogger.com/profile/07327620522294658036noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-55367434261008007422009-02-15T01:55:00.000-08:002009-02-15T01:55:00.000-08:00To get do-notation, can't you just use NoImplicitP...To get do-notation, can't you just use NoImplicitPrelude?Ganesh Sittampalamhttp://www.blogger.com/profile/16862546723726662511noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-49534432288549125952009-02-15T00:27:00.000-08:002009-02-15T00:27:00.000-08:00So shouldn't they be called arrowads instead since...So shouldn't they be called arrowads instead since they are no longer abstract monoids?Kefernoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-14755426227772722752009-02-15T00:13:00.001-08:002009-02-15T00:13:00.001-08:00Here lies a dependently typed version: http://www....Here lies a dependently typed version: http://www.cs.nott.ac.uk/~nad/repos/lib/Category/Monad/Indexed.agdaJean-Philippe Bernardyhttp://www.blogger.com/profile/09574587903886283067noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-58498879230812434432009-02-15T00:11:00.000-08:002009-02-15T00:11:00.000-08:00Here lies a dependently typed version: http://www....Here lies a dependently typed version: http://www.cs.nott.ac.uk/~nad/repos/lib/Category/Monad/Indexed.agdaJean-Philippe Bernardyhttp://www.blogger.com/profile/09574587903886283067noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-76137775584508380072009-02-14T22:59:00.000-08:002009-02-14T22:59:00.000-08:00Nice observation. Certainly, one major reason w...Nice observation. Certainly, one major reason why parameterized monads are so attractive is exactly because of the easy upgrade path. Anybody who is comfortable writing monadic code can get started very easily, and allow the typechecker to do the heavy mental lifting for them.Leon Smithhttp://www.blogger.com/profile/06462854866941248768noreply@blogger.com