- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] Where do I start if I would like help improve GHC compilation times?
by Johannes Waldmann 19 Apr '17

19 Apr '17

> it would be quite helpful if `pretty` > gained a special-case for the infinite band-width case Absolutely +1 this. Not "pretty" but similar: https://github.com/jwaldmann/wl-pprint-text/commit/7843d96db57ab01c0be336a5… - J.W.

2 1

Re: [Haskell-cafe] Wow Monads!
by David McClain 19 Apr '17

19 Apr '17

Hi Sergiu, Excellent point you make about type checking versus provably correct code. I probably allowed myself to be lulled by a false equivalence many times in the past, confusing one for the other under pressure to get something working. But then, how many programmers actually produce provably correct code? I can see that happening very easily in the small. But for overall large programs? - DM > On Apr 18, 2017, at 14:36, Sergiu Ivanov <sivanov(a)colimite.fr> wrote: > > > Hello David, > > Thanks a lot for sharing your opinions, I find it very interesting. > > Thus quoth David McClain at 19:26 on Mon, Apr 17 2017: >> >> That’s when I began migrating back over to my old standby Lisp >> system. I live inside of my Lisp all day long, for days on end. It is >> a whole ecosystem. There is not crisp boundary of edit / compile / >> debug. It is all incremental and extensional. I think that kind of >> environment, regardless of language, is the holy grail of computing. > > Just a small question: have you ever tried Smalltalk/Squeak/Pharo? (I'm > in no way affiliated.) > > These guys seem to be quite keen on blending the edit/compile/debug > boundaries. > > -- > Sergiu

2 1

Re: [Haskell-cafe] Problem with tuple with one element constrained
by Justus Adam 19 Apr '17

19 Apr '17

I am not sure really what you are trying to do, but here are a few approaches which I think may solve your problem. 1. Calculate the monadic value outside or fmap over the tuple constructor for instance do x <- functionCall return (y, x) or (y, ) <$> functionCall (uses the TupleSections extension) 2. Use explicit forall and scoped type variables If you really want to return a tuple with that monadic value from a function then the `Monad m` constraint must be on the function itself. Like so Compiled with ExplicitForAll and ScopedTypeVariables myFunction :: forall m. Monad m => m ... myFunction = let x :: m SomeType (y, x) = (..., return ...) in ... Which binds `m` to be of the same type as the outer `m`. This is necessary as there must be some way that even from outside the function we can figure out what concretely `m` actually is. Ergo it must be bound in some way to the functions type signature. 3. ExistentialTypes If you __really__ think you only need a `Monad` constraint on this type (which I doubt) you can use an existential to wrap things into generic monads. (Uses ExistentialTypes) data ExtMonad a = forall m. Monad m => ExtMonad m a The thing I don't quite understand is, if you have a function call, which produces the value, doesn't that call return a concrete monad? Rather than just `Monad m`? It sounds to me like you're actually barking up the wrong tree when you try and do what you are doing here so I suggest using something like approach 1 or 2 and perhaps rethinking if your problem may lay somewhere else. Regards Justus -- Justus Adam dev(a)justus.science On Tue, Apr 18, 2017, at 12:41 PM, Tyson Whitehead wrote: > I've been unable to get the following (simplified) code to be accepted by > GHCi (8.0.1 and 8.0.2) > > Prelude> let (x, y) = (1, return 2) > <interactive>:1:5: error: > • Could not deduce (Monad m0) > from the context: Num t > bound by the inferred type for ‘x’: > Num t => t > at <interactive>:1:5-24 > The type variable ‘m0’ is ambiguous > • When checking that the inferred type > x :: forall a (m :: * -> *) t. (Num a, Num t, Monad m) => t > is as general as its inferred signature > x :: forall t. Num t => t > > and I don't seem to be able to provide a type signatures that GHCi is > okay with > > Prelude> let { x :: Int; y :: Monad m => m Int; (x, y) = (1, return 2) } > <interactive>:5:40: error: > • Ambiguous type variable ‘m0’ > prevents the constraint ‘(Monad m0)’ from being solved. > • When checking that the inferred type > x :: forall a (m :: * -> *) t (m1 :: * -> *). > (Num a, Num t, Monad m) => > t > is as general as its signature > x :: Int > > Prelude> let (x, y) = (1, return 2) :: (Int, Monad m => m Int) > <interactive>:4:31: error: > • Illegal qualified type: Monad m => m Int > GHC doesn't yet support impredicative polymorphism > • In an expression type signature: (Int, Monad m => m Int) > In the expression: (1, return 2) :: (Int, Monad m => m Int) > In a pattern binding: > (x, y) = (1, return 2) :: (Int, Monad m => m Int) > > Prelude> let (x,y) = (1,return 2) :: Monad m => (Int, m Int) > <interactive>:7:5: error: > • Ambiguous type variable ‘m0’ > prevents the constraint ‘(Monad m0)’ from being solved. > • When checking that the inferred type > x :: forall (m :: * -> *). Monad m => Int > is as general as its inferred signature > x :: Int > > It seems the constraint on y leaks to x where it isn't well formed? Any > help and/or explanations would be greatly appreciated. In my actual code > the assignment is from the return value of a function so I can't just > split it into two separate statements. > > Thanks! -Tyson > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post.

1 0

Cross-compiling GHC
by Jan von Löwenstein 19 Apr '17

19 Apr '17

Hi, I would like to have an integer-simple GHC for Mac and Linux. As there is no official download for that I should probably build it myself. My CI server is running Linux containers though. When https://ghc.haskell.org/trac/ghc/wiki/Building/CrossCompiling says "build must equal host", does that mean I cannot produce a mac ghc with Linux ci server? How do others produce ghc for mac or Windows? Best Jan

2 2

slow type level function
by Baojun Wang 19 Apr '17

19 Apr '17

Hello cafe, I tried to play with some type level natural numbers, and it seems type level function is quite slow, for instance: (full source) https://gist.github.com/wangbj/5939aa7a30c3d756d98f5b5775e162a6 data Z data S n class KnownNat n where natSing :: n -> Integer instance KnownNat Z where natSing _ = 0 instance KnownNat n => KnownNat (S n) where natSing _ = 1 + natSing (undefined :: n) natVal :: KnownNat n => n -> Integer natVal = natSing natSing doesn't seems to know how to optimize when KnownNat is very big (i.e: 10000), I tried Peano Add/Mul, and they are very slow to be really useful. Is there any ways to improve this? How fully dependent typed language such as Adga/Idris handle this, do they have the same performance issue? Thanks baojun

2 2

Re: [Haskell-cafe] Wow Monads!
by David McClain 19 Apr '17

19 Apr '17

Your’e welcome… > On Apr 18, 2017, at 10:20, Bryan Richter <b(a)chreekat.net> wrote: > > On Tue, Apr 18, 2017 at 09:57:10AM -0700, David McClain wrote: >> <...> > > These posts of yours have been incredibly interesting to me, and I just > wanted to thank you for sharing them! I think my point about ecosystem programming is really about the importance of immediate feedback when crafting software. You need a powerful language so that you don’t get torpedoed with your fresh ideas with lots of mandatory scaffolding. In C-like languages the goal becomes one of writing a correct line of code. The strongly typed languages, of the FPL variety, don’t force that upon you. But you do get sidetracked by the challenge of getting that last bit of code to type check successfully. And if you aren’t already in an ecosystem with the language, even more distracted by the demands of the edit / compile cycle. Any distractions from your idea means that, if you happened to have chosen the wrong approach, you aren’t thinking properly about that aspect because the distractions have set up a nearer term goal for you to reach. We become like hamsters on a wheel, and we feel good after doing battle successfully. But the problem is, after all that, did it work the way you hoped? And without immediate feedback, even if you have some distractions that you must put up with, you are using an extended tape measure to flip the light switch on the opposite wall. I think Haskell does offer some ecosystems. I have one that I installed on my Mac a couple months ago called “Haskell for Mac” by Chakravarty. It seems a pretty nifty little environment, but I have only been in there for about an hour or two. Part of my own push for polygot creds. Another one that looks possibly interesting is Shen, formerly Qi. I did a fair amount with the old Qi language, even adding / correcting the compiler system to fit my own needs. Mastering the logic system is another challenge ahead of me. I was impressed at the implementation, and the equational reasoning, which I first saw back in the 1990’s with the publication of the SML Language. But right off the bat, Haskell will present the bigger challenge to me. There is a huge scaffold of type class hierarchy that comes in the base environment. Reminds me a bit of trying to learn the old MSVC system from yore… - DM

1 0

containers: Efficiently concatenating nested maps (or should I look at another data structure)
by Oliver Charles 18 Apr '17

18 Apr '17

Hi all, First, a little context. I'm currently working on [1] a little OpenGL project - a Quake 3 map viewer in Haskell. For the most part, things are working out great, but the way I construct the scene is costing me a lot of alloction, and I wonder if I can do better. The OpenGL system is essentially a giant state machine. Whenever you issue a draw call ("draw these triangles"), OpenGL will do different things depending on what the state is. For example, if you have a texture bound, then the triangle will be textured, and if you have blending enabled, then the triangle might be blended into whatever was drawn previously. While this can be tricky to manage, Haskell does a good job of giving us tools to model state. The real spanner is that state transitions are not free. In the above example, the state transitions associated with binding a texture or enabling blending both cost time - and this time is variable depending on the state change. In this case, setting the currently bound texture is a very expensive operation, whereas setting the blending mode is less costly. For this reason, it's common in graphics programming to want to sort draw calls to minimise state changes. For example, we might draw all triangles with texture 1, then all triangles with texture 2 - rather than interleaving those draw calls. To model this in Haskell, I'm using a tree-like structure to group and express each state change [2]. To give you an example of what this looks like, I have: class RenderNode a m where draw :: a -> m () instance RenderNode (IO ()) IO where draw = id newtype BindTexture a = BindTexture (MonoidalIntMap a) [3] deriving (Functor, Monoid) instance (MonadIO m, RenderNode a m) => RenderNode (BindTexture a) m where draw (BindTexture t) = IM.foldrWithKey (\texture0 m next -> do glActiveTexture GL_TEXTURE0 glBindTexture GL_TEXTURE_2D (fromIntegral texture0) draw m next) (return ()) (getMonoidalIntMap t) newtype BlendMode a = BlendMode (MonoidalMap (GLuint, GLuint) a) [3] deriving (Functor, Monoid) blendMode :: (GLuint, GLuint) -> a -> BlendMode a blendMode srcDst = BlendMode . MonoidalMap . Map.singleton srcDst instance (MonadIO m, RenderNode a m) => RenderNode (BlendMode a) m where draw (BlendMode m) = Map.foldrWithKey (\(srcBlend, destBlend) child next -> do glBlendFunc srcBlend destBlend draw child next) (return ()) (getMonoidalMap m) I can then stack these nodes together to form a "render graph": newtype RenderGraph = RenderGraph (BindTexture (BlendMode (IO ()))) deriving (Monoid) The IO action at the leaf corresponds to a draw call to draw some triangles. Now that I've explained the basics of my rendering plan, I just need to tell you a little bit about Quake 3 maps. A Quake 3 map is essentially a big soup of "faces", where each face is a collection of triangles (that can be drawn in one call) and a set of associated state. Furthermore, each face is assigned a "cluster" (an Int), and we have a function that given a cluster gives us back a list of other clusters that we can "see" - this is visibility determination, or occlusion culling. I am hence modelling the map as an IntMap RenderGraph - each cluster maps to a RenderGraph of how to draw all the faces in that cluster, organised to minimise draw calls. Then, given some sort of visibility check, when I render I filter this IntMap to only the clusters that can be seen, and combine all the render graphs: IntMap.foldlWithKey' (\scene clusterNumber clusterFaces -> scene <> clusterFaces) mempty clusters In reality, this results in combining a few hundred-thousad very deeply nested structures, and naturally that's resulting in a fair bit of allocation pressure. I need to do this almost every frame, because as the camera moves, we might be able to see different clusters, so I don't think there's really much that I can cache. My actual final RenderGraph is Sort |> Cull |> MultiplePasses |> BindTexture |> SetUniform Bool |> SetDynamicUniform (M33 Float) |> AlphaFunc |> BlendMode |> DepthFunc where (|>) is Functor composition, and each of those functors is either a Map or IntMap. It seems to deteriorate to pairwise `mappend`, as you can see from the definition of mappend for MonoidalMap or MonoidalIntMap in [3]. Can anyone think of any obvious ways to rewrite this to have less allocation pressure? I'm of course open to other ways to batch operations, but there is something I find quite beautiful about shoving everything into Maps and mappending them. In the C world, the approach is usually to combine all the states into a single bitmask, and then sort that. That same approach might be possible here, but I'd like to keep the pick-and-choose compositional nature that I've got above. Thanks for reading this far, I hope my post has made sense. If you need clarification on anything, the source is below, and don't hesitate to ask me any questions! -- ocharles [1]: http://github.com/ocharles/hs-quake-3 [2]: https://github.com/ocharles/hs-quake-3/blob/master/RenderGraph.hs [3]: newtype MonoidalMap k a = MonoidalMap { getMonoidalMap :: Map k a } instance Functor (MonoidalMap k) where fmap f (MonoidalMap a) = MonoidalMap (fmap f a) instance (Monoid a, Ord k) => Monoid (MonoidalMap k a) where mempty = MonoidalMap Map.empty mappend (MonoidalMap a) (MonoidalMap b) = MonoidalMap (Map.unionWith mappend a b) mconcat = coerce . Map.unionsWith mappend . (coerce :: [MonoidalMap k a] -> [Map k a]) newtype MonoidalIntMap a = MonoidalIntMap { getMonoidalIntMap :: IntMap a } deriving (Functor) instance Monoid a => Monoid (MonoidalIntMap a) where mempty = MonoidalIntMap IM.empty mappend (MonoidalIntMap a) (MonoidalIntMap b) = MonoidalIntMap (IM.unionWith mappend a b) mconcat = coerce . IM.unionsWith mappend . (coerce :: [MonoidalIntMap a] -> [IntMap a])

1 0

VSTTE 2017 - Second Call for Papers
by Andrei Paskevich 18 Apr '17

18 Apr '17

9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE) https://vstte17.lri.fr July 22-23, 2017, Heidelberg, Germany Co-located with the 29th International Conference on Computer-Aided Verification, CAV 2017 Important Dates * Abstract submission: Mon, Apr 24, 2017 * Full paper submission: Mon, May 1, 2017 * Notification: Mon, Jun 5, 2017 * VSTTE: Sat-Sun, Jul 22-23, 2017 * Camera-ready: Mon, Aug 21, 2017 Overview The goal of the VSTTE conference series is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. We welcome submissions describing significant advances in the production of verified software, i.e., software that has been proved to meet its functional specifications. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. We are especially interested in submissions describing large-scale verification efforts that involve collaboration, theory unification, tool integration, and formalized domain knowledge. We also welcome papers describing novel experiments and case studies evaluating verification techniques and technologies. Topics of interest for VSTTE include education, requirements modeling, specification languages, specification/verification/certification case studies, formal calculi, software design methods, automatic code generation, refinement methodologies, compositional analysis, verification tools (e.g., static analysis, dynamic analysis, model checking, theorem proving, satisfiability), tool integration, benchmarks, challenge problems, and integrated verification environments. Paper Submissions We accept both long (limited to 16 pages) and short (limited to 10 pages) paper submissions. Short submissions also cover Verification Pearls describing an elegant proof or proof technique. Submitted research papers and system descriptions must be original and not submitted for publication elsewhere. Each submission will be evaluated by at least three members of the Program Committee. We expect that one author of every accepted paper will present their work at the conference. Paper submissions must be written in English using the LNCS LaTeX format (http://www.springer.com/gp/computer-science/lncs/conference-proceedings-gui…) and must include a cogent and self-contained description of the ideas, methods, results, and comparison to existing work. Papers will be submitted via EasyChair at the VSTTE 2017 conference page (https://www.easychair.org/conferences/?conf=vstte2017) The post-conference proceedings of VSTTE 2017 will be published in the LNCS series. Authors of accepted papers will be requested to sign the copyright transfer form. A selection of best papers will be invited for publication in the Journal of Automated Reasoning. Invited Speakers * Christoph Weidenbach (Max Planck Institute for Informatics, Germany) * Santiago Zanella-Beguelin (Microsoft Research, UK) Program Committee * June Andronick (University of New South Wales, Australia) * Christel Baier (TU Dresden, Germany) * Sandrine Blazy (Université de Rennes 1, France) * Arthur Charguéraud (Inria, France) * Ernie Cohen (Amazon Web Services, USA) * Rayna Dimitrova (MPI-SWS, Germany) * Carlo A. Furia (Chalmers University of Technology, Sweden) * Arie Gurfinkel (University of Waterloo, Canada) * Hossein Hojjat (Rochester Institute of Technology, USA) * Marieke Huisman (University of Twente, Netherlands) * Bart Jacobs (KU Leuven, Belgium) * Rajeev Joshi (NASA Jet Propulsion Laboratory, USA) * Zachary Kincaid (Princeton University, USA) * Akash Lal (Microsoft Research, India) * Shuvendu Lahiri (Microsoft Research, USA) * Francesco Logozzo (Facebook, USA) * Peter Müller (ETH Zürich, Switzerland) * Jorge A. Navas (SRI International, USA) * Scott Owens (University of Kent, UK) * Andrei Paskevich (Université Paris-Sud, France), co-chair * Gerhard Schellhorn (Universität Augsburg, Germany) * Peter Schrammel (University of Sussex, UK) * Natarajan Shankar (SRI International, USA) * Mihaela Sighireanu (Université Paris-Diderot, France) * Julien Signoles (CEA LIST, France) * Michael Tautschnig (Queen Mary University of London, UK) * Tachio Terauchi (JAIST, Japan) * Oksana Tkachuk (NASA Ames Research Center, USA) * Mattias Ulbrich (Karlsruhe Institute of Technology, Germany) * Thomas Wies (New York University, USA), co-chair

1 0

Req. for co-maintaining hs-libhdf5 and bindings-hdf5
by Marco Zocca 18 Apr '17

18 Apr '17

Dear all, I would like to help taking care of two libraries for HDF5. The author, James Cook (mokus0 on GitHub, CC'd here), didn't reply to a private email I sent about this on April 12. I hope he's doing well, by the way. HDF5 is a popular format for scientific datasets, and it would be a pity to see the Haskell bindings bitrot. I have previous experience building Haskell C bindings with HSC, c2hs and inline-c, and as co-maintainer I would, as first steps, add memory brackets and user-facing `exceptions`, enable continuous integration (Travis) and "stack-ify" the libraries. Hoping to hear soon from James and/or the Hackage trustees; All the best, Marco (ocramz)

1 0

Call for participation: PLDI 2017 and co-located events
by Tobias Grosser 18 Apr '17

18 Apr '17

Call for participation: PLDI 2017 and co-located events PLDI is the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance. The co-located conferences take place in Barcelona, June 18-23, 2017. This year, PLDI is co-located with ECOOP, LCTES, DEBS, ISMM, Curry On and others. The conferences will take place at the Universitat Polytècnica de Catalunya in Barcelona, Spain. http://conf.researchr.org/home/pldi-2017 Registration is now open, please visit: https://regmaster4.com/2017conf/BARC17/register.php to register. The early registration rate ends on May 26th. The tentative program is available at: http://pldi17.sigplan.org/program/program-pldi-2017 PLDI will also hold an ACM Student Research Competition: http://pldi17.sigplan.org/track/pldi-2017-student-research-competition Co-located events: + ECOOP: European Conference on Object-Oriented Programming + DEBS: annual conference on Distributed Event-Based Systems + Curry On: conference on programming languages and emerging challenges in industry. + ISMM: International Symposium on Memory Management + LCTES: Languages, Compilers, and Tools for Embedded Systems Co-located workshops include: + ARRAY: Workshop on Libraries, Languages and Compilers for Array Programming + DSW: Deep Specifications in the Wild + FMS: Formal Methods for Security + IC: Workshop on Incremental Computing + MAPL: Machine Learning and Programming Languages + PLMW: Programming Languages Mentoring Workshop + SOAP: International Workshop on the State Of the Art in Java Program Analysis + WCIRE: Workshop for Compiler Infrastructure for Research and Education Additionally, there will be eight co-located tutorials: + Bug detection in JavaScript web apps using the SAFE framework + Building your own modular static analyzer with Facebook Infer + Engineering Static Analyzers with Soufflé + Graal: High Performance Compilation for Managed Languages + P4: Programming the Network Data Plane + Polyhedral Compilation + Refinement Types for Program Verification and Synthesis + Scala, LMS and Delite for High-Performance DSLs and Program Generators + WALA Hack-A-Thon + Writing Verified Programs in CakeML See the web site for a schedule and further details and links. For further updates, follow PLDI on the social media: Facebook: https://www.facebook.com/PLDIConf Twitter: https://twitter.com/PLDI Albert Cohen, PLDI 2017 General Chair Tobias Grosser, PLDI 2017 Publicity Chair

1 0