May 2016 - Haskell-Cafe

JSON parser that returns the rest of the string that was not used
by Ryan Newton 30 May '16

30 May '16

As someone who spent many years putting data in S-expression format, it seems natural to me to write multiple S-expressions (or JSON objects) to a file, and expect a reader to be able to read them back one at a time. This seems comparatively uncommon in the JSON world. Accordingly, it looks like the most popular JSON parsing lib, Aeson, doesn't directly provide this functionality. Functions like decode just return a "Maybe a", not the left-over input, meaning that you would need to somehow split up your multi-object file before attempting to parse, which is annoying and error prone. It looks like maybe you can get Aeson to do what I want by dropping down to the attoparsec layer and messing with IResult. But is there a better way to do this? Would this be a good convenience routine to add to aeson in a PR? I.e. would anyone else use this? Thanks, -Ryan

7 10

Quantum Programming EDSLs other than Quipper
by Nicola Gigante 30 May '16

30 May '16

Hi all, Quipper [1] is a well-known library that provides an EDSL for writing and simulating quantum algorithms in Haskell. I was wondering if there was any other attempt to design an EDSL in Haskell to express quantum algorithms. In particular, Quipper is not able to statically ensure that the algorithm written is physically meaningful, as one could violate the "non-cloning property", for example (a qubit cannot be copied, for those who do not speak quantumly). Violations like this are detected at runtime when simulating the algorithm or when producing the corresponding circuit as output. Authors of Quipper already said that some of those properties could be possible to check “if Haskell had linear types”. The point is that Haskell's support for dependently typed programming has grown quite a lot in the last years, and I think that, at least theoretically, something better can now be achieved. So do anyone know any more recent attempt to express quantum computations in an Haskell EDSL that leverages cutting-edge type-level features to statically check for physically meaningful programs? Greetings, Nicola [1]: http://www.mathstat.dal.ca/~selinger/quipper/

2 4

configurable mapping between data declarations and given XML schema?
by Johannes Waldmann 30 May '16

30 May '16

Dear Cafe, I have a legacy XML schema, and some Haskell data declarations. I want to map bidirectionally between XML documents and data. I absolutely cannot change the schema. I could change the data declarations, but it would not help much, since I don't think there is any form of declaring data that would allow me to derive the transformations generically. So, I have a mess of ad-hoc transformations. What could be done about this? I think I need "generic with customization". More detail: https://github.com/jwaldmann/haskell-tpdb/issues/16 Comments appreciated. - J.W.

3 2

Mobile Development
by Justin Wood 29 May '16

29 May '16

I'm wondering if anyone has any experience they can share, know of any blog posts or anything else documenting the use of Haskell when developing a mobile application. Ideally, I would like something along the lines of having a native UI, a language bridge, and use Haskell for the core logic. My main focus would be getting this to work on Android and iOS. If this would also work on Blackberry and Windows Phone it would be a plus. I have successfully done this using C++ in place of Haskell in the past, but would really be interested in getting something working using Haskell. Thanks, Justin

4 3

Testing for different dependency versions?
by Christopher Howard 29 May '16

29 May '16

Hi, I was wondering: what is the most practical way to go about testing or otherwise determining if your packaged library works with other dependency versions? E.g., cabal init specified base 4.6 because that is what happens to be installed on my Debian Jessie system, but that wouldn't even build on hackage. -- http://justonemoremathproblem.com To protect my privacy, please use PGP encryption. It's free and easy to use! My public key ID is 0x340EA95A (pgp.mit.edu)

2 1

Re: [Haskell-cafe] Testing for different dependency versions?
by Simon Jakobi 29 May '16

29 May '16

(I'm sending this again because I had subscribed to the mailing list with a different email address) Hi! I'm not sure if there's a better tool out there but I think stack (http://haskellstack.org/) is pretty convenient for testing a package with different versions of base and other packages on the same system. To test your package with base-4.7 you'd simply run stack test --resolver ghc-7.8 --install-ghc To test your package with base-4.8.2.0 and pkg-x-1.2.3 you'd save the following in a stack.yaml in the same directory as your cabal file: resolver: ghc-7.10.3 extra-deps: - pkg-x-1.2.3 Then run stack solver --update-config to add the remaining dependencies and stack test to build the package and run the tests. If you have your package on Github you can also use Travis CI to test your package with different configurations: http://docs.haskellstack.org/en/stable/travis_ci/ Hope that helps! Simon

1 1

Higher order type functions
by Matt 28 May '16

28 May '16

Hi folks! I'm playing with GHC 8 and have the following type family definend: type family InsertSorted (gt :: k -> k -> Bool) (a :: k) (xs :: [k]) :: [k] where InsertSorted f a '[] = '[a] InsertSorted f a (x ': xs) = If (f a x) (x ': InsertSorted f a xs) (a ': x ': xs) With appropriate type functions, I can evaluate this in GHCi with `:kind!` and it does what I want: λ> :kind! InsertSorted GreaterThan One '[Two, Four] InsertSorted GreaterThan One '[Two, Four] :: [Face] = '['One, 'Two, 'Four] λ> :kind! InsertSorted GreaterThan Queen '[Two, Four] InsertSorted GreaterThan Queen '[Two, Four] :: [Face] = '['Two, 'Four, 'Queen] However, I get an error if I try to use this in a type signature. This code: data Deck (b :: [k]) where Empty :: Deck '[] (:::) :: CardT s f -> Deck xs -> Deck (InsertSorted GreaterThan '(s, f) xs) gives me this error: • The type family ‘GreaterThan’ should have 2 arguments, but has been given none • In the definition of data constructor ‘:::’ In the data type declaration for ‘Deck’ What's the best way to use higher order type families? Thanks! Matt Parsons Here's the definitions I'm using for the above code: data Face = One | Two | Three | Four | Five | Six | Seven | Eight | Nine | Jack | Queen | King deriving (Eq, Ord, Bounded, Enum) type family FaceOrd (a :: Face) (b :: Face) :: Ordering where FaceOrd a a = 'EQ FaceOrd a 'One = 'GT FaceOrd 'One a = 'LT FaceOrd a b = FaceOrd (PredFace a) (PredFace b) type family FaceGT (a :: Face) (b :: Face) :: Bool where FaceGT a b = CompK a b == GT class GtK (a :: k) where type GreaterThan (a :: k) (b :: k) :: Bool instance GtK (a :: Face) where type GreaterThan a b = CompK a b == GT

3 3

read "2" in a "void" context?
by Erik Rantapaa 28 May '16

28 May '16

Hi fellow Haskellers! If I bring up ghci and evaluate `read 2` I get the error "Prelude.read: no parse" GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help Prelude> read "2" *** Exception: Prelude.read: no parse Exactly how is this message coming about? I understand that `read` needs a return type in order to determine which type class instance to run. So, in this case, which type is `read` being asked to return? Thanks, Erik

4 4

Reminder: Functional High-Performance Computing 2016
by David Duke 28 May '16

28 May '16

Dear colleagues, A reminder of the approaching paper deadline (10th June) for FHPC 2016 ... ====================================================================== CALL FOR PAPERS FHPC 2016 The 5th ACM SIGPLAN Workshop on Functional High-Performance Computing Nara, Japan September 22, 2016 https://sites.google.com/site/fhpcworkshops/ Co-located with the International Conference on Functional Programming (ICFP 2016) Submission Deadline: Friday, 10 June, 2016 (anywhere on earth) ====================================================================== The FHPC workshop aims at bringing together researchers exploring uses of functional (or more generally, declarative or high-level) programming technology in application domains where high performance is essential. The aim of the meeting is to enable sharing of results, experiences, and novel ideas about how high-level, declarative specifications of computationally challenging problems can serve as maintainable and portable code that approaches (or even exceeds) the performance of machine-oriented imperative implementations. All aspects of performance critical programming and parallel programming are in-scope for the workshop, irrespective of hardware target. This includes both traditional large-scale scientific computing (HPC), as well as work targeting single node systems with SMPs, GPUs, FPGAs, or embedded processors. It is becoming apparent that radically new and well founded methodologies for programming such systems are required to address their inherent complexity and to reconcile execution performance with programming productivity. Experience reports are also welcome. Proceedings: ============ FHPC 2016 seeks to encourage a range of submissions, focussing on work in progress and facilitating early exchange of ideas and open discussion on innovative and/or emerging results. To this end submissions should take the form of short (maximum 6 page) papers. Accepted papers will be published by the ACM and will appear in the ACM Digital Library. * Submissions due: Friday, 10 June, 2016 (anywhere on earth) * Author notification: Friday, 8 July, 2016 * Final copy due: Sunday, 31 July, 2016 Submitted papers must be in portable document format (PDF), formatted according to the ACM SIGPLAN style guidelines (2 column, 9pt format). See http://www.sigplan.org/authorInformation.htm for more information and style files. Papers should be no longer than 6 pages. Contributions to FHPC 2016 should be submitted via Easychair, at the following URL: * https://www.easychair.org/conferences/?conf=fhpc16 The FHPC workshops adhere to the ACM SIGPLAN policies regarding programme committee contributions and republication. Any paper submitted must adhere to ACM SIGPLAN's republication policy. PC member submissions are welcome, but will be reviewed to a higher standard. http://www.sigplan.org/Resources/Policies/Review http://www.sigplan.org/Resources/Policies/Republication Travel Support: =============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC programme, see its web page (http://www.sigplan.org/PAC.htm) Programme Committee: ==================== David Duke (co-chair) University of Leeds, UK Yukiyoshi Kameyama (co-chair) University of Tsukuba, Japan Baris Aktemur Özyeğin University, Turkey Marco Aldinucci University of Torino, Italy Jost Berthold Commonwealth Bank, Australia Kei Davis Los Alamos National Laboratory, USA Kento Emoto Kyushu Institute of Technology, Japan Zhenjiang Hu National Institute of Informatics, Japan Ben Lippmeier University of New South Wales, Australia Rita Loogen University of Marburg, Germany Geoffrey Mainland Drexel University, USA Mike Rainey INRIA, France Mary Sheeran Chalmers University of Technology, Sweden Satnam Singh Facebook, UK

1 0

Re: [Haskell-cafe] Fwd: representing institutions in haskell
by Till Mossakowski 28 May '16

28 May '16

Dear Rick, actually, in the Hets system [1], which is one of the largest Haskell programs, we have represented logics as institutions since 2002. Hets comprises of about 25 logics represented as institutions, including propositional logic, first-order logic, higher-oder logic, modal logic, OWL, and even some functional programming language. Hets provides parsing, static analysis, and proof management for logical theories formulated within these institutions (and also heterogeneous theories spanning several institutions). Interfaces to various theorem provers, SAT solvers and model finders are included. Hets' input language is the Distributed Ontology, Model and Specification language (DOL) [2], which has been standardized by the Object Management Group (OMG). More specifically, Hets employs a type class "Category" for representing categories, with functions for identities, domain, codomain and composition. On top of this, institutions form a multi-parameter type class "Logic", with a representation of signatures and signature morphisms as a category. The set of sentences is represented as one parameter type. This is a pragmatic decision, since in most institutions, sentences are uniform over signatures, and making this dependent on signature would be much more complicated. But many functions on sentences depend on a signature. Sentence translation along a signature morphism is represented by a function of the type class as well. Models and satisfaction are generally not represented due to their (in general) infinitary nature. But in some case, we represent models as certain theories, e.g. when processing the output of some model finder. Such models can even be translated using institution comorphisms. That said, we are interested in improving the representations of institutions in Hets, e.g. by making more using some libraries for category theory that have not been available in 2002 when we started Hets. However, I must admit that I did not understand your representation, Rick. Could you explain its general principles? What is the purpose of having "data Sign a = Sign a"? Why do conjunction and disjunction play such a role, given that there are institutions like equational logic that neither have conjunction nor disjunction? I could I execute your code, neither with ghc 7.6.3, nor ghc 8.0.2. I suggest that you choose some simple logic, like propositional logic, and represent it as an institution in Haskell with your approach. Then we will have a better basis for discussion. Best, Till [1] http://hets.eu [2] http://dol-omg.org Am 17.05.2016 um 14:55 schrieb rick: > Hello Christian: > > I thought I should send this to you separately in case you are not on > the Haskell list any more. > > You may enjoy the samples below which use some standard Haskell > libraries that may not have been available when you and Till started > work on HETS. > > -- > Rick > > -------- Forwarded Message -------- > Subject: [Haskell-cafe] representing institutions in haskell > Date: Mon, 16 May 2016 15:13:34 -0400 > From: rick <rick(a)rickmurphy.org> > To: haskell-cafe(a)haskell.org > > Has anyone here taken an interest in representing institutions [1] in > Haskell? > > Institutions originated in work on CLEAR [2] which was the first > algebraic specification language with rigorous semantics. > > Institutions take some time to explain, or unravel if you follow the > reference, but they come with a convenient slogan : "Truth is invariant > under change of notation." > > The stretch goal of institutions is transforming logics while preserving > satisfaction. > > They are conceived in terms of categorical abstractions, so it's natural > to represent them in categories. I hope some folks here find > institutions a useful domain to apply their work on categories. > > I've attached two samples in Haskell that uses some standard libraries : > Arrow, Monad, Category and Dual. > > The first sample, ri-0, outlines the essentials. The category of > signatures, constructions in the categories, signature morphisms, > sentences, models and the satisfaction condition. > > Using plain old Nat reduces the complexity of the exposition. > > I provide a constructive witness for satisfaction of the morphism from > conjunction to disjunction. > > You may recognize that I borrow some Bird/Hinze notation on Functors > like mapSign. And you find some experiments with Quickcheck and Yampa. > > Ri-0 runs from main, but just computes the witness to the satisfaction > condition. > > The second sample, ri-1, builds on ri-0. Rather than Nat, I use Either > to inject disjunction into the exposition. The exposition becomes more > complex, but the increased complexity is justified because maintaining > satisfaction under change on notation is central to institutions. > > The functions prodSum takes conjunction to disjunction and sumProd takes > disjunction to conjunction. I owe a citation to @BartoszMilewski and his > work on categories for programmers where I first saw these functions. > > The satisfaction condition and witness appear more complex in ri-1, but > its really just the substitution of the signature morphism on product > and sum rather than plain old Nat as in ri-0. > > I also plan a better write up, but before I do I expect to learn much > from an email exchange with interested folks here. > > Thanks for taking a look at this material. > > 1. https://cseweb.ucsd.edu/~goguen/pps/ins.ps > > 2. http://hopl.info/showlanguage.prx?exp=945 >

1 0