- Haskell-Cafe - Haskell.org

WST 2018 - Call for Participation (July 18-19, 2018)
by Salvador Lucas 04 Jun '18

04 Jun '18

========================================================================== WST 2018 - Call for Participation 16th International Workshop on Termination part of FLoC 2018 July 18-19, 2018, Oxford, United Kingdom http://wst2018.webs.upv.es/ ========================================================================== REGISTRATION (June 6th is the last day for early registration!) http://www.floc2018.org/register/ INVITED SPEAKERS: James Worrell - University of Oxford "Termination Checking and Invariant Synthesis for Affine Programs" Akihisa Yamada - NII Japan "Towards a Unified Method for Termination" PROGRAMME (see also the list of accepted papers attached below): https://easychair.org/smart-program/FLoC2018/WST-program.html TERMINATION AND COMPLEXITY COMPETITION: In 2018, the Termination and Complexity Competition (TERCOMP) will run in parallel with FLoC 2018 as part of the FLoC Olympic Games. The results of the competition will be presented and discussed during a special session at WST 2018. ACCEPTED PAPERS: Eric Hehner. Objective and Subjective Specifications. Guillaume Genestier and Frédéric Blanqui. Termination of Lambda-Pi modulo rewriting using the size-change principle Jera Hensel, Florian Frohn and Jürgen Giesl. Complexity Analysis for Bitvector Programs Alfons Geser, Dieter Hofbauer and Johannes Waldmann. Comparing on Strings: Semantic Kachinuki Order Nachum Dershowitz and Jean-Pierre Jouannaud. GPO: A Path Ordering for Graphs Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada. A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving Jonas Schöpf and Christian Sternagel. TTT2 with Termination Templates for Teaching Cristina David, Daniel Kroening and Peter Schrammel. Procedure-Modular Termination Analysis Salvador Lucas. Well-founded models in proofs of termination Aalok Thakkar, Balaji Krishnamurthy and Piyush Gupta. Verification of Rewriting-based Query Optimizers Jesús J. Doménech, Samir Genaim and John P. Gallagher. Control-Flow Refinement via Partial Evaluation Alicia Merayo Corcoba and Samir Genaim. Inference of Linear Upper-Bounds on the Expected Cost by Solving Cost Relations Dieter Hofbauer. Embracing Infinity - Termination of String Rewriting by Almost Linear Weight Functions Carsten Fuhs and Cynthia Kop. Improving Static Dependency Pairs for Higher-Order Rewriting

1 0

A law for MonadReader
by Li-yao Xia 03 Jun '18

03 Jun '18

Hello Café, While trying to document laws for mtl classes (https://github.com/haskell/mtl/issues/5) I have been puzzling over the subtle logical relationships between a few variants. Consider the following four possible laws for MonadReader's ask: (1) (ask >> ask) = ask (2) (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2)) = (ask >>= \r -> return (r, r)) (3) (ask >> return ()) = return () Let reader :: MonadReader r m => (r -> a) -> m a reader f = fmap f ask (4) reader is a monad homomorphism from ((->) r) to m, i.e.: reader (\_ -> a) = return a (reader m >>= \x -> reader (k x)) = reader (m >>= k) Question: which ones imply which ones? Note that (1) and (2) do not imply (3) or (4). Intuitively, (1) and (2) say that ask is idempotent ("asking twice is the same as asking once"), but (3) and (4) imply the stronger property of nullipotence ("ask has no side effects"). --- Any help with the following conjectures is welcome (we're assuming the monad laws hold in the first place): A. (1) and (2) are equivalent. I can prove that (2) implies (1). However the converse eludes me. B. (3) and (4) are equivalent. Again, I can prove that (4) implies (3), but I had no success with the converse. C. ((3) or (4)) implies ((1) and (2)) ((3) implies (1)), and ((4) implies ((1) and (2))) are straightforward, but without the above equivalence, the missing bit is ((3) implies (2)) It seems that parametricity plays an important role in the conjectured implications. I didn't manage to apply free theorems to this problem, but perhaps you will have better luck. Regards, Li-yao

4 6

(names for) invariants for Eq and Ord?
by Johannes Waldmann 02 Jun '18

02 Jun '18

Dear Cafe, I am somewhat surprised that the Haskell Standard (*) https://www.haskell.org/onlinereport/haskell2010/haskellch6.html#x13-127000… does not contain any notation for (intended) properties of Eq and Ord instances, and their relation. For Java (standard library), the API spec uses wording like "consistent with equals" https://docs.oracle.com/javase/10/docs/api/java/lang/Comparable.html I am well aware that semantics (transitivity, etc.) cannot be enforced statically, in either language. But both standards still speak of "total order". Do we (Haskell) need something similar to "consistent with equals"? It depends. E.g., looking at a (random) source in containers (Data.Map.Internal), it seems that it will always use the result of compare, never of (==), on keys. That's not obvious from the docs. I just checked -- I can make a type where (==) = undefined, but write a proper Ord instance, and use it as key type. I am asking this because I will be teaching type classes, with Eq and Ord as examples. I detected the funny situation that the Java specification looks "more mathematical" than the corresponding Haskell one. What will the students think ... - J.W. (*) The Haskell standard is what you find when you scroll down, down, down to the very bottom of https://www.haskell.org/documentation . So, probably not that important...

6 5

No Enum for (,), no Enum or Bounded for Either
by Tom Ellis 02 Jun '18

02 Jun '18

I'm a bit surprised that whilst `Either` and `(,)` have instances for `Ord` * `(,)` has no instance for `Enum` * `Either` has no instance for `Enum` or `Bounded` Is there a particular reason for that? It might be tricky to implement toEnum :: Int -> a fromEnum :: a -> Int but in the presence of `Bounded` that should be possible. Tom

8 15

[ANN] karya, music editor
by Evan Laforge 01 Jun '18

01 Jun '18

This is an announcement for Karya, which is a music editor written in Haskell. There are more details at: http://ofb.net/~elaforge/karya/doc/overview.md.html or if you just want to listen to music: http://ofb.net/~elaforge/karya/doc/examples.md.html Source is at: https://github.com/elaforge/karya Even if you're not interested in the music part, it's an example of a haskell program with a GUI, REPL based interface, tests, profiling, and a shake-based build system, although probably idiosyncratic implementations of all of the above. It should run on OS X (well tested) and X11 (poorly tested). If you are interested in the music part, this is basically in the "score writing" genre of software, in that it's suitable for writing a score in a textual non-realtime way. But though non-realtime, it's still interactive, so you can hear what you just wrote. And though textual and language-oriented, it's also semi-graphical, so it's closer to the sequencer / music editor type application than a music-oriented DSL like Haskore. It's hard to describe because as far as I know there's nothing else similar. If you have used a DAW but wanted to define higher level abstractions, or if you used Haskore (or similar) but found it difficult to write music purely textually, you might be interested in this. Or if you want to use your own tunings or scales, or do expressive control of pitch and dynamics. You'll need an external MIDI synthesizer though. There is a direct synthesis backend, but it's not practically usable yet. It's somewhat mature, in that I've been using for all my own music for the last 5 years or so, but of course also has many areas of active development, from graphics, to language design and interpretation, to music notation design, to audio synthesis and numerics. There is some documentation, but it's undoubtedly sparse since I'm the only user. Ask if you have questions! Details will be materialized on demand. Some things not mentioned on the "official" page since they're in progress: - A DSL to notate solkattu, which is Carnatic percussion syllables, and is a sort of instrument-independent notation for rhythmic structures, along with rules for realizing on various instruments. This is closer to a traditional music DSL like Haskore, but winds up different since it's rhythmically oriented. There's a small library of compositions. - An offline synthesis framework, including a sampler and FAUST-based synthesizer, built on a streaming audio library. I'm currently working on implementing off-line incremental audio rendering, which as far as I know is unique.

3 4

PLMW@ICFP: CALL FOR SCHOLARSHIP APPLICATIONS and PARTICIPATION (deadline June 30!)
by Niki Vazou 31 May '18

31 May '18

PLMW@ICFP: CALL FOR SCHOLARSHIP APPLICATIONS and PARTICIPATION (deadline June 30!) ACM SIGPLAN Programming Languages Mentoring Workshop Co-located with ICFP'18 PLMW web page: https://icfp18.sigplan.org/track/PLMW-ICFP-2018 The purpose of the programming languages mentoring workshop (PLMW) is to encourage senior undergraduate and early career (first or second year) to pursue careers in programming language research. We are specifically interested in attracting groups who have traditionally not had the opportunity to participate in research in functional programming. This workshop will be a combination of learning about the work being done in several areas of programming language research and mentoring with respect to helping students prepare for graduate school and the rest of their career. We will bring together leaders in programming language research from academia and industry to give talks on the kind of research typically performed after obtaining a Ph.D. The workshop will engage students, specifically interested in programming language research, in a process of imagining how they might contribute to the world. We especially encourage women and underrepresented minority students to attend PLMW. This workshop is part of the activities surrounding ICFP, the International Conference on Functional Programming, and takes place the day before the main conference. One goal of the workshop is to make ICFP conference more accessible to newcomers. We hope that participants will stay through the entire conference. ## Travel Scholarship Applications (Due 30 June) Please fill out this form https://goo.gl/forms/7o4nENLxzAo2zwYy1. by 30 June to apply for travel funding. See the PLMW web page for additional details. The workshop registration is open to all. Students with alternative sources of funding are welcome. Best, Niki Vazou

1 0

ANN: fast-arithmetic 0.6.0.7
by Vanessa McHale 31 May '18

31 May '18

Hi all, I have just published a new version of fast-arithmetic <https://hackage.haskell.org/package/fast-arithmetic>. It provides fast primitives for number theory and combinatorics on Linux and Mac. The latest release has few dependencies and thus builds should be quite robust.

1 0

Re: [Haskell-cafe] ANN: primitive 0.6.4.0
by Dr.Koster 31 May '18

31 May '18

I have make some comments on reddit, but still I want to record them here: After reading the new code, I got a feeling that there're some API lacking considerations. Here is some of my personal concerns: The generalized MVar is basically useless because ST is meant to seal its state token, you won't want to add a forkST. You can argue that the atomic operations on MutVar is already added, but still I want to justify its usefulness. There're too much combinators added to PrimArray, is there a plan to port these to other arrays? If we ever provide toList operations, then I would really want it to be a good producer in base's fold-build fusion' view, it's robust and easy to implement, and folding is basically the same speed with List.fold and toList. Anyway it seems I missed the bike shedding, but still I want to thank for all the efforts, I'll try to follow new GitHub workflow more closely. Cheers Winter 发自我的iPhone ------------------ Original ------------------ From: Carter Schonwald <carter.schonwald(a)gmail.com> Date: Thu,May 31,2018 2:55 AM To: haskell-cafe <haskell-cafe(a)haskell.org>, Haskell Libraries <libraries(a)haskell.org> Subject: Re: [Haskell-cafe] ANN: primitive 0.6.4.0 This is a pretty exciting (albeit minor version) I'd like to especially thank David Feuer (treeowl ) and Andrew Martin (andrewthad) for their contributions the change log has a huge number of bug fixes relative to 0.6.2-3 also we added some new modules of features PrimArray --- unboxed nonsliceable vectors MVar -- Mvars that run in any PrimMonad augmented the Data.Primitive exports for increased consistency (the new .Ptr and .Mvar modules aren't exported in this minor version so users can easily migrate) Changes in version 0.6.4.0 Introduce Data.Primitive.PrimArray, which offers types and function for dealing with a ByteArray tagged with a phantom type variable for tracking the element type. Implement isByteArrayPinned and isMutableByteArrayPinned. Add Eq1, Ord1, Show1, and Read1 instances for Array and SmallArray. Improve the test suite. This includes having property tests for typeclasses from base such as Eq, Ord, Functor, Applicative, Monad, IsList, Monoid, Foldable, and Traversable. Fix the broken IsList instance for ByteArray. The old definition would allocate a byte array of the correct size and then leave the memory unitialized instead of writing the list elements to it. Fix the broken Functor instance for Array. The old definition would allocate an array of the correct size with thunks for erroring installed at every index. It failed to replace these thunks with the result of the function applied to the elements of the argument array. Fix the broken Applicative instances of Array and SmallArray. The old implementation of <*> for Arrayfailed to initialize some elements but correctly initialized others in the resulting Array. It is unclear what the old behavior of <*> was for SmallArray, but it was incorrect. Fix the broken Monad instances for Array and SmallArray. Fix the implementation of foldl1 in the Foldable instances for Array and SmallArray. In both cases, the old implementation simply returned the first element of the array and made no use of the other elements in the array. Fix the implementation of mconcat in the Monoid instance for SmallArray. Implement Data.Primitive.Ptr, implementations of Ptr functions that require a Prim constraint instead of a Storable constraint. Add PrimUnlifted instances for TVar and MVar. Use compareByteArrays# for the Eq and Ord instances of ByteArray when building with GHC 8.4 and newer. Add Prim instances for lots of types in Foreign.C.Types and System.Posix.Types. Reexport Data.Primitive.SmallArray and Data.Primitive.UnliftedArray from Data.Primitive. Add fold functions and map function to Data.Primitive.UnliftedArray. Add typeclass instances for IsList, Ord, and Show. Add defaultSetByteArray# and defaultSetOffAddr# to Data.Primitive.Types.

3 2

Config Files and monoids
by Olaf Klinke 30 May '18

30 May '18

Dear cafe, a recent post here [1] mentioned that configurations, such as the ones read from a config file, can be given Monoid instances, where mempty is the empty or default configuration and mappend merges two partial configurations, producing a more complete one. The vgrep package explicitly does this, for instance. Although the ConfigParser type from the ConfigFile package has a binary 'merge' operation, it does define neither a Monoid not a Semigroup instance. I'm struggling to make the concept of monoidal configuration work when there is no sensible default configuration. Suppose my configuration type is data Config = Config {foo :: Bool, bar :: Int} with no reasonable default, e.g. emptyConfig = Config { foo = error "you did not specify option foo", bar = error "you did not specify option bar" } Some configuration monoids seem to have the second operand override the first, or the other way around. However, I wish that when cfg1 = emptyConfig {foo = True} cfg2 = emptyConfig {bar = 4} then cfg1 <> cfg2 == Config {foo = True, bar = 4}. So it seems that for mappend to work as intended one needs a terminating function that tells me if a record field is already defined, e.g. when all fields are Maybes. Vgrep.Environment.Config.Monoid does it this way. My solution so far was to resort to the monoid of endofunctions (as the getflag package does), that is, define cfg1, cfg2 :: Config -> Config cfg1 = \cfg -> cfg {foo = True} cfg2 = \cfg -> cfg {bar = 4} And then build (cfg1.cfg2) emptyConfig. (Alternatively, one might structure these as lenses instead of endofunctions, see e.g. Data.Monoid.Endo.Fold in the endo package.) Thus I arrived at class Config cfg where emptyConfig :: cfg -- may contain some defaults configOptions :: [Parser (cfg -> cfg)] Do you think every other concept of configuration parsing can be cast into this typeclass? -- Olaf [1] https://mail.haskell.org/pipermail/haskell-cafe/2018-May/129063.html

5 5

Re: [Haskell-cafe] (names for) invariants for Eq and Ord?
by Olaf Klinke 30 May '18

30 May '18

Prelude> import qualified Data.Map as M Prelude M> let k = 0/0 in let v = 0 in M.lookup k (M.insert k v M.empty) == Just v False This one is not surprising because the presence of 0/0 destroys the total order of Double, so strictly speaking this should not have an Ord instance. Olaf

1 0