- Haskell-Cafe - Haskell.org

Origin of monad transformers (was: Algebraic Effects?)
by Olaf Klinke 20 Sep '18

20 Sep '18

> The only monads with distributive laws are in Data.Distributive, and > they're all isomorphic to (->) e for some e. So that's effectively > ReaderT. That is true for this particular signature of distributive law, and I find this a fascinating result. Especially because there are Haskell terms witnessing this categorical fact. In [1, Theorem 2.4.2] it is stated (as I understand it) that if two monads H and K have a distributive law, then the first is a functor on the Kleisli category of the second while the second is a functor on the Eilenberg-Moore category of the first. In the same paper, Section 4 describes monads on Set (including e.g. trees, bags, Maybe) which distribute over all commutative monads. But maybe one does not need such heavy categorical machinery to describe where monad transformers in Haskell come from. Consider the following. There are at least three kinds of monad transformers t in mtl: (1) t m a = m (t' a) for some monad t' (e.g. ExceptT) (2) t m a = t' (m a) for some monad t' (e.g. ReaderT) (3) t m a = g (m (f a)) for some functors g and f. (e.g. StateT) Only (2) is of the Data.Distributive kind, but all three can be unified under the following scheme: Lemma: If F ⊣ G is an adjunction where F: C → D and G: D → C are functors, and if M: D → D is a monad on D, then G∘M∘F is a monad. Proof: One can factor M through the Kleisli category of M L ⊣ R where L: D → Kleisli(M) and R: Kleisli(M) → D. Since adjoints compose, we have L∘F ⊣ G∘R and G∘R∘L∘F = G∘M∘F. q.e.d. There is another interesting paper [2] showing that for certain class of monads, checking the conditions for a distributive law is easier than the general case. Olaf [1] http://emis.ams.org/journals/TAC/volumes/18/7/18-07.pdf [2] https://doi.org/10.1016/S0022-4049(01)00097-4

1 0

Typeclassopedia for numbers
by Dominik Schrempf 20 Sep '18

20 Sep '18

Hello, the Typeclassopedia[1] lists standard Haskell (algebraic ?) type classes and their relations. I was wondering if a similar construct also exists for numeric type classes (and probably also their instances), since I am always struggling with how, e.g., 'Integral' number are related to 'Fractional' and so on and so forth. Thanks, Dominik [1] https://wiki.haskell.org/Typeclassopedia

2 3

Re: [Haskell-cafe] Parsing LocalTime from Unix seconds
by Olaf Klinke 19 Sep '18

19 Sep '18

Is the result of parsing Unix seconds to LocalTime even well-defined? A LocalTime could be in any time zone, while Unix epoch is relative to a certain time-point in UTC. Hence the parse result must depend on what time zone the LocalTime is referring to. Olaf

6 7

Call for lightning talks and participation -- Haskell Implementors' Workshop
by Joachim Breitner 19 Sep '18

19 Sep '18

Call for Contributions ACM SIGPLAN Haskell Implementors’ Workshop Sunday, 23 September, 2018 https://icfp18.sigplan.org/track/hiw-2018-papers Co-located with ICFP 2018 St. Louis, Missouri, US https://conf.researchr.org/home/icfp-2018 The Haskell Implementors Workshop is only one week away! Time to look at our great program at https://icfp18.sigplan.org/track/hiw-2018-papers#program and plan your day! Lightning Talks --------------- Like in the previous years, we will have slots for lightning talks. And because they were so successful last year, we will have more! *Topics* Anything related to Haskell implementations, fun uses of Haskell etc. goes. Feel free to tell us about ongoing work, to entertain, to rant, to stir a debate! (If you ever have been to a security or crypto conference, you might have attended their “rump session”. While there will not be alcohol involved at HIW, I hope that we can still match their creativity and insightful fun.) *Rules* * There are 3 sets of 3 lightning talks. * Sign-up is on day of the event, in person, on paper. No prior registration possible. * Lightning talks are 8 mins or less. If you know that your lightning talk takes less time, please say so, and maybe we can put four lightning talks into the slot. * Lightning talks do not count as peer-reviewed publications and are not published in the conference proceedings. Program Committee ----------------- * Edwin Brady (University of St. Andrews, UK) * Joachim Breitner – chair (DFINITY / University of Pennsylvania) * Ben Gamari (Well-Typed LLP) * Michael Hanus (Kiel University) * Roman Leshchinsky (Facebook) * Niki Vazou (University of Maryland) Contact ------- * Joachim Breitner <joachim(a)cis.upenn.edu> -- Joachim Breitner former post-doctoral researcher http://cis.upenn.edu/~joachim

2 1

Algebraic Effects?
by Olaf Klinke 18 Sep '18

18 Sep '18

> Have distributive laws [1] ever been used for monad composition in > Haskell? After all, two monads with a distributive law compose. > > Till There is the distributive package on Hackage, which at least matches the type of the nLab definition. Many common monad transformers stem from monads that are "universally distributive" in the following sense: If t is a monad transformer, then for all other monads m a function with one of the following types can be defined: t Identity (m a) -> m (t Identity a) m (t Identity a) -> t Identity (m a) For which transformers is this the case? For those where t m a is isomorphic to one of the two types t Identity (m a) m (t Identity a) Examples: distr_Reader :: Functor m => m (r -> a) -> r -> m a distr_Reader = \m -> \r -> fmap ($r) m distr_Writer :: Functor m => (w,m a) -> m (w,a) distr_Writer = \(w,m) -> fmap ((,) w) m distr_Either :: Applicative m => Either e (m a) -> m (Either e a) distr_Either (Left e) = pure (Left e) distr_Either (Right m) = fmap Right m distr_Maybe :: Applicative m => Maybe (m a) -> m (Maybe a) distr_Maybe Nothing = pure Nothing distr_Maybe (Just m) = fmap Just m More generally, two monads distribute when one is an endofunctor on the Kleisli category of the other. (The nLab page says Eilenberg-Moore category, I'm not sure whether the two statements are equivalent.) A morphism in the Kleisli category of m is a function a -> m b. An endofunctor f on the Kleisli category must map such a function to a function f a -> m (f b). For example, kleisli_Maybe :: Applicative m => (a -> m b) -> Maybe a -> m (Maybe b) kleisli_Maybe _ Nothing = pure Nothing kleisli_Maybe k (Just a) = fmap Just (k a) kleisli_Reader :: Functor m => (a -> r -> b) -> m a -> r -> m b kleisli_Reader k x r = fmap (flip k r) x Notice that in the former case we used the Kleisli category of m whereas in the latter case we used the Kleisli category of Reader. The more general picture involves an adjunction and the monad m. This covers StateT and the continuation monad. It is well-known that any adjunction F -| G between two categories gives rise to a monad, namely GF. Suppose F:C->D and G:D->C are functors. The adjuntion says that the hom-sets D(Fa,b) and C(a,Gb) are naturally isomorphic. For the state monad, C = Hask (the category of Haskell types and functions) D = Hask, F = (,) s G = (->) s and the isomorphism of hom-sets is currying and uncurrying between (s,a) -> b and a -> (s -> b). In case of the continuation monad Cont r a = (a -> r) -> r, we have C = Hask, D = Hask^op (Hask with direction of arrows reversed) F a = (a -> r) G b = (b -> r) and the isomorphism of hom-sets is between a -> (b -> r) and b -> (a -> r) where the latter is Hask^op(Fa,b). In the case of StateT, since the intermediate category D is Hask, any functor m is an endofunctor on the intermediate category. I do not recall under which conditions the composite GMF is a monad. Olaf

1 0

natural mergesort in Data.List
by Christian Sternagel 18 Sep '18

18 Sep '18

Dear Cafe, some years ago I formalized the mergesort implementation [1] from http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html… (as far as I can tell it didn't change since 2012) in the proof assistant Isabelle/HOL [2]. More specifically, I proved its functional correctness (the result is sorted and contains all elements of the input with exactly the same multiplicities) and that it is a stable sorting algorithm. Very recently I also formalized a complexity result in Isabelle/HOL, namely that the number of comparisons is bounded from above by n + n * ⌈log 2 n⌉ for lists of length n. For this proof I had to change the definition of "sequences", "ascending", and "descending" slightly. Now here is my question: Does anyone now of reasons why the current implementation of "sequences" is allowed to produce spurious empty lists in its result? The version I used in my formalization only differs in the following three spots: sequences [x] = [[x]] -- this is the only important change, since sequences [] = [] -- then the result does not contain empty lists instead of sequences xs = [xs] and ascending a as [] = let !x = as [a] in [x] instead of ascending a as bs = let !x = as [a] in x : sequences bs and descending a as [] = [a:as] instead of descending a as bs = (a:as) : sequences bs [1] https://www.isa-afp.org/entries/Efficient-Mergesort.html [2] http://isabelle.in.tum.de/

3 6

Get-together at ICFP about Haskell in K-12 education
by Chris Smith 18 Sep '18

18 Sep '18

Hello Haskell community! I've been floating an idea around about hosting a get-together in St. Louis for anyone interested in Haskell at the K-12 (pre-university) level. Some of you know that this has been a big passion of mine for the last 8 years or so. I'd love to discuss with others while a lot of us are in the same place -- whether you're interested in organized teaching, or just teaching your own kids, or just curious about the idea. I've put together this form to collect RSVPs and availability. Interest Form <https://docs.google.com/forms/d/e/1FAIpQLSdJPWIMroEyBuqP15ngmZrp0XwwP-C5uuE…> Thanks, Chris Smith

1 2

CoqPL 2019: Call for Presentations
by Robbert Krebbers 17 Sep '18

17 Sep '18

=================================================================== CoqPL 2019 5th International Workshop on Coq for Programming Languages -- January 19, 2019, co-located with POPL Cascais/Lisbon, Portugal CALL FOR PRESENTATIONS https://popl19.sigplan.org/track/CoqPL-2019 =================================================================== Workshop Overview ----------------- The series of CoqPL workshops provide an opportunity for programming languages researchers to meet and interact with one another and members from the core Coq development team. At the meeting, we will discuss upcoming new features, see talks and demonstrations of exciting current projects, solicit feedback for potential future changes, and generally work to strengthen the vibrant community around our favorite proof assistant. Topics in scope include: - General purpose libraries and tactic language extensions - Domain-specific libraries for programming language formalization and verification - IDEs, profilers, tracers, debuggers, and testing tools - Reports on ongoing proof efforts conducted via (or in the context of) the Coq proof assistant - Experience reports from Coq usage in educational or industrial contexts Workshop Format --------------- The workshop format will be driven by you, members of the community. We will solicit abstracts for talks and proposals for demonstrations and flesh out format details based on responses. We expect the final program to include experiment reports, panel discussions, and invited talks (details TBA). Talks will be selected according to relevance to the workshop, based on the submission of an extended abstract. To foster open discussion of cutting edge research which can later be published in full conference proceedings, we will not publish papers from the workshop. However, presentations will be recorded and the videos made publicly available. Submission details ------------------ Submission page: https://coqpl19.hotcrp.com/ Submission: Monday, October 15, 2018. Notification: Thursday, November 8, 2018. Workshop: Saturday, January 19, 2019 (tentative, date to be confirmed soon). Submissions for talks and demonstrations should be described in an extended abstract, between 1 and 2 pages in length (excluding the bibliography). We suggest formatting the text using the two-column ACM SIGPLAN latex style (9pt font). Templates are available from the ACM SIGPLAN page: http://www.sigplan.org/Resources/Author. Program Committee ----------------- Chairs: - Robbert Krebbers Delft University of Technology, the Netherlands - Ilya Sergey University College London, UK Program Committee: - Olivier Danvy Yale-NUS College, Singapore - Ronghui Gu Columbia University, USA - William Mansky Princeton University, USA - Talia Ringer University of Washington, USA - Gordon Stewart Ohio University, USA - Enrico Tassi Inria, France - Anton Trunov IMDEA Software Institute, Spain - Edwin Westbrook Galois, Inc., USA - Steve Zdancewic University of Pennsylvania, USA

1 0

Parsing LocalTime from Unix seconds
by Marc Busqué 14 Sep '18

14 Sep '18

In GHCi ``` :m +Data.Time parseTimeM True defaultTimeLocale "%s" "1535684406" :: Maybe UTCTime -- => Just 2018-08-31 03:00:06 UTC parseTimeM True defaultTimeLocale "%s" "1535684406" :: Maybe LocalTime -- => Just 1970-01-01 00:00:00 ``` Why? ¯\(°_o)/¯ Marc Busqué http://waiting-for-dev.github.io/about/

2 2

Request for example of putting LaTeX in Haskell code comments for Haddock processing.
by David Banas 13 Sep '18

13 Sep '18

Hi all, Can anyone provide a know working example (GHC 8.4.3) of embedding LaTeX in Haskell source code comments intended for Haddock processing? Both in-line and block, if you’ve got them, would be great. Thanks! -db

5 5