Admin

Do Be Do Be Do

Monads and algebraic effects are general concepts that give a definition of what a "side-effect" can be: an instance of monad, or an instance of algebraic effect, is a specific realization of a side-effect. While most programming languages provide a fixed family of built-in side-effects, monads or algebraic effects give a structured way to introduce a new notion of effect as a library.

A recent avenue of programming language research is how to locally define several realizations of the same effect interface/signature. There may be several valid notions of "state" or "non-determinism" or "probabilistic choice", and different parts of a program may not require the same realization of those -- a typical use-case would be mocking an interaction with the outside world, for example. Can we let users locally define a new interpretation of an effect, or write code that is generic over the specific interpretation? There are several existing approaches, such as monad transformer stacks, free monads interpreters, monad reification and, lately, effect handlers, as proposed in the programming language Eff.

Frank, presented in the publication below, is a new language with user-defined effects that makes effect handling a natural part of basic functional programming, instead of a separate, advanced feature. It is a significant advance in language design, simplifying effectful programming. Functions, called operators, do not just start computing a result from the value of their arguments, they interact with the computation of those arguments by having the opportunity to handle any side-effects arising during their evaluation. It feels like a new programming style, a new calling convention that blends call-by-value and effect handling -- Sam Lindley suggested the name call-by-handling.

Frank also proposes a new type-and-effect system that corresponds to this new programming style. Operators handle some of the effects raised by their arguments, and silently forward the rest to the computation context; their argument types indicate which effects they handle. In other words, the static information carried by an argument types is the delta/increment between the effects permitted by the ambient computation and the effects of evaluating this argument. Frank calls this an adjustment over the ambient ability. This delta/increment style results in lightweight types for operators that can be used in different contexts (a form of effect polymorphism) without explicit quantification over effect variables. This design takes part in a research conversation on how to make type-and-effect systems usable, which is the major roadblock for their wider adoption -- Koka and Links are also promising in that regard, and had to explore elaborate conventions to elide their polymorphic variables.

Another important part of Frank's type-system design is the explicit separation between values that are and computations that do. Theoretical works have long made this distinction (for example with Call-By-Push-Value), but programmers are offered the dichotomy of either having only effectful expressions or expressing all computations as values (Haskell's indirect style). Frank puts that distinction in the hands of the user -- this is different from distinguishing pure from impure computations, as done in F* or WhyML.

If you wish to play with the language, a prototype implementation is available.


Do Be Do Be Do (arXiv)
Sam Lindley, Conor McBride, Craig McLaughlin
2017

We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar’s effect handler abstraction.

Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is simply the special case of a Frank operator that interprets no commands. Moreover, Frank’s operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values.

Effect typing in Frank employs a novel form of effect polymorphism which avoid mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards.

We introduce Frank by example, and then give a formal account of the Frank type system and its semantics. We introduce Core Frank by elaborating Frank operators into functions, case expressions, and unary handlers, and then give a sound small-step operational semantics for Core Frank.

Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type system.

Admin

As many of you know, the email functionality of the website has not been working for a very, very long time. In addition, all new users are still being approved by me, to combat spam. All this means manual work by me, prompted by frustrated emails by new members. Alas, given other commitments, I find that the backlog is growing and I simply cannot find the time to handle these emails (i.e., approve the user, set an initial password, let them know and ask them to change it). If any member want to help me with this, I would be grateful. This will involve getting extra admin privileges on the site, after which I can forward the requests in the pipe line to you to approve.

Thanks!

Dynamic Witnesses for Static Type Errors (or, ill-typed programs usually go wrong)

Dynamic Witnesses for Static Type Errors (or, ill-typed programs usually go wrong) by Eric L. Seidel, Ranjit Jhala, Westley Weimer:

Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to dynamically synthesize witness values that can make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses.

Sounds like a great idea to make type systems more accessible, particularly for beginners. The current limitations are described the discussion, section 54:

There are, of course, drawbacks to our approach. Four that stand out are: (1) coverage limits due to random generation, (2) the inability to handle certain instances of infinite types, (3) dealing with an explosion in the size of generated traces, and (4) handling ad-hoc polymorphism.

It's also not clear whether this would produce proper witnesses for violations of higher kinded types or other more sophisticated uses of type systems. There are plenty of examples where invariants are encoded in types, eg. lightweight static capabilities.

How to Build Static Checking Systems Using Orders of Magnitude Less Code

How to Build Static Checking Systems Using Orders of Magnitude Less Code, by Fraser Brown Andres Notzli Dawson Engler:

Modern static bug finding tools are complex. They typically consist of hundreds of thousands of lines of code, and most of them are wedded to one language (or even one compiler). This complexity makes the systems hard to understand, hard to debug, and hard to retarget to new languages, thereby dramatically limiting their scope.

This paper reduces the complexity of the checking system by addressing a fundamental assumption, the assumption that checkers must depend on a full-blown language specification and compiler front end. Instead, our program checkers are based on drastically incomplete language grammars (“micro-grammars”) that describe only portions of a language relevant to a checker. As a result, our implementation is tiny—roughly 2500 lines of code, about two orders of magnitude smaller than a typical system. We hope that this dramatic increase in simplicity will allow developers to use more checkers on more systems in more languages.

We implement our approach in µchex, a language-agnostic framework for writing static bug checkers. We use it to build micro-grammar based checkers for six languages (C, the C preprocessor, C++, Java, JavaScript, and Dart) and find over 700 errors in real-world projects.

Looks like an interesting approach with some compelling results, and will make a good tool for the toolbox. See also the Reddit thread for further discussion.

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness by Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon Peyton Jones:

For ML and Haskell, accurate warnings when a function definition has redundant or missing patterns are mission critical. But today’s compilers generate bogus warnings when the programmer uses guards (even simple ones), GADTs, pattern guards, or view patterns. We give the first algorithm that handles all these cases in a single, uniform framework, together with an implementation in GHC, and evidence of its utility in practice.

Another great paper on a very useful incremental improvement on GADTs as found in Haskell, OCaml and Idris. Exhaustiveness checking is critical for a type system's effectiveness, and the redundant matching warnings are a nice bonus.

Domain settings

I am about to make some changes to the name server definitions. Since changes take time to propagate, you may have trouble reaching the site for awhile. If this happens, try using the .com domain instead of the preferred .org domain.

LtU's new server

Lambda the Ultimate is now running on a new, faster, more reliable server. The old one is now, uh... pining for the fjords. This should resolve the increasingly frequent outages we've seen recently. Because the old server had started failing, we didn't have time to do as much quality control on the migration as we would have liked. If anyone notices any issues with the site, please comment in this thread. Currently known issues:
  • Non-Latin UTF-8 characters apparently didn't survive the database migration correctly. This is a particular issue if you have a username containing non-Latin characters - you may not be able to log in currently.
  • It's possible that some comments posted later on Monday don't appear on the new site. (Resolved: there were no missing comments)
  • New user signup emails are not yet working.
  • Due to DNS propagation, not everyone will see the new site immediately. (Now resolved)
The struck out issues have been resolved. The remaining issue, with user signup emails, should be resolved in the next few days.

LtU is migrating from Drupal

As many of you know we have been suffering for a long time from the deficiencies of Drupal. We have not updated our infrastructure for a long time. Among the features members have been asking for are better integration with other sites and more social features. In particular, many said they want to be able to mark the posts that they find particularly helpful. I am happy to announce that we have big news!

In the coming days we will be migrating LtU from Drupal to Facebook. All the awesome features of Facebook will be automatically available; in particular the "Like" mechanism. You will also be able to share photos with other PLT enthusiasts, re-share their shares etc. Best of all, you will be guaranteed the privacy standards of Facebook.

Rest assured, we have not made this decision without considering the alternatives. We studied Google+ but given Google's unprovoked assault on RSS with the decision to discontinue Google Reader we found it unconscionable to go with Google.

LtU's twitter feed will have to go, I am afraid, given the relationship between our new home and twitter. Hopefully this issue will be resolved once twitter gives up and is acquired by FB.

The LtU feed will have ads, per usual on FB. I know this is somewhat of an inconvenience, but at least the ads you will be served will be personalized[1].

Ehud and the LtU Team.

[1] I am assured that ads for dynamically typed and scripting languages will never be served to you again after you mark them as "offensive" once.


Update: No, we are not migrating to Facebook. This was an April Fools joke.

Who's online

Earlier today I enabled a drupal feature that list the names of users currently online. It was on the bottom of the right-hand navigation bar, and looked something like this:

Who's online
There are currently 7 users and 887 guests online.
Online users:

Matt M
Ehud Lamm
Mattias Engdegård
naasking
Andreas Rossberg
...

Some might see this as a privacy violation or otherwise object. Since I heard complaints I disabled this feature. What do you think?

Setting up new accounts suspended

Due to issues with spam accounts I have suspended the creation of new accounts. New members cannot sign up for an account at the moment. I apologize for the inconvenience.

XML feed