News aggregator

Set-Theoretic Types for Polymorphic Variants

Lambda the Ultimate - Thu, 06/09/2016 - 7:38am

Set-Theoretic Types for Polymorphic Variants by Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn:

Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive.

In this work, we present an alternative formalization of polymorphic variants, based on set-theoretic types and subtyping, that yields a cleaner and more streamlined system. Our formalization is more expressive than the current one (it types more programs while preserving type safety), it can internalize some meta-theoretic properties, and it removes some pathological cases of the current implementation resulting in a more intuitive and, thus, predictable type system. More generally, this work shows how to add full-fledged union types to functional languages of the ML family that usually rely on the Hindley-Milner type system. As an aside, our system also improves the theory of semantic subtyping, notably by proving completeness for the type reconstruction algorithm.

Looks like a nice result. They integrate union types and restricted intersection types for complete type inference, which prior work on CDuce could not do. The disadvantage is that it does not admit principal types, and so inference is non-deterministic (see section 5.3.2).

Categories: Offsite Discussion

ANN: Intero for Emacs

haskell-cafe - Wed, 06/08/2016 - 1:01pm
Here is a new Emacs package providing *very basic* Haskell programmer needs: - Type checking - Autocompletion - Go to definition - Type of selection - A basic REPL support It’s very simple, tries to *just work*, is based on Stack (required), the Emacs package auto-installs the correct version of its backend within your Stack working directory, supports the recently released GHC 8 all the way back to GHC 7.8.3. Having to configure anything to get basic functionality is considered a bug. The home page is here with details and demonstrations: The GitHub project where you can submit feature requests or bug reports: Thanks for reading! ​ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

Jan Stolarek: Coq’Art, CPDT and SF: a review of books on Coq proof assistant

Planet Haskell - Wed, 06/08/2016 - 11:30am

I have been pretty quiet on the blog in the past couple of months. One of the reasons for this is that I have spent most of my time learning Coq. I had my first contact with Coq well over a year ago when I started reading CPDT. Back then I only wanted to learn the basics of Coq to see how it works and what it has to offer compared to other languages with dependent types. This time I wanted to apply Coq to some ideas I had at work, so I was determined to be much more thorough in my learning. Coq is far from being a mainstream language but nevertheless it has some really good learning resources. Today I would like to present a brief overview of what I believe are the three most important books on Coq: “Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions” (which I will briefly refer to as Coq’Art) by Yves Bertot and Pierre Castéran, “Certified Programming with Dependent Types” (CPDT) by Adam Chlipala and “Software Foundations” (SF for short) by Benjamin Pierce and over a dozen over contributors. All three books significantly differ in their scope and focus. CPDT and Coq’Art are standard, printed books. CPDT is also available online for free. Software Foundations is only available as an online book. Interestingly, there is also a version of SF that seems to be in the process of being revised.

I believe Coq’Art was the first book published on Coq. There are two editions – 2004 hardcover version and a 2010 paperback version – but as far as I know there are no differences between them. Too bad the 2010 edition was not updated for the newest versions of Coq – some of the code examples don’t work in the newest compiler. Coq’Art takes a theoretical approach, ie. it teaches Coq largely by explaining how the rules of Calculus of Constructions work. There are also practical elements like case studies and exercises but they do not dominate the book. Personally I found Coq’Art to be a very hard read. Not because it dives too much in theory – it doesn’t – but because the presentation seems to be chaotic. For example, description of a single tactic can be spread throughout deveral places in the book. In principle, I don’t object to extending earlier presentation with new details once the reader gets a hold of some new concepts, but I feel that Coq’Art definitely goes too far. Coq’Art also presents material in a very unusual order. Almost every introduction to Coq or any other functional language begins with defining data types. Coq’Art introduces them in chapter 6. On the other hand sorts and universes – something I would consider an advanced concept for anyone who is not familiar with type-level programming – are presented in the second chapter. (Note that first chapter is a very brief overview of the language.) By contrast, CPDT goes into detailed discussion of universes in chapter 12 and SF does not seem to cover them at all. Overall, Coq’Art is of limited usefulness to me. To tell the truth this is not because of its focus on theory rather than practice, but because of language style, which I find rather inaccessible. Many times I had problems understanding passages I was reading, forcing me to re-read them again and again, trying to figure out what is the message that the authors are trying to convey. I did not have such problems with CPDT, SF, nor any other book I have read in the past few years. At the moment I have given up on the idea of reading the book from cover to cover. Nevertheless I find Coq’Art a good supplementary reading for SF. Most importantly because of the sections that explain in detail the inner workings of various tactics.

As mentioned at the beginning, I already wrote a first impressions post about CPDT. Back then I said the book “is a great demonstration of what can be done in Coq but not a good explanation of how it can be done”. Having read all of it I sustain my claim. CPDT does not provide a thorough and systematic coverage of basics, but instead focuses on advanced topics. As such, it is not the best place to start for beginners but it is a priceless resource for Coq practitioners. The main focus of the book is proof automation with Ltac, Coq’s language for writing automated proof procedures. Reader is exposed to Ltac early on in the book, but detailed treatment of Ltac is delayed until chapter 14. Quite surprisingly, given that it is hard to understand earlier chapters without knowing Ltac. Luckily, the chapters are fairly independent of each other and can be read in any order the reader wishes. Definitely it is worth to dive into chapter 14 and fragments of apter 13 as early as possible – it makes understanding the book a whole lot easier. So far I have already read chapter 14 three times. As I learn Coq more and more I discover new bits of knowledge with each read. In fact, I expect to be going back regularly to CPDT.

Coq’Art and CPDT approach teaching Coq in totally different ways. It might then be surprising that Software Foundations uses yet another approach. Unlike Coq’Art it is focused on practice and unlike CPDT it places a very strong emphasis on learning the basics. I feel that SF makes Coq learning curve as flat as possible. The main focus of SF is applying Coq to formalizing programming languages semantics, especially their type systems. This should not come as a big surprise given that Benjamin Pierce, the author of SF, authored also “Types and Programming Languages” (TAPL), the best book on the topic of type systems and programming language semantics I have seen. It should not also be surprising that a huge chunk of material overlaps between TAPL and SF. I find this to be amongst the best things about SF. All the proofs that I read in TAPL make a lot more sense to me when I can convert them to a piece of code. This gives me a much deeper insight into the meaning of lemmas and theorems. Also, when I get stuck on an exercise I can take a look at TAPL to see what is the general idea behind the proof I am implementing.

SF is packed with material and thus it is a very long read. Three months after beginning the book and spending with it about two days a week I am halfway through. The main strength of SF is a plethora of exercises. (Coq’Art has some exercises, but not too many. CPDT has none). They can take a lot of time – and I really mean a lot – but I think this is the only way to learn a programming language. Besides, the exercises are very rewarding. One downside of the exercises is that the book provides no solutions, which is bad for self-studying. Moreover, the authors ask people not to publish the solutions on the internet, since “having solutions easily available makes [SF] much less useful for courses, which typically have graded homework assignments”. That being said, there are plenty of github repositories that contain the solved exercises (I also pledge guilty!). Although it goes against the authors’ will I consider it a really good thing for self-study: many times I have been stuck on exercises and was able to make progress only by peeking at someone else’s solution. This doesn’t mean I copied the solutions. I just used them to overcome difficulties and in some cases ended up with proofs more elegant than the ones I have found. As a side note I’ll add that I do not share the belief that publishing solutions on the web makes SF less useful for courses. Students who want to cheat will get the solutions from other students anyway. At least that has been my experience as an academic teacher.

To sum up, each of the books presents a different approach. Coq’Art focuses on learning Coq by understanding its theoretical foundations. SF focuses on learning Coq through practice. CPDT focuses on advanced techniques for proof automation. Personally, I feel I’ve learned the most from SF, with CPDT closely on the second place. YMMV

Categories: Offsite Blogs

so strange but interesting

haskell-cafe - Wed, 06/08/2016 - 11:07am
Hi, I know it might be something strange, but still so interesting, you have to see it here <> Warmest, dek5< at > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

[ANN] New docs for the Aivika simulation platform

haskell-cafe - Wed, 06/08/2016 - 9:37am
Hi Cafe, I wrote a new article "Aivika - A Constructor of General-Purpose Simulation Libraries" [1]. It uncovers key ideas of that how I implemented nested simulation and parallel distributed simulation in the Aivika platform [2]. Monads, immutable data structures, managed side effects, continuations, streams, recursive computations are all those things that are widely used in Aivika. The article can be useful for those who will have a willingness to use my simulation libraries for nested simulation, or distributed simulation, or some other field I cannot still imagine. Finally, I wrote a small tutorial for beginners [3]. It takes a simple discrete event simulation model and shows how we can add a Monte-Carlo experiment, save the results in the CSV files, plot histograms and charts, for the example, the deviation chart with a trend and confidence interval using rule 3-sigma. This tutorial can be used for quick diving into Aivika. All the programming code is written in Haskell. Best regards, David Sorokin
Categories: Offsite Discussion

ANN: SciFlow-0.5.0

haskell-cafe - Tue, 06/07/2016 - 10:48pm
Hi Cafe, I've been working on a package to manage data analysis pipelines, mainly for personal use. But I feel there may be others who are interested in this as well, so I just published an up-to-date version to hackage. Briefly, this package help you design and manage data analysis pipelines written in Haskell, with computation steps being just Haskell functions with type: a -> IO b. I use template Haskell to construct the dependency graph, and computation steps are assembled according to the graph and type checked at compile time. Each step can be configured to run either locally or on a remote machine. Concurrency is also supported. Independent steps will run simultaneously. Take a look at for breif introduction and some examples. This package is still under heavy development, but it is quite stable otherwise as I've been using it on our cluster for some time. I hope you would find it useful and any feedback is welcome! _______________________________________________
Categories: Offsite Discussion

How to capture the output of GHCi :show command

haskell-cafe - Tue, 06/07/2016 - 7:02pm
I would like to be able to bind the output of GHCi's :show to a variable, but I don't see a nice way to do so. Is it possible to do this directly in GHCi? My specific use for this is appending to the current prompt.
Categories: Offsite Discussion

Vacancy: Professor Software technology at UtrechtUniversity

haskell-cafe - Tue, 06/07/2016 - 5:08pm
The Faculty of Science at Utrecht University is seeking to appoint a Full Professor in Software Technology to lead, alongside the other two chairs, the division of Software Systems within the Faculty. The full Professor directs and supervises research in the field of software technology, specifically in the design and development of formalisms and methodologies for effective program construction and program analysis. She/he develops new initiatives, aiming at research programs in software technology. This includes the acquisition of external research funds, both at the national and international levels, and the dissemination of research results and its applications to the relevant research communities. The full professor has a leading role in teaching and supervision. She or he contributes to the department’s curriculum development at BSc, MSc and PhD levels. The full professor plays an active role in the leadership and administrative duties of the Department and/or Faculty. For more information about
Categories: Offsite Discussion

Vacancy: Professor Software technology at UtrechtUniversity

General haskell list - Tue, 06/07/2016 - 5:07pm
The Faculty of Science at Utrecht University is seeking to appoint a Full Professor in Software Technology to lead, alongside the other two chairs, the division of Software Systems within the Faculty. The full Professor directs and supervises research in the field of software technology, specifically in the design and development of formalisms and methodologies for effective program construction and program analysis. She/he develops new initiatives, aiming at research programs in software technology. This includes the acquisition of external research funds, both at the national and international levels, and the dissemination of research results and its applications to the relevant research communities. The full professor has a leading role in teaching and supervision. She or he contributes to the department’s curriculum development at BSc, MSc and PhD levels. The full professor plays an active role in the leadership and administrative duties of the Department and/or Faculty. For more information about
Categories: Incoming News

Twan van Laarhoven: Stream fusion for streaming, without writing any code

Planet Haskell - Tue, 06/07/2016 - 3:02pm

I recently came accross the streaming library. This library defines a type Stream (Of a) m b for computations that produce zero or more values of type a in a monad m, and eventually produce a value of type b. This stream type can be used for efficient IO without having to load whole files into memory. The streaming library touts bechmark results showing superior performance compared to other libraries like conduit, pipes and machines.

Looking at the datatype definition,

data Stream f m r = Step !(f (Stream f m r)) | Effect (m (Stream f m r)) | Return r

it struck me how similar this type is to what is used in the stream fusion framework. The main difference being that the streaming library allows for interleaved monadic actions, and of course the lack of decoupling of the state from the stream to allow for fusion. But the vector library actually also uses such a monadic stream fusion framework, to allow for writing into buffers and such. This is type is defined in the module Data.Vector.Fusion.Stream.Monadic.

data Stream m a = forall s. Stream (s -> m (Step s a)) s data Step s a where Yield :: a -> s -> Step s a Skip :: s -> Step s a Done :: Step s a

So, why not try to use vector's stream type directly as a representation of streams? I added this type as an extra alternative to the benchmark, and without writing any more code, the results are pretty impressive:

The only function that could be improved is scanL. In vector this function is implemented in terms of prescan (scanL without the first element) and cons, which makes it pretty inefficient. So I made a specialized implementation.

And that's all. A simple streaming 'library' with state of the art performance, while writing hardly any new code. Now to be fair, there are some reasons why you wouldn't always want to use these fusing streams. In particular, the resulting code could get quite large, and without fusion they may not be the most efficient.

Categories: Offsite Blogs

On-site GHC-related Haskell/C opportunity atPositive Technologies (Moscow)

haskell-cafe - Tue, 06/07/2016 - 1:07pm
Good day! The Moscow office of Positive Technologies ( is looking for an experienced Haskell developer with a strong C background. You will be working in a team that develops a next generation security platform: think widely available, easy to use, dramatically enhanced security. In particular, we want you to help rewrite our core application in Haskell, which in turn requires porting GHC runtime to run on bare metal. Details can be seen in our Reddit posting: To apply, send you resume or questions to career< at > and CC skosyrev< at >
Categories: Offsite Discussion

uninstalling ghc-8.0.1-x86_64 installed through""

haskell-cafe - Mon, 06/06/2016 - 4:03pm
Hi all, How can I uninstall cleanly ghc-8.0.1-x86_64 that I installed using the script (found on website under Generic Linux). I'm on ubuntu Trusty. Thanks, Pat _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >
Categories: Offsite Discussion

WADT 2016 -- Extended Deadline

General haskell list - Mon, 06/06/2016 - 2:16pm
CFP: WADT 2016 - 23rd International Workshop on Algebraic Development Techniques (extended deadline) Link: When Sep 21, 2016 - Sep 24, 2016 Where Gregynog, UK Submission Deadline June 17, 2016 (extended) Notification July 3, 2016 (extended) Final Version Due July 15, 2016 AIMS AND SCOPE The algebraic approach to system specification encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, it now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed and mobile systems). The workshop will provide an opportunity to present recent and ongoing work, to meet colleagues, and to discuss new ideas and future trends. TOP
Categories: Incoming News

New Haddock

General haskell list - Mon, 06/06/2016 - 2:03pm
I couldn’t find an announcement of the new version of Haddock. You can now document your libraries even more beautifully. For example, will render as <> Also don’t forget you can put really nice diagrams in your documentation e.g. <> and <>. Dominic Steinitz dominic< at > _______________________________________________ Haskell mailing list Haskell< at >haskel
Categories: Incoming News

Philip Wadler: Papers We Love: John Reynolds, Definitional Interpreters for Higher Order Languages

Planet Haskell - Mon, 06/06/2016 - 11:32am
I will be speaking on John Reynolds paper, Definitional Interpreters for Higher Order Languages, at Papers We Love, London, 6:30pm Tuesday 7 June; details here.
Categories: Offsite Blogs

Having issue in running Haskell code in Atom

haskell-cafe - Sun, 06/05/2016 - 9:21pm
Hello All, I have started learning Haskell couple of days ago. I was looking for an IDE and found Atom as one of them. When I started using it I installed multiple packages and tried running creating Haskell files and saving it. This IDE always gives me following error. Please help to debug this: [Enter steps to reproduce below:] 1. ... 2. ... **Atom Version**: 1.7.4 **System**: Microsoft Windows 10 Pro **Thrown From**: [haskell-ghc-mod]( package, v1.14.5 ### Stack Trace Haskell-ghc-mod: ghc-mod failed to launch. It is probably missing or misconfigured. ENOENT ``` At Error: spawn ghc-mod ENOENT PATH: undefined path: undefined Path: C:\Program Files (x86)\Intel\iCLS Client\;C:\Program Files\Intel\iCLS Client\;C:\Windows\system32;C:\Windows;C:\Windows\System32\Wbem;C:\Windows\System32\WindowsPowerShell\v1.0\;C:\Program Files\Intel\Intel(R) Management Engine Components\DAL;C:\Program Files (x86)\Intel\Intel(R) Management Engine Components\DAL;C:\Program F
Categories: Offsite Discussion

Robert Harper: PFPL Commentary

Planet Haskell - Sun, 06/05/2016 - 8:42pm

I am building a web page devoted to the 2nd edition of Practical Foundations for Programming Languages, recently published by Cambridge University Press.  Besides an errata, the web site features a commentary on the text explaining major design decisions and suggesting alternatives.  I also plan to include additional exercises and to make sample solutions available to faculty teaching from the book.

The purpose of the commentary is to provide the “back story” for the development, which is often only hinted at, or is written between the lines, in PFPL itself.  To emphasize enduring principles over passing fads, I have refrained from discussing particular languages in the book.  But this makes it difficult for many readers to see the relevance.  One purpose of the commentary is to clarify these connections by explaining why I said what I said.

As a starting point, I explain why I ignore the familiar concept of a “paradigm” in my account of languages.  The idea seems to have been inspired by Kuhn’s (in)famous book The Structure of Scientific Revolutions, and was perhaps a useful device at one time.  But by now the idea of a paradigm is just too vague to be useful, and there are many better ways to explain and systematize language structure.  And so I have avoided it.

I plan for the commentary to be a living document that I will revise and expand as the need arises.  I hope for it to provide some useful background for readers in general, and teachers in particular.  I wish for the standard undergraduate PL course to evolve from a superficial taxonomy of the weird animals in the language zoo to a systematic study of the general theory of computation.  Perhaps PFPL can contribute to effecting that change.



Filed under: Research, Teaching
Categories: Offsite Blogs

Ken T Takusagawa: [awlyiqda] Type signatures asking for more than they need

Planet Haskell - Sun, 06/05/2016 - 7:14pm

A type signature to a function creates the requirement that an argument passed to the function have a specified type.  However, operationally, the function only needs for the argument to have certain operations (other functions) defined on it.

Type classes in Haskell provide a means for a function to be polymorphic, accepting many different types, with the type class defining the set of fundamental functions (methods) available.  However, even type classes may be too much: a function might require only a subset of the fundamental functions.

Duck typing is a much "looser" way of addressing this same problem.  Previous thoughts on this problem.

Sometimes, even though all the operations a function needs might be defined on a type, we want to use the type signature of the function to restrict what it can be called on.  The "explode" method might be defined for both firecrackers and nuclear weapons, but we might never want to accidentally pass a nuclear weapon to a certain function.

There is also a software engineering, and somewhat social, aspect to this problem.  Even though today's implementation of a function might not require some method of a type class, tomorrow's improved implementation might.  Declaring the type signature to be more than minimal is like making a reservation for future demands of functionality in the arguments.  Making such a reservation forces all other software calling that function to provide that functionality, even though it isn't currently used.  A type signature therefore represents a battle over a property line: who "owns" the right to decide what functionality an object should have?

Categories: Offsite Blogs

haskell-ide-engine versus hsdev (and Debuggers)

haskell-cafe - Sun, 06/05/2016 - 6:35pm
Hello, I am new to Haskell and thinking of contributing to the IDE efforts. I've noticed two projects which aim to provide a "service" that editors and IDEs can call to help present useful information to programmers. I am wondering how these projects differ and why they are separate efforts since they seem to have very similar end goals? Another thing that I am wondering is if either of these two projects aims to provide debugger support and what the general state of debuggers for Haskell is? I've seen a project for a Haskell remote debugger which looks it was ghci/interpreter based and was being used by Eclipse and IntelliJ. It didn't work when I tried it, however, and I am not sure that the project is still active. It also looks like ghc only recently began adding support for debugging compiled Haskell and that initial efforts may be to get things working with gdb or lldb. Am I correctly understanding the current landscape as far as Haskell debuggers go? Thanks! Leonard _________________________________
Categories: Offsite Discussion

Final CFP: 4th ACM SIGPLAN International Workshop onFunctional Art, Music, Modelling and Design

haskell-cafe - Sun, 06/05/2016 - 2:09pm
4th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design Co-located with ICFP Nara, Japan, 24 September, 2016 Key Dates: Submission deadline - June 24 Author Notification - 15 July Camera Ready - 31 July Workshop - September 24, 2016 We welcome submissions from academic, professional, and independent programmers and artists. Final Call for Papers, Demos, *and* Performances The ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design (FARM) gathers together people who are harnessing functional techniques in the pursuit of creativity and expression. Functional Programming has emerged as a mainstream software development paradigm, and its artistic and creative use is booming. A growing number of software toolkits, frameworks and environments for art, music and design now employ functional programming languages and techniques. FARM is a forum for exploration and critical evaluation of these developments,
Categories: Offsite Discussion