Day 1 - Intro Problem

As a reminder, these writeups won't be super detailed, since I have to do one every day. I'll try to focus on the key ideas though, and I'll always link to my code!

Solution code on GitHub

All 2022 Problems

Subscribe to Monday Morning Haskell!

Problem Overview

This year we're dealing with elves. Each elf is carrying some snack items with a certain number of calories. Our input has one calorie count per line, and an empty line denotes that we have reached the end of one elf's snack collection and started another.

1000
2000
3000

4000

5000
6000

7000
8000
9000

10000

For the first part, we just want to find the elf with the most calories. This is the 4th elf, with a total of 24000 calories (7000+8000+9000).

For the second part, we want the sum of calories from the three elves with the most. So we take the 24000 from the elf with the most, and add the 3rd elf (11000 calories) and the 5th elf (10000 calories). This gives a total of 45000.

Full Description

Solution Approach and Insights

Nothing complicated here. Once we parse into list-of-lists-of-ints, we just use map sum and either take the maximum or the sum of the top 3.

Relevant Utilities

Function parseFile

Parsing the Input

Here's our parsing code. One nuance...I needed to add an extra empty line to the given inputs in order to make this parse work. Dealing with empty line separators is a little tricky with megaparsec (or at least I haven't mastered the right pattern yet), because the "chunk separator" is the same as the "line separator" within each chunk (eol parser).

parseInput :: (MonadLogger m) => ParsecT Void Text m [[Int]]
parseInput =
  sepEndBy1 parseIntLines eol
  where
    parseIntLines = some parseIntLine
    parseIntLine = do
      i <- parsePositiveNumber
      eol
      return i

Getting the Solution

As above, nothing complicated here. Use map sum and take the maximum.

processInputEasy :: (MonadLogger m) => [[Int]] -> m Int
processInputEasy intLists = return $ maximum (map sum intLists)

With the hard part, we sort, reverse, take 3, and then take another sum.

processInputHard :: (MonadLogger m) => [[Int]] -> m Int
processInputHard intLists = return $ sum $ take 3 $ reverse $ sort (map sum intLists)

Answering the Question

And no additional processing is needed - we have our answer! (My standard template has the answer always wrapped in Maybe to account for failure cases).

solveEasy :: FilePath -> IO (Maybe Int)
solveEasy fp = runStdoutLoggingT $ do
  input <- parseFile parseInput fp
  Just <$> processInputEasy input

solveHard :: FilePath -> IO (Maybe Int)
solveHard fp = runStdoutLoggingT $ do
  input <- parseFile parseInput fp
  Just <$> processInputHard input

Video

Link to YouTube

by James Bowen at December 01, 2022 04:00 PM

Higher-orderness is first-order interaction

There is an inherent beauty to be found in simple, pervasive ideas that shift our perspective on familiar objects. Such ideas can help tame the complexity of abstruse abstractions by offering a more intuitive angle from which to understand them.

The aim of this post is to present an alternative angle — that of interactive semantics — from which to view one of the fundamental notion of functional programming: higher-order functions.

Interactive semantics provide an intuitive understanding of the concept of higher-order functions, which is a worthy mathematical investigation in itself. But this approach is also practical, shedding a new light on existing programming techniques and programming language features. We will review the example of higher-order contracts in this post. We will also present direct application of interactive semantics in the design and the implementation of programming languages.

Denotational semantics

Take the following programs, written respectively in Java, Rust, and Haskell:

public int incrByTwo(int x) {
  return x + 2;
}

fn incr_by_two(x: i32) -> i32 {
    let constant = 1;
    let offset = 1;
    constant + offset + x
}

incrByTwo :: Int -> Int
incrByTwo x = 1 + x + 1

While they look different on the surface, our intuition tells us that they are also somehow all the same. But what does “being the same” even mean for functions defined in such different languages?

One point of view is that syntax is merely a way to represent a more fundamental object, and that each of the above examples in fact represents the exact same object. From a purely mathematical point of view, these programs all fundamentally represent the function which adds $2$ to its argument.

$f:\mathbb{Z}\to \mathbb{Z}=x\mapsto x+2$.

The process of stripping away the purely syntactic details of a program to discover the mathematical objects at its core is the main concern of the field of denotational semantics. We refer to the mathematical object a program represents as its denotation. The idea being that by ridding ourselves of the unimportant details of a particular syntax we can focus better on the essence of the program.

The motivation for doing this partly stems from fundamental philosophical questions, such as: “what really is a program?” Attempting to answer such questions unveils deep connections between computer science and the rest of mathematics. However, stripping a program down to its substance can also provide us with techniques to answer much more concrete questions. For example: proving that two given programs always behave in the same way.

While incrByTwo operates on integers, even the most bare-bone functional language features much more complex objects: functions.

Higher-orderness

A higher-order function is a function which manipulates other functions. The various instances of incrByTwo only represent a first-order function, since their sole argument is a number. On the other hand, the usual map operation on lists is higher-order, as it takes as an argument a function describing how to transform each element of the list. This can be seen clearly in the Haskell syntax for the type of map, in particular the presence of the function type (a -> b) as the first argument:

map :: (a -> b) -> [a] -> [b]

Integers are easy to grok. They are static pieces of data that one can inspect and pass around. Functions are a different matter: they are an opaque entity that can only be actioned by handing it over data or functions.

This distinction is not only theoretical but also practical: while choosing a concrete representation of integers on a CPU is often relatively simple, selecting a representation for functions and closures, together with a calling convention, is not.

Traditionally, mathematicians have simply encoded functions as data. In set theory, the formal lingua franca of modern mathematics, a function is a (potentially infinite) set of tuples pairing each input with the corresponding output. Our incrByTwo denotation $n\mapsto n+2$ is represented as the infinite set:

$\{\dots ,(-1,1),(0,2),(1,3),\dots \}=\{(n,n+2)\mid n\in \mathbb{Z}\}$

While the set representation of functions is useful for mathematics, a static, infinite dictionary with virtually instant lookup turns out not to be a great model for computation, for a number of philosophical and technical reasons¹. At its core, the notion of functions as sets ignores a fundamental concept of computation: time, and its direct manifestation, interaction.

Interactive semantics

Game Semantics (GS hereafter) is a line of thought which takes its root in dialectical interpretations of logic. In GS, we not only consider the inputs and outputs of a higher-function, but also all the interactions with other functions given as arguments. That is, we consider the traces of the function (the Player in GS), viewed as a dialogue with an Opponent, representing the environment in which the function executes (the calling context).

Take a simple higher-order function:

negate :: (Bool -> Bool) -> Bool -> Bool
negate f x = if f x then false else true

The evaluation of the run negate (\y. y) false now corresponds to a play in a game defined by the type of negate. Let’s first attach a unique label to each occurrence of Bool:

(Bool -> Bool) -> Bool -> Bool
( B1 ->   B2 ) ->  B3  ->  B4

The play goes like this ²:

• Opponent (caller): hey, could you give me your return value (B4) ?
• Player (negate): sure, but first give me the return value of f (evaluating f x, B2)
• O: ok, but first give the value of its parameter y (B1)
• P: ok, then I need the value of my parameter x (B3)
• O: x is false (B3)
• P: then y is false (B1)
• O: then f returns false (B2)
• P: then I finally return true (B4)

The full denotation of negate is then a strategy for this game.

Polarity

The game partitions the occurrences of Bool into outputs/positive, where the Opponent asks first and the Player answers, and inputs/negative, where roles are switched. This distinction is called polarity.

Consider the anonymous function \y. y from the previous call to negate (let’s call it f).

The play for f false, from the point of view of f, looks like:

• O: asks for return value
• P (f): asks for parameter y
• O: answers y is false
• P: returns false

If you come back to the first play of negate and hide the moves external to the call f x, the above play exactly matches a subset of the original one, just with the polarities flipped!

• Opponent (caller): hey, could you give me your return value (B4) ?
• Player (negate): sure, but first give me the return value of f (evaluating f x, B2)
• O: sure, but first give the value of the its parameter y (B1)
• P: ok, then I need the value of my parameter x (B3)
• O: x is false (B3)
• P: then y is false (B1)
• O: then f returns false (B2)
• P: then I finally return true (B4)

The Player/Opponent distinction is perfectly symmetric. Indeed, from the point of view of f in the subcall f x, the caller is negate, which thus becomes the opponent.

Determining the polarity is easy: look at the type of the function and compute the path from the root to a type occurrence in terms of going to the left or to the right of an arrow. The occurrence is positive if the number of left is even (including 0), and negative otherwise. For negate, working on a type with labels and parentheses ((B1 ->a B2) ->b (B3->c B4)):

• B1 is positive (left of ->b, left of ->a)
• B2 is negative (left of ->b, right of ->a)
• B3 is negative (right of ->b, left of ->c)
• B4 is positive (right of ->b, right of ->c)

The essence of GS is to model the execution of a higher-order function as an interaction over basic values. The beauty lies in the simplicity of the concept and the perfect symmetry between Player and Opponent. Polarity tells us if a value is an input, which must be provided by the environment, or an output, which must be provided by the function, either directly or indirectly through subcalls.

From a theoretical perspective, GS was the first technique to provide a class of denotational models that satisfy a strong form of correspondence between programs and their denotations (they gave the first fully abstract model for PCF). Game semantics seems to hit a sweet-spot by hiding unessential aspects of programs without forgetting the essential dynamic of interaction.

But the GS point of view is also practical. Let’s illustrate a few applications equipped with our new interactive lens.

Applications

Higher-order contracts

At Tweag, I am working on a configuration language called Nickel. Nickel features contracts, a form of higher-order dynamic type-checking. Contracts enable safe interaction between typed code and untyped code by preventing the untyped code from injecting ill-typed parameters.

Take a variant of our negate function in Nickel:

let negate : (Bool -> Bool) -> Bool -> Bool = fun f x => !(f x)

When calling e.g. negate (fun y => y) false from untyped code, the interpreter will check that the values bound to x, y, f x, and !(f x) are booleans.

Now, if we break the contract of f by calling negate (fun y => 2) false, the first line of the output will be:

error: contract broken by the caller

Conversely, if we define negate to break the contract of f³:

negate | (Bool -> Bool) -> Bool -> Bool = fun f x => !(f 5)

And make a legal call negate (fun y => y) false, the error becomes:

error: contract broken by a function

Higher-order contracts are precisely exploiting the same idea of breaking higher-orderness into first-order interactions! A contract for a higher-order function decomposes into primitive contracts (here Bool), incurring one check for each type occurrence. The blame distinction caller/function corresponds to the polarity of GS.

The trace of the second example looks like (labelling the type as (B1 -> B2) -> B3 -> B4):

• Opponent (caller): let’s check that negate returns a Bool (evaluating negate (fun y => y) false, B4)
• Player (negate): sure, but first let’s check that f returns a Bool (evaluating f x, B2)
• O: ok, but then I need a Bool for y (B1)
• P: ok, then I need a Bool for x (B3)
• O: x is false (B3)
• P: ok, false is a Bool. Then y is 5 (B1)
• O: hey, 5 is not a Bool! I blame the player (B1)

For the typed version of negate, Player represents the internal, type-safe boundaries. Opponent is the external world, potentially untyped, and the contract is the border police meticulously controlling everything that crosses the boundary.

Circuits and distributed computing

If you look at the plays of the previous section, they have strong feeling of message-passing style. The function is exchanging primitive data with the environment. This view has been exploited for example to design compilation techniques and a language runtime that makes it trivial to break down terms and run them on distinct distributed nodes. In contrast, making a classic stack-based virtual machine distributed is not trivial.

The interactive interpretation has been used as well to compile high level functional programs down to integrated circuit, precisely by reducing the complexity of higher-orderness to exchanging first-order messages⁴.

Conclusion

Interactive semantics like Game Semantics have moved forward the understanding of the nature of programs and computations by incorporating an aspect forgotten by a naive set-based semantics: interaction. Such interactive semantics have proven theoretically fruitful and particularly flexible (they can model side effects, concurrency, and more). Game Semantics also has practical applications by serving as a guideline for compilation techniques and language design.

But in the end, I think that the richness of the interactive semantics resides in its surprisingly simple and intuitive foundation (who has never played games!). My humble hope for this post is that in a no so distant future, you may stare at a language feature, an abstract concept or a programming technique and suddenly exclaim:

Of course! It’s just that higher-orderness is first-order interaction.

---

1. Non-exhaustively:

   • Set-theoretic functions don’t work well for an untyped functional language (where everything has the same type) for cardinality reasons
   • Set-theoretic functions don’t work well with polymorphism

   ↩

2. The dataflow may look funny if you’re used to languages using the common strict evaluation strategies. Here, we first enter the body of the function, and only ask for and evaluate arguments when their value is actually used: Haskell programmers may have recognized a non-strict evaluation strategy (here, call-by-name). GS can also model strict evaluation, but we stick to the traditional presentation of games for simplicity.↩

3. negate isn’t well-typed anymore, so we use a contract annotation | which eschews typechecking but keeps the runtime checks↩

4. Geometry of Synthesis I, II, III, and IV.↩

December 01, 2022 12:00 AM

Advent of Code 2022!

Tomorrow is December 1st, which means that tonight (midnight Eastern American time, 9pm Pacific) is the start of Advent of Code! This is an informal, annual coding contest where you can solve one programming puzzle each day from December 1st up through Christmas on December 25th. The problems generally get more challenging as the month goes on, as you'll start needing to use more advanced data structures and solution techniques.

Last year I did Advent of Code for the first time, writing up all my solutions in Haskell (of course). This year I will be doing the contest again, and this time I plan to create more blog content as I go, rather than doing writeups way after the fact. Of course, I might not be able to do everything every day, but I'll try to keep up!

Here are all the ways I'll be trying to put my solutions out there for you to learn from (and critique!).

Code

I will push all my code to my GitHub repository, on the aoc-2022 branch. So once my solutions are done you'll be able to see them for yourself!

Writeups

I will also attempt to do daily write-ups on the blog, giving a rough descriptive outline of each solution. These won't be as detailed as the write-ups I did in the last month or so, but all the code will be there and I'll describe all the key insights and general solution approach.

Videos

I'll also be recording myself as I solve the problems so you can watch my solution process in real time. I'll post these videos to my YouTube channel. These videos will generally be unedited since I won't have time to go back through everything every day. I also won't be able to do these as much when it gets closer to Christmas as I'll be traveling and away from my recording setup. Some of these videos might have more commentary, some might have less. I haven't decided yet and it will vary from day-to-day.

Streaming

I will not have a regular streaming schedule. As much as possible, I plan to attempt to solve problems as soon as they come out, and the contest rules request that people do not stream solutions until the leaderboard (for the fastest solutions) is filled for that particular problem. This is in order to prevent someone from copying the solution and getting on the leaderboard without effort. (For what it's worth, I doubt I'll actually be fast enough to get on the leaderboard).

If I get behind on my solutions, then it's very possible I'll do some streaming sessions while I catch up. You can follow me on Twitter or on my Twitch stream to know when I'm going live!

Conclusion

I'll try to keep up and solve the problem every day and keep up with content, but life gets busy, so I can't make any guarantees! But hopefully I'll have all the solutions published by the end of the year!

I encourage you to try out the Advent of Code problems for yourself! It's a great tool for learning a new programming language (especially Haskell!).

I'll also be doing a couple newsletter updates over the course of this month, so make sure to subscribe to our mailing list to get those and stay up to date!

by James Bowen at November 30, 2022 03:30 PM

A Remarkable Property of Real-Valued Functions on Intervals of the Real Line

Today the 17 October 2019 I discussed a very remarkable fixed point theorem discovered by the Ukrainian mathematician Oleksandr Micholayovych Sharkovsky.

We recall that a periodic point of period for a function is a point such that . With this definition, a periodic point of period is also periodic of period for every which is a multiple of . If but for every from 1 to , we say that is the least period of .

Theorem 1. (Sharkovsky’s “little” theorem) Let be an interval and let be a continuous function su. If has a point of least period 3, then it has points of arbitrary least period; in particular, it has a fixed point.

Note that no hypothesis is made on being open or closed, bounded or unbounded.

Our proof of Sharkovsky’s “little” theorem follows the one given in (Sternberg, 2010), and could even be given in a Calculus 1 course: the most advanced result will be the intermediate value theorem.

Lemma 1. Let be a compact interval of the real line, let be a continuous function. Suppose that for some compact interval it is . Then has a fixed point in .

Proof. Let and be the minimum and the maximum of in , respectively. As , it is and . Choose such that and . Then is nonpositive at and nonnegative at . By the intermediate value theorem applied to , must have a fixed point in the closed and bounded interval (possibly reduced to a single point) delimited by and , which is a subset of .

Lemma 2. In the hypotheses of Lemma 1, let be a closed and bounded interval contained in . Then there exists a closed and bounded subinterval of such that .

Proof. Let . We may suppose , otherwise the statement is trivial. Let be the largest such that . Two cases are possible.

1. There exists such that . Let be the smallest such , and let . Then surely , but if for some we had either or , then by the intermediate value theorem, for some  we would also have either or , against our choice of and .
2. for every . Let then be the largest such that , and let . Then for reasons similar to those of the previous point.

Proof of Sharkovsky’s “little” theorem. Let be such that , , and . Up to cycling between these three values and replacing with , we may suppose . Fix a positive integer : we will prove that there exists such that and for every .

Let and be the “left” and “right” side of the closed and bounded interval : then and by the intermediate value theorem. In particular, , and Lemma 1 immediately tells us that has a fixed point in . Also, , so also has a point of period 2 in , again by Lemma 1: call it . This point cannot be a fixed point, because then it would also belong to as , but which has period 3. As we can obviously take , we only need to consider the case .

By Lemma 2, there exists a closed and bounded subinterval of such that . In turn, as , there also exists a closed and bounded subinterval of such that , again by Lemma 2: but then, . By iterating the procedure, we find a sequence of closed and bounded intervals such that, for every , and .

We stop at and recall that : we are still in the situation of Lemma 2, with in the role of . So we choose as a closed and bounded subinterval not of , but of , such that . In turn, as , there exists a closed and bounded subinterval of such that . Following the chain of inclusions we obtain . By Lemma 1, has a fixed point in , which is a periodic point of period for .

Can the least period of for be smaller than ? No, it cannot, for the following reason. If has period , then so has , and in addition is divisible by . But while for every : consequently, if has period , then . But this is impossible, because by construction as , while .

Theorem 1 is a special case of a much more general, and complex, result also due to Sharkovsky. Before stating it, we need to define a special ordering on positive integers.

Definition. The Sharkovsky ordering between positive integers is defined as follows:

• Identify the number , with odd integer, with the pair .
• Sort the pairs with in lexicographic order.
  That is: first, list all the odd numbers, in increasing order; then, all the doubles of the odd numbers, in increasing order; then, all the quadruples of the odd numbers, in increasing order; and so on.
  For example, and
• Set for every and .
  That is: the powers of 2 follow, in the Sharkovskii ordering, any number which has an odd factor.
  For example, .
• Sort the pairs of the form —i.e., the powers of 2—in reverse order.

The set of positive integer with the Sharkowsky ordering has then the form:

Note that is a total ordering.

Theorem 2. (Sharkovsky’s “great” theorem) Let be an interval on the real line and let be a continuous function.

1. If has a point of least period , and , then has a point of least period . In particular, if has a periodic point, then it has a fixed point.
2. For every integer it is possible to choose and so that has a point of minimum period and no points of minimum period for any . In particular, there are functions whose only periodic points are fixed.

Bibliography:

• Keith Burns and Boris Hasselblatt. The Sharkovsky theorem: A natural direct proof. The American Mathematical Monthly 118(3) (2011), 229–244. doi:10.4169/amer.math.monthly.118.03.229
• Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, Second Edition, Westview Press 2003.
• Shlomo Sternberg, Dynamical Systems, Dover 2010.

by Silvio Capobianco at November 29, 2022 05:58 PM

Black Friday Sale Ends Today!

Today is Cyber Monday, which marks the last day of our Black Friday Thanksgiving sale! This is your last chance to get the biggest deals of the year on all of our online courses here at Monday Morning Haskell!

For the rest of the day, you can get 20% off any of our courses by using the code BLACKFRIDAY22 at checkout. And you can get an extra discount (up to 30% off) if you subscribe to our monthly newsletter!

Here's one final review of our different courses.

Haskell From Scratch

This is our full-length beginners course. It will give you a full introduction to Haskell's syntax and core concepts. You'll also get the chance to start developing your Haskell problem solving skills. It's the best option if you've never written a full Haskell project before!

Course Description

---

Making Sense of Monads

This shorter course focuses strictly on monads and other functional structures. If monads have been a tricky subject for you in the past, hopefully this course can help you finally conquer them! The course includes two mini-projects for you to hone your skills!

Course Description

---

Effectful Haskell

Effectful Haskell goes a step beyond our introductory monads course. You'll learn some practical applications for advanced monadic ideas - like how to use monad classes and free monads to organize effects in your program. Effectful Haskell also includes some basic practice in deploying an application to Heroku.

Course Description

---

Practical Haskell

Practical Haskell is our second full-length course. Over the course of five modules, you'll build out the different layers of a full-stack application. You'll learn how to interact with a database, build a web server and develop a web frontend with Elm!

Course Description

---

Haskell Brain

Haskell Brain is our machine-learning course. It will teach you how to use TensorFlow in conjunction with Haskell, as well as a couple other related libraries and techniques!

Course Description

---

Conclusion

So don't miss out on these offers! Remember the code BLACKFRIDAY22 at checkout for 20% off, and you can subscribe to our mailing list for an ever better offer!

Later this week, we'll be back with the start of Advent of Code, so there will be a ton of new content in the next month!

by James Bowen at November 28, 2022 03:30 PM

Haskell development job with Well-Typed

tl;dr If you’d like a job with us, send your application as soon as possible.

Over the next few months, we are looking for one or more Haskell experts to join our team at Well-Typed. At the moment, we are looking particularly for someone who is knowledgeable and interested in one or more of the following areas:

• GHC development.
• General Haskell development, with a good understanding of issues relating to performance.

This is a great opportunity for someone who is passionate about Haskell and who is keen to improve and promote Haskell in a professional context.

About Well-Typed

We are a team of top notch Haskell experts. Founded in 2008, we were the first company dedicated to promoting the mainstream commercial use of Haskell. To achieve this aim, we help companies that are using or moving to Haskell by providing a range of services including consulting, development, training, and support and improvement of the Haskell development tools. We work with a wide range of clients, from tiny startups to well-known multinationals. We have established a track record of technical excellence and satisfied customers.

Our company has a strong engineering culture. All our managers and decision makers are themselves Haskell developers. Most of us have an academic background and we are not afraid to apply proper computer science to customers’ problems, particularly the fruits of FP and PL research.

We are a self-funded company so we are not beholden to external investors and can concentrate on the interests of our clients, our staff and the Haskell community.

About the job

The role is not tied to a single specific project or task, and is fully remote.

In general, work for Well-Typed could cover any of the projects and activities that we are involved in as a company. The work may involve:

• working on GHC, libraries and tools;

• Haskell application development;

• working directly with clients to solve their problems;

• teaching Haskell and developing training materials.

We try wherever possible to arrange tasks within our team to suit peoples’ preferences and to rotate to provide variety and interest.

Well-Typed has a variety of clients. For some we do proprietary Haskell development and consulting. For others, much of the work involves open-source development and cooperating with the rest of the Haskell community: the commercial, open-source and academic users.

About you

Our ideal candidate has excellent knowledge of Haskell, whether from industry, academia or personal interest. Familiarity with other languages, low-level programming and good software engineering practices are also useful. Good organisation and ability to manage your own time and reliably meet deadlines is important. You should also have good communication skills.

You are likely to have a bachelor’s degree or higher in computer science or a related field, although this isn’t a requirement.

Further (optional) bonus skills:

• experience in teaching Haskell or other technical topics,

• experience of consulting or running a business,

• experience with Cardano and/or Plutus,

• knowledge of and experience in applying formal methods,

• familiarity with (E)DSL design,

• knowledge of networking, concurrency and/or systems programming,

• experience with working on GHC,

• experience with web programming (in particular front-end),

• … (you tell us!)

Offer details

The offer is initially for one year full time, with the intention of a long term arrangement. Living in England is not required. We may be able to offer either employment or sub-contracting, depending on the jurisdiction in which you live. The salary range is 50k–90k GBP per year.

If you are interested, please apply by email to jobs@well-typed.com. Tell us why you are interested and why you would be a good fit for Well-Typed, and attach your CV. Please indicate how soon you might be able to start.

We are looking to fill at least one position as soon as possible, so please send in your application as soon as you can. That said, we expect to be continuously hiring over the next few months, and are willing to consider applications from expert Haskell developers at any time, so there is no firm application deadline.

by andres, duncan, adam, christine at November 28, 2022 12:00 AM

Whatever became of the Peanuts kids?

One day I asked Lorrie if she thought that Schroeder actually grew up to be a famous concert pianist. We agreed that he probably did. Or at least Schroeder has as good a chance as anyone does. To become a famous concert pianist, you need to have talent and drive. Schroeder clearly has talent (he can play all that Beethoven and Mozart on a toy piano whose black keys are only painted on) and he clearly has drive. Not everyone with talent and drive does succeed, of course, but he might make it, whereas some rando like me has no chance at all.

That led to a longer discussion about what became of the other kids. Some are easier than others. Who knows what happens to Violet, Sally, (non-Peppermint) Patty, and Shermy? I imagine Violet going into realty for some reason.

As a small child I did not understand that Lucy's “psychiatric help 5¢” lemonade stand was hilarious, or that she would have been the literally worst psychiatrist in the world. (Schultz must have known many psychiatrists; was Lucy inspired by any in particular?) Surely Lucy does not become an actual psychiatrist. The world is cruel and random, but I refuse to believe it is that cruel. My first thought for Lucy was that she was a lawyer, perhaps a litigator. Now I like to picture her as a union negotiator, and the continual despair of the management lawyers who have to deal with her.

Her brother Linus clearly becomes a university professor of philosophy, comparative religion, Middle-Eastern medieval literature, or something like that. Or does he drop out and work in a bookstore? No, I think he's the kind of person who can tolerate the grind of getting a graduate degree and workin his way into a tenured professorship, with a tan corduroy jacket with patches on the elbows, and maybe a pipe.

Peppermint Patty I can imagine as a high school gym teacher, or maybe a yoga instructor or massage therapist. I bet she'd be good at any of those. Or if we want to imagine her at the pinnacle of achievement, coach of the U.S. Olympic softball team. Marcie is calm and level-headed, but a follower. I imagine her as a highly competent project manager.

In the conversation with Lorrie, I said “But what happens to Charlie Brown?”

“You're kidding, right?” she asked.

“No, why?”

“To everyone's great surprise, Charlie Brown grows up to be a syndicated cartoonist and a millionaire philanthropist.”

Of course she was right. Charlie Brown is good ol' Charlie Schultz, whose immense success suprised everyone, and nobody more than himself.

Charles M. Schultz was born 100 years ago last Saturday.

by Mark Dominus (mjd@plover.com) at November 27, 2022 05:46 PM

Wombat coprolites

I was delighted to learn some time ago that there used to be giant wombats, six feet high at the shoulders, unfortunately long extinct.

It's also well known (and a minor mystery of Nature) that wombats have cubical poop.

Today I wondered, did the megafauna wombat produce cubical megaturds? And if so, would they fossilize (as turds often do) and leave ten-thousand-year-old mineral cubescat littering Australia? And if so, how big are these and where can I see them?

A look at Intestines of non-uniform stiffness mold the corners of wombat feces (Yang et al, Soft Matter, 2021, 17, 475–488) reveals a nice scatter plot of the dimensions of typical wombat scat, informing us that for (I think) the smooth-nosed (common) wombat:

• Length: 4.0 ± 0.6 cm
• Height: 2.3 ± 0.3 cm
• Width: 2.5 ± 0.3 cm

Notice though, not cubical! Clearly longer than they are thick. And I wonder how one distinguishes the width from the height of a wombat turd. Probably the paper explains, but the shitheads at Soft Matter want £42.50 plus tax to look at the paper. (I checked, and Alexandra was not able to give me a copy.)

Anyway the common wombat is about 40 cm long and 20 cm high, while the extinct giant wombats were nine or ten times as big: 400 cm long and 180 cm high, let's call it ten times. Then a propportional giant wombat scat would be a cuboid approximately 24 cm (9 in) wide and tall, and 40 cm (16 in) long. A giant wombat poop would be as long as… a wombat!

But not the imposing monoliths I had been hoping for.

Yang also wrote an article Duration of urination does not change with body size, something I have wondered about for a long time. I expected bladder size (and so urine quantity) to scale with the body volume, the cube of the body length. But the rate of urine flow should be proportional to the cross-sectional area of the urethra, only the square of the body length. So urination time should be roughly proportional to body size. Yang and her coauthors are decisive that this is not correct:

we discover that all mammals above 3 kg in weight empty their bladders over nearly constant duration of 21 ± 13 s.

What is wrong with my analysis above? It's complex and interesting:

This feat is possible, because larger animals have longer urethras and thus, higher gravitational force and higher flow speed. Smaller mammals are challenged during urination by high viscous and capillary forces that limit their urine to single drops. Our findings reveal that the urethra is a flow-enhancing device, enabling the urinary system to be scaled up by a factor of 3,600 in volume without compromising its function.

Wow. As Leslie Orgel said, evolution is cleverer than you are.

However, I disagree with the conclusion: 21±13 is not “nearly constant duration”. This is a range of 8–34s, with some mammals taking four times as long as others.

The appearance of the fibonacci numbers here is surely coincidental, but wouldn't it be awesome if it wasn't?

[ Addendum: I wondered if this was the only page on the web to contain the bigram “wombat coprolites”, but Google search produced this example from 2018:

Have wombats been around for enough eons that there might be wombat coprolites to make into jewelry? I have a small dinosaur coprolite that is kind of neat but I wouldn't make that turd into a necklace, it looks just like a piece of poop.

]

by Mark Dominus (mjd@plover.com) at November 26, 2022 03:43 PM

Black Friday Spotlight: Haskell Brain!

Machine learning is one of the most important skills in software today. The field has typically been dominated by languages like Python (through TensorFlow and PyTorch) and R. So it's a bit frustrating for Haskell fans who want to use this awesome language as widely as possible but struggle to apply it to this critical domain.

However, there are a few tools out there that allow us to use Haskell for machine learning! Chief among these are the Haskell Tensorflow bindings. They aren't easy to use though, and there aren't many tutorials either!

The Haskell Brain seeks to fill this gap. This course will walk you through all the important questions about getting started with Haskell and TensorFlow.

1. What system setup is required?
2. How are tensors represented in Haskell?
3. How can I train a machine learning model with tensors?

If you're ready to start answering these questions, head to the course sales page!

For more details about what's included in the course, including FAQ, head over to our course description page.

The best part of it is that for the next few days, you can get 20% off this course through our Black Friday sale! Just use the code BLACKFRIDAY22 and checkout. If you want an even better deal of 30% off, you can subscribe to our mailing list! You'll get a special code when you sign up. So don't miss out!

by James Bowen at November 26, 2022 03:30 PM

Black Friday Spotlight: Practical Haskell

How do you actually do something in Haskell? A programming language is only helpful if we can use it to solve real problems. Perhaps you've written up some neat and tidy solutions to small problems with Haskell. But does the language actually have the libraries and tools to build useful programs?

The answer to this question is a resounding Yes! Not only does Haskell have useful libraries for practical problems, but the "Haskell Approach" to these problems often has clear advantages! For instance, in Haskell you can:

1. Write database queries that are type-safe, interoperating seamlessly with well-defined Haskell types.
2. Define a web server where the API is clearly laid out and defined in terms of Haskell types.
3. Link your Haskell types to frontend types that will populate your Web UI
4. Organize "effects" within your system so that the capabilities of different functions are explicitly defined and known to your program at compile-time.
5. Use monads to describe a test case in plan language.

These ideas can supercharge your Haskell abilities! But they aren't necessarily easy to pick up. It takes a fair amount of commitment to learn them well enough to use in your own projects.

Luckily, Monday Morning Haskell has a great tool for you to learn these skills! Our Practical Haskell Course will teach you how to build a functional application that integrates systems like databases, web servers, frontend web pages, and behavioral tests.

If this sounds like exactly what you've been looking for to rapidly improve your Haskell, head to the course page to get started!

If you're curious for more details, head to our course description page to learn about what you can expect in the course.

Don't forget, you've got a couple more days to take advantage of our Black Friday Sale! You can use the code BlackFriday22 to get 20% off any of our courses, including Practical Haskell. If you subscribe to our mailing list, you can get an even better code for 30% off! So don't miss out on those savings!

by James Bowen at November 25, 2022 03:30 PM

Threads and messages with Rust and WebAssembly

On most systems, you can implement concurrency using either threads or processes, where the main difference between the two is that threads share memory and processes don’t. Modern web browsers support concurrency through the Web Workers API. Although Web Workers are by default closer to a multi-process model, when used with WebAssembly you can opt-in to a more thread-like experience. Just like in systems programming, the choice of threads vs. processes comes with various trade-offs and performance implications; I’ll be covering some of them in this post. These examples will be in Rust, but similar trade-offs should apply to other languages compiled to WASM.

The Web Workers API (multi-processing on the web)

When used from JavaScript, the Web Workers API is very simple: call new Worker("/path/to/worker.js") and your browser will fetch worker.js and start running it concurrently. Inter-worker communication works in a very JavaScripty way, by setting message handler callbacks and then sending messages. To use Web Workers from compiled WASM code, you’ll need to go “through” JavaScript: you need a little JavaScript glue for spawning the worker, and you need to do the message sending and callback handling using some JavaScript bindings. Here’s a little example that spawns a worker, sends a message, and gets a reply:

// Spawn a worker and communicate with it.
fn spawn_worker() {
  let worker = web_sys::Worker::new("./worker.js");
  let callback = wasm_bindgen::Closure<FnMut(web_sys::MessageEvent)>::new(|msg| {
    assert_eq!(msg.data.as_f64(), Some(2.0));
  }));
  // Set up a callback to be invoked whenever we receive a message from the worker.
  // .as_ref().unchecked_ref() turns a wasm_bindgen::Closure into a &js_sys::Function
  worker.set_onmessage(callback.as_ref().unchecked_ref());

  // Send a message to the worker.
  worker.post_message(&JsValue::from(1.0)).expect("failed to post");

  // Did you notice that `set_onmessage` took a borrow? We still own `callback`, and we'd
  // better not free it too soon! See also
  // https://rustwasm.github.io/wasm-bindgen/reference/weak-references.html
  std::mem::forget(callback); // FIXME: memory management is hard
}

// An entry point for the JavaScript worker to call back into WASM.
#[wasm_bindgen]
pub fn worker_entry_point(arg: i32) {
  // Add 1 to our argument and send it back to the main thread.
  // Yeah, the js_sys/web_sys bindings are ... low-level.
  js_sys::global()
    .dyn_into::<web_sys::DedicatedWorkerGlobalScope>()
    .unwrap()
    .post_message(&JsValue::from(arg + 1))
    .unwrap();
}

And here’s the JavaScript glue code in worker.js, which receives messages and calls worker_entry_point:

importScripts("./path/to/wasm_bindgen/module.js")
self.onmessage = async event => {
  const { child_entry_point } = await wasm_bindgen(
    "./path/to/wasm_bindgen/module_bg.wasm"
  )
  worker_entry_point(Number(event.data))
}

Note that when using the Web Workers API, all of the messages you send are JsValues. This is fine for sending primitive types, but it becomes annoying if you want to send structured types, which must be converted into JsValues and back. You can simplify this process by using a helper crate like gloo-worker, which provides a convenient way to send structured data between workers. Under the hood, it serializes and deserializes data to and from a js_sys::ArrayBuffer.

Dealing with large data can also be tricky, because post_message requires that you copy the data. To avoid large data copies, you can use a SharedArrayBuffer (a buffer that can be accessed by multiple workers) or the post_message_with_transfer function, which allows for transferring the ownership of certain JavaScript objects from one worker to another without copying. The downside of this workaround is that it doesn’t work directly with objects living in WASM memory. For example, if you have a Vec<u8> that you want to send to another worker, you’ll need to either copy it to an ArrayBuffer and transfer it, or copy it to a SharedArrayBuffer and share it.

Shared memory in WebAssembly (multi-threading on the web)

Workers that share an address space can communicate with less boilerplate and minimal data-copying. To create shared memory workers, note that wasm_bindgen’s auto-generated initialization function takes a second (optional) parameter: a WASM memory object for the module to use. Memory chunks can be shared between WASM modules, so we can instantiate a new module using the same memory as the first one, and the two modules will share it.

Having two WASM workers sharing the same memory opens the door to more expressive inter-worker communication. For example, we can easily write a function for executing a closure in another worker, just like how the std::thread::spawn function works. The trick is to create a closure and send its address to the other worker. Since the memory space is shared, the receiving worker can cast that address back into a closure and execute it.

// A function imitating `std::thread::spawn`.
pub fn spawn(f: impl FnOnce() + Send + 'static) -> Result<web_sys::Worker, JsValue> {
  let worker = web_sys::Worker::new("./worker.js")?;
  // Double-boxing because `dyn FnOnce` is unsized and so `Box<dyn FnOnce()>` is a fat pointer.
  // But `Box<Box<dyn FnOnce()>>` is just a plain pointer, and since wasm has 32-bit pointers,
  // we can cast it to a `u32` and back.
  let ptr = Box::into_raw(Box::new(Box::new(f) as Box<dyn FnOnce()>));
  let msg = js_sys::Array::new();
  // Send the worker a reference to our memory chunk, so it can initialize a wasm module
  // using the same memory.
  msg.push(&wasm_bindgen::memory());
  // Also send the worker the address of the closure we want to execute.
  msg.push(&JsValue::from(ptr as u32))
  worker.post_message(&msg);
}

#[wasm_bindgen]
// This function is here for `worker.js` to call.
pub fn worker_entry_point(addr: u32) {
  // Interpret the address we were given as a pointer to a closure to call.
  let closure = unsafe { Box::from_raw(ptr as *mut Box<dyn FnOnce()>) };
  (*closure)();
}

The JavaScript worker glue must be changed slightly, to use the received memory chunk when initializing its WASM module.

importScripts("./path/to/wasm_bindgen/module.js")
self.onmessage = async event => {
  // event.data[0] should be the Memory object, and event.data[1] is the value to pass into child_entry_point
  const { child_entry_point } = await wasm_bindgen(
    "./path/to/wasm_bindgen/module_bg.wasm",
    event.data[0]
  )
  child_entry_point(Number(event.data[1]))
}

And now we can spawn closures on another thread just like in native multi-threaded code, using the spawn function above instead of std::thread::spawn. You can even use Rust’s native inter-thread communication tools, like std::sync::mpsc, to transfer data between threads without copying! Our first worker example becomes as simple as:

let (to_worker, from_main) = std::sync::mpsc::channel();
let (to_main, from_worker) = std::sync::mpsc::channel();
spawn(move || { to_main.send(from_main.recv().unwrap() + 1.0); });
to_worker.send(1.0);
assert_eq!(from_worker.recv().unwrap(), 2.0);

Ok, there are some caveats. Shared memory WASM modules need some features that weren’t in the first iteration of the WASM spec, so you’ll need to build with some extra [target-features][targer-features]. You’ll also need to rebuild the standard library with those features, which requires a nightly compiler and unstable flags. Something like this will do the trick:

RUSTFLAGS="-C target-feature=+atomics,+bulk-memory,+mutable-globals" cargo build --target=wasm32-unknown-unknown --release -Z build-std=panic_abort,std

And then you’ll need to configure your web server with some special headers, because shared WASM memory builds on SharedArrayBuffer.

But there’s a more serious issue with shared-memory workers: our example called from_worker.recv() in the main thread, and most browsers will throw an exception if you try to block the main thread, even for a very short time. Since Rust doesn’t have any tooling for checking non-blockingness (see here for some discussion), this might be difficult to ensure.

If the extra discipline is just too onerous or unreliable, you can guarantee a non-blocked main thread by moving all shared-memory WASM modules off of it: from the main thread, use the JavaScript message-passing methods to communicate with one or more workers, which are free to communicate amongst each other using whichever (possibly blocking) methods they want.

How much does all of this actually matter?

To measure the performance implications of the various options, I made some buffers and sent them back and forth repeatedly between workers while measuring the round-trip time. I repeated the experiment with two different buffer sizes (a large 20 MB buffer, and a small 16 B one) and three different message-passing methods. The timings were done on Firefox 101, and the code is available here.

	20MB buffer	16B buffer
post_message	28ms	0.028ms
post_message_with_transfer	0.033ms	0.033ms
std::sync::mpsc::channel	0.0062ms	0.0062ms

You’ll notice that Rust-native shared memory is the fastest by a substantial factor but not a very large absolute amount, unless you really need to send a lot of messages. Between the JavaScript methods, post_message_with_transfer has some small overhead compared to post_message for small buffers, but this is dwarfed by the copying time if you have substantial data to send.

At Tweag, we’ve been working with a client on an optimized WASM library that caches and doles out largish (around 20MB each) chunks of data. We tried various different threading architectures and ended up making do without shared memory. Our heavy use of non-lock-free primitives made it hard to keep the main browser thread happy when using shared memory, while the hybrid architecture depicted above forced us into too many expensive copies (we couldn’t just transfer the data to the main thread because we needed a copy in cache). With a separate-memory architecture, we arranged our data processing so that large buffers are only ever transferred, never copied. And the small overhead of post_message_with_transfer was negligible compared to the other processing we were doing.

Your ideal architecture might be different from ours. By explaining some of the trade-offs involved, I hope this post will help you find it!

November 24, 2022 12:00 AM

Announcing a live tutorial on eventlog2html and ghc-debug

We are happy to announce that we will be live-streaming a free tutorial on Haskell debugging tools via YouTube:

Profiling Memory Usage With eventlog2html and ghc-debug

Finley McIlwaine, 2022-12-01, 1900–2100 GMT

Understanding and analysing the memory usage of Haskell programs is a notoriously difficult yet important problem. Recent improvements to GHC’s profiling capabilities, along with better tooling, has made it much easier to deeply and precisely analyse the memory usage characteristics of even large Haskell programs.

This workshop aims to present two such tools that allow high and low level memory usage analysis of Haskell programs: eventlog2html and ghc-debug. We will learn how to set up and use eventlog2html to generate high-level visuals and statistics of our program’s execution. We will also learn how to set up and use ghc-debug to precisely and programmatically explore our program’s low-level memory usage profile.

We will examine these tools by using them on several pre-prepared Haskell programs. The workshop aims to be beneficial to Haskell programmers of all levels. Beginner Haskell programmers can expect to gain a deeper understanding of lazy evaluation and the impacts it can have on program performance. Experienced Haskell programmers can expect to gain an understanding of exactly what these tools have to offer and the skills necessary to use these tools on their own Haskell programs.

This is a re-run of a similar workshop Finley presented at MuniHac 2022, which unfortunately was not recorded.

We hope that many of you will join us next Thursday for this stream! There will be an option to ask questions during the presentation via the YouTube chat. There is no need to register.

by finley, andres at November 23, 2022 12:00 AM

Graphs, Kites and Darts

Graphs, Kites and Darts

Non-periodic tilings with Penrose’s kites and darts

We continue our investigation of the tilings using Haskell with Haskell Diagrams. What is new is the introduction of a planar graph representation. This allows us to define more operations on finite tilings, in particular forcing and composing.

Previously in Diagrams for Penrose Tiles we implemented tools to create and draw finite patches of Penrose kites and darts (such as the samples depicted in figure 1). The code for this and for the new graph representation and tools described here can be found on GitHub https://github.com/chrisreade/PenroseKiteDart.

To describe the tiling operations it is convenient to work with the half-tiles: LD (left dart), RD (right dart), LK (left kite), RK (right kite) using a polymorphic type HalfTile (defined in a module HalfTile)

data HalfTile rep 
 = LD rep | RD rep | LK rep | RK rep   deriving (Show,Eq)

Here rep is a type variable for a representation to be chosen. For drawing purposes, we chose two-dimensional vectors (V2 Double) and called these Pieces.

type Piece = HalfTile (V2 Double)

The vector represents the join edge of the half tile (see figure 2) and thus the scale and orientation are determined (the other tile edges are derived from this when producing a diagram).

Finite tilings or patches are then lists of located pieces.

type Patch = [Located Piece]

Both Piece and Patch are made transformable so rotate, and scale can be applied to both and translate can be applied to a Patch. (Translate has no effect on a Piece unless it is located.)

In Diagrams for Penrose Tiles we also discussed the rules for legal tilings and specifically the problem of incorrect tilings which are legal but get stuck so cannot continue to infinity. In order to create correct tilings we implemented the decompose operation on patches.

The vector representation that we use for drawing is not well suited to exploring properties of a patch such as neighbours of pieces. Knowing about neighbouring tiles is important for being able to reason about composition of patches (inverting a decomposition) and to find which pieces are determined (forced) on the boundary of a patch.

However, the polymorphic type HalfTile allows us to introduce our alternative graph representation alongside Pieces.

Tile Graphs

In the module Tgraph.Prelude, we have the new representation which treats half tiles as triangular faces of a planar graph – a TileFace – by specialising HalfTile with a triple of vertices (clockwise starting with the tile origin). For example

LD (1,3,4)       RK (6,4,3)

type Vertex = Int
type TileFace = HalfTile (Vertex,Vertex,Vertex)

When we need to refer to particular vertices from a TileFace we use originV (the first vertex – red dot in figure 2), oppV (the vertex at the opposite end of the join edge – dashed edge in figure 2), wingV (the remaining vertex not on the join edge).

originV, oppV, wingV :: TileFace -> Vertex

Tgraphs

The Tile Graphs implementation uses a type Tgraph which has a list of tile faces and a maximum vertex number.

data Tgraph = Tgraph { maxV  :: Vertex
                     , faces :: [TileFace]
                     }  deriving (Show)

For example, fool (short for a fool’s kite) is a Tgraph with 6 faces and 7 vertices, shown in figure 3.

fool = Tgraph { maxV = 7
               , faces = [RD (1,2,3),LD (1,3,4),RK (6,2,5)
                         ,LK (6,3,2),RK (6,4,3),LK (6,7,4)
                         ]
              }

(The fool is also called an ace in the literature)

With this representation we can investigate how composition works with whole patches. Figure 4 shows a twice decomposed sun on the left and a once decomposed sun on the right (both with vertex labels). In addition to decomposing the right graph to form the left graph, we can also compose the left graph to get the right graph.

After implementing composition, we also explore a force operation and an emplace operation to extend tilings.

There are some constraints we impose on Tgraphs.

• No spurious vertices. The vertices of a Tgraph are the vertices that occur in the faces of the Tgraph (and maxV is the largest number occurring).
• Connected. The collection of faces must be a single connected component.
• No crossing boundaries. By this we mean that vertices on the boundary are incident with exactly two boundary edges. The boundary consists of the edges between the Tgraph faces and exterior region(s). This is important for adding faces.
• Tile connected. Roughly, this means that if we collect the faces of a Tgraph by starting from any single face and then add faces which share an edge with those already collected, we get all the Tgraph faces. This is important for drawing purposes.

In fact, if a Tgraph is connected with no crossing boundaries, then it must be tile connected. (We could define tile connected to mean that the dual graph excluding exterior regions is connected.)

Figure 5 shows two excluded graphs which have crossing boundaries at 4 (left graph) and 13 (right graph). The left graph is still tile connected but the right is not tile connected (the two faces at the top right do not have an edge in common with the rest of the faces.)

Although we have allowed for Tgraphs with holes (multiple exterior regions), we note that such holes cannot be created by adding faces one at a time without creating a crossing boundary. They can be created by removing faces from a Tgraph without necessarily creating a crossing boundary.

Important We are using face as an abbreviation for half-tile face of a Tgraph here, and we do not count the exterior of a patch of faces to be a face. The exterior can also be disconnected when we have holes in a patch of faces and the holes are not counted as faces either. In graph theory, the term face would generally include these other regions, but we will call them exterior regions rather than faces.

In addition to the constructor Tgraph we also use

checkedTgraph:: [TileFace] -> Tgraph

which creates a Tgraph from a list of faces, but also performs checks on the required properties of Tgraphs. We can then remove or select faces from a Tgraph and then use checkedTgraph to ensure the resulting Tgraph still satisfies the required properties.

selectFaces, removeFaces  :: [TileFace] -> Tgraph -> Tgraph
selectFaces fcs g = checkedTgraph (faces g `intersect` fcs)
removeFaces fcs g = checkedTgraph (faces g \\ fcs)

Edges and Directed Edges

We do not explicitly record edges as part of a Tgraph, but calculate them as needed. Implicitly we are requiring

• No spurious edges. The edges of a Tgraph are the edges of the faces of the Tgraph.

To represent edges, a pair of vertices (a,b) is regarded as a directed edge from a to b. A list of such pairs will usually be regarded as a directed edge list. In the special case that the list is symmetrically closed [(b,a) is in the list whenever (a,b) is in the list] we will refer to this as an edge list rather than a directed edge list.

The following functions on TileFaces all produce directed edges (going clockwise round a face).

type Dedge = (Vertex,Vertex)
  -- join edge - dashed in figure 2
joinE  :: TileFace -> Dedge 
  -- the short edge which is not a join edge
shortE :: TileFace -> Dedge   
-- the long edge which is not a join edge
longE  :: TileFace -> Dedge
  -- all three directed edges clockwise from origin
faceDedges :: TileFace -> [Dedge]

For the whole Tgraph, we often want a list of all the directed edges of all the faces.

graphDedges :: Tgraph -> [Dedge]
graphDedges g = concatMap faceDedges (faces g)

Because our graphs represent tilings they are planar (can be embedded in a plane) so we know that at most two faces can share an edge and they will have opposite directions of the edge. No two faces can have the same directed edge. So from graphDedges g we can easily calculate internal edges (edges shared by 2 faces) and boundary directed edges (directed edges round the external regions).

internalEdges, boundaryDedges :: Tgraph -> [Dedge]

The internal edges of g are those edges which occur in both directions in graphDedges g. The boundary directed edges of g are the missing reverse directions in graphDedges g.

We also refer to all the long edges of a Tgraph (including kite join edges) as phiEdges (both directions of these edges).

phiEdges :: Tgraph -> [Dedge]

This is so named because, when drawn, these long edges are phi times the length of the short edges (phi being the golden ratio which is approximately 1.618).

Drawing Tgraphs (Patches and VPinned)

The module Tgraph.Convert contains functions to convert a Tgraph to our previous vector representation (Patch) defined in TileLib so we can use the existing tools to produce diagrams.

makePatch :: Tgraph -> Patch

drawPatch :: Patch -> Diagram B -- defined in module TileLib

drawGraph :: Tgraph -> Diagram B
drawGraph = drawPatch . makePatch

However, it is also useful to have an intermediate stage (a VPinned) which contains both faces and locations for each vertex. This allows vertex labels to be drawn and for faces to be identified and retained/excluded after the location information is calculated.

data VPinned  = VPinned {vLocs :: VertexLocMap
                        ,vpFaces :: [TileFace]
                        }

A VPinned has a map from vertices to locations and a list of faces. We make VPinned transformable so it can also be an argument type for rotate, translate, and scale.

The conversion functions include

makeVPinned   :: Tgraph -> VPinned
dropLabels :: VPinned -> Patch -- discards vertex information
drawVPinned   :: VPinned -> Diagram B  -- draws labels as well

drawVGraph   :: Tgraph -> Diagram B
drawVGraph = drawVPinned . makeVPinned

One consequence of using abstract graphs is that there is no unique predefined way to orient or scale or position the patch arising from a graph representation. Our implementation selects a particular join edge and aligns it along the x-axis (unit length for a dart, philength for a kite) and tile-connectedness ensures the rest of the patch can be calculated from this.

We also have functions to re-orient a VPinned and lists of VPinneds using chosen pairs of vertices. [Simply doing rotations on the final diagrams can cause problems if these include vertex labels. We do not, in general, want to rotate the labels – so we need to orient the VPinned before converting to a diagram]

Decomposing Graphs

We previously implemented decomposition for patches which splits each half-tile into two or three smaller scale half-tiles.

decompose :: Patch -> Patch

We now have a Tgraph version of decomposition in the module Tgraphs:

decomposeG :: Tgraph -> Tgraph

Graph decomposition is particularly simple. We start by introducing one new vertex for each long edge (the phiEdges) of the Tgraph. We then build the new faces from each old face using the new vertices.

As a running example we take fool (mentioned above) and its decomposition foolD

*Main> foolD = decomposeG fool

*Main> foolD
Tgraph { maxV = 14
       , faces = [LK (1,8,3),RD (2,3,8),RK (1,3,9)
                 ,LD (4,9,3),RK (5,13,2),LK (5,10,13)
                 ,RD (6,13,10),LK (3,2,13),RK (3,13,11)
                 ,LD (6,11,13),RK (3,14,4),LK (3,11,14)
                 ,RD (6,14,11),LK (7,4,14),RK (7,14,12)
                 ,LD (6,12,14)
                 ]
       }

which are best seen together (fool followed by foolD) in figure 6.

Composing graphs, and Unknowns

Composing is meant to be an inverse to decomposing, and one of the main reasons for introducing our graph representation. In the literature, decomposition and composition are defined for infinite tilings and in that context they are unique inverses to each other. For finite patches, however, we will see that composition is not always uniquely determined.

In figure 7 (Two Levels) we have emphasised the larger scale faces on top of the smaller scale faces.

How do we identify the composed tiles? We start by classifying vertices which are at the wing tips of the (smaller) darts as these determine how things compose. In the interior of a graph/patch (e.g in figure 7), a dart wing tip always coincides with a second dart wing tip, and either

1. the 2 dart halves share a long edge. The shared wing tip is then classified as a largeKiteCentre and is at the centre of a larger kite. (See left vertex type in figure 8), or
2. the 2 dart halves touch at their wing tips without sharing an edge. This shared wing tip is classified as a largeDartBase and is the base of a larger dart. (See right vertex type in figure 8)

[We also call these (respectively) a deuce vertex type and a jack vertex type later in figure 10]

Around the boundary of a graph, the dart wing tips may not share with a second dart. Sometimes the wing tip has to be classified as unknown but often it can be decided by looking at neighbouring tiles. In this example of a four times decomposed sun (sunD4), it is possible to classify all the dart wing tips as largeKiteCentres or largeDartBases so there are no unknowns.

If there are no unknowns, then we have a function to produce the unique composed graph.

composeG:: Tgraph -> Tgraph

Any correct decomposed graph without unknowns will necessarily compose back to its original. This makes composeG a left inverse to decomposeG provided there are no unknowns.

For example, with an (n times) decomposed sun we will have no unknowns, so these will all compose back up to a sun after n applications of composeG. For n=4 (sunD4 – the smaller scale shown in figure 7) the dart wing classification returns 70 largeKiteCentres, 45 largeDartBases, and no unknowns.

Similarly with the simpler foolD example, if we classsify the dart wings we get

largeKiteCentres = [14,13]
largeDartBases = [3]
unknowns = []

In foolD (the right hand graph in figure 6), nodes 14 and 13 are new kite centres and node 3 is a new dart base. There are no unknowns so we can use composeG safely

*Main> composeG foolD
Tgraph { maxV = 7
       , faces = [RD (1,2,3),LD (1,3,4),RK (6,2,5)
                 ,RK (6,4,3),LK (6,3,2),LK (6,7,4)
                 ]
       }

which reproduces the original fool (left hand graph in figure 6).

However, if we now check out unknowns for fool we get

largeKiteCentres = []
largeDartBases = []
unknowns = [4,2]    

So both nodes 2 and 4 are unknowns. It had looked as though fool would simply compose into two half kites back-to-back (sharing their long edge not their join), but the unknowns show there are other possible choices. Each unknown could become a largeKiteCentre or a largeDartBase.

The question is then what to do with unknowns.

Partial Compositions

In fact our composeG resolves two problems when dealing with finite patches. One is the unknowns and the other is critical missing faces needed to make up a new face (e.g the absence of any half dart).

It is implemented using an intermediary function for partial composition

partCompose:: Tgraph -> ([TileFace],Tgraph) 

partCompose will compose everything that is uniquely determined, but will leave out faces round the boundary which cannot be determined or cannot be included in a new face. It returns the faces of the argument graph that were not used, along with the composed graph.

Figure 9 shows the result of partCompose applied to two graphs. [These are force kiteD3 and force dartD3 on the left. Force is described later]. In each case, the excluded faces of the starting graph are shown in pale green, overlaid by the composed graph on the right.

Then composeG is simply defined to keep the composed faces and ignore the unused faces produced by partCompose.

composeG:: Tgraph -> Tgraph
composeG = snd . partCompose 

This approach avoids making a decision about unknowns when composing, but it may lose some information by throwing away the uncomposed faces.

For correct Tgraphs g, if decomposeG g has no unknowns, then composeG is a left inverse to decomposeG. However, if we take g to be two kite halves sharing their long edge (not their join edge), then these decompose to fool which produces an empty graph when recomposed. Thus we do not have g = composeG (decomposeG g) in general. On the other hand we do have g = composeG (decomposeG g) for correct whole-tile Tgraphs g (whole-tile means all half-tiles of g have their matching half-tile on their join edge in g)

Later (figure 21) we show another exception to g = composeG(decomposeG g) with an incorrect tiling.

We make use of

selectFacesVP    :: [TileFace] -> VPinned -> VPinned
removeFacesVP    :: [TileFace] -> VPinned -> VPinned
selectFacesGtoVP :: [TileFace] -> Tgraph -> VPinned
removeFacesGtoVP :: [TileFace] -> Tgraph -> VPinned

for creating VPinneds from selected tile faces of a Tgraph or VPinned. This allows us to represent and draw a subgraph which need not be connected nor satisfy the no crossing boundaries property provided the Tgraph it was derived from had these properties.

Forcing

When building up a tiling, following the rules, there is often no choice about what tile can be added alongside certain tile edges at the boundary. Such additions are forced by the existing patch of tiles and the rules. For example, if a half tile has its join edge on the boundary, the unique mirror half tile is the only possibility for adding a face to that edge. Similarly, the short edge of a left (respectively, right) dart can only be matched with the short edge of a right (respectively, left) kite. We also make use of the fact that only 7 types of vertex can appear in (the interior of) a patch, so on a boundary vertex we sometimes have enough of the faces to determine the vertex type. These are given the following names in the literature (shown in figure 10): sun, star, jack (=largeDartBase), queen, king, ace, deuce (=largeKiteCentre).

The function

force :: Tgraph -> Tgraph

will add some faces on the boundary that are forced (i.e new faces where there is exactly one possible choice). For example:

• When a join edge is on the boundary – add the missing half tile to make a whole tile.
• When a half dart has its short edge on the boundary – add the half kite that must be on the short edge.
• When a vertex is both a dart origin and a kite wing (it must be a queen or king vertex) – if there is a boundary short edge of a kite half at the vertex, add another kite half sharing the short edge, (this converts 1 kite to 2 and 3 kites to 4 in combination with the first rule).
• When two half kites share a short edge their common oppV vertex must be a deuce vertex – add any missing half darts needed to complete the vertex.
• …

Figure 11 shows foolDminus (which is foolD with 3 faces removed) on the left and the result of forcing, ie force foolDminus on the right which is the same graph we get from force foolD.

foolDminus = 
    removeFaces [RD(6,14,11), LD(6,12,14), RK(5,13,2)] foolD

Figures 12, 13 and 14 illustrate the result of forcing a 5-times decomposed kite, a 5-times decomposed dart, and a 5-times decomposed sun (respectively). The first two figures reproduce diagrams from an article by Roger Penrose illustrating the extent of influence of tiles round a decomposed kite and dart. [Penrose R Tilings and quasi-crystals; a non-local growth problem? in Aperiodicity and Order 2, edited by Jarich M, Academic Press, 1989. (fig 14)].

In figure 15, the bottom row shows successive decompositions of a dart (dashed blue arrows from right to left), so applying composeG to each dart will go back (green arrows from left to right). The black vertical arrows are force. The solid blue arrows from right to left are (force . decomposeG) being applied to the successive forced graphs. The green arrows in the reverse direction are composeG again and the intermediate (partCompose) figures are shown in the top row with the ignored faces in pale green.

Figure 16 shows the forced graphs of the seven vertex types (with the starting graphs in red) along with a kite (top right).

These are related to each other as shown in the columns. Each graph composes to the one above (an empty graph for the ones in the top row) and the graph below is its forced decomposition. [The rows have been scaled differently to make the vertex types easier to see.]

Adding Faces to a Tgraph

This is technically tricky because we need to discover what vertices (and implicitly edges) need to be newly created and which ones already exist in the Tgraph. This goes beyond a simple graph operation and requires use of the geometry of the faces. We have chosen not to do a full conversion to vectors to work out all the geometry, but instead we introduce a local representation of angles at a vertex allowing a simple equality test.

Integer Angles

All vertex angles are integer multiples of 1/10th turn (mod 10) so we use these integers for face internal angles and boundary external angles. The face adding process always adds to the right of a given directed edge (a,b) which must be a boundary directed edge. [Adding to the left of an edge (a,b) would mean that (b,a) will be the boundary direction and so we are really adding to the right of (b,a)]. Face adding looks to see if either of the two other edges already exist in the graph by considering the end points a and b to which the new face is to be added, and checking angles.

This allows an edge in a particular sought direction to be discovered. If it is not found it is assumed not to exist. However, this will be undermined if there are crossing boundaries . In this case there must be more than two boundary directed edges at the vertex and there is no unique external angle.

Establishing the no crossing boundaries property ensures these failures cannot occur. We can easily check this property for newly created graphs (with checkedTgraph) and the face adding operations cannot create crossing boundaries.

Touching Vertices and Crossing Boundaries

When a new face to be added on (a,b) has neither of the other two edges already in the graph, the third vertex needs to be created. However it could already exist in the Tgraph – it is not on an edge coming from a or b but from another non-local part of the Tgraph. We call this a touching vertex. If we simply added a new vertex without checking for a clash this would create a nonsense graph. However, if we do check and find an existing vertex, we still cannot add the face using this because it would create a crossing boundary.

Our version of forcing prevents face additions that would create a touching vertex/crossing boundary by calculating the positions of boundary vertices.

No conflicting edges

There is a final (simple) check when adding a new face, to prevent a long edge (phiEdge) sharing with a short edge. This can arise if we force an incorrect graph (as we will see later).

Implementing Forcing

Our order of forcing prioritises updates (face additions) which do not introduce a new vertex. Such safe updates are easy to recognise and they do not require a touching vertex check. Surprisingly, this pretty much removes the problem of touching vertices altogether.

As an illustration, consider foolDMinus again on the left of figure 11. Adding the left dart onto edge (12,14) is not a safe addition (and would create a crossing boundary at 6). However, adding the right dart RD(6,14,11) is safe and creates the new edge (6,14) which then makes the left dart addition safe. In fact it takes some contrivance to come up with a Tgraph with an update that could fail the check during forcing when safe cases are always done first. Figure 17 shows such a contrived Tgraph formed by removing the faces shown in green from a twice decomposed sun on the left. The forced result is shown on the right. When there are no safe cases, we need to try an unsafe one. The four green faces at the bottom are blocked by the touching vertex check. This leaves any one of 9 half-kites at the centre which would pass the check. But after just one of these is added, the check is not needed again. There is always a safe addition to be done at each step until all the green faces are added.

Boundary information

The implementation of forcing has been made more efficient by calculating some boundary information in advance. This boundary information uses a type Boundary

data Boundary 
  = Boundary
    { bDedges     :: [Dedge]
    , bvFacesMap  :: Mapping Vertex [TileFace]
    , bvLocMap    :: Mapping Vertex (Point V2 Double)
    , allFaces    :: [TileFace]
    , allVertices :: [Vertex]
    , nextVertex  :: Vertex
    } deriving (Show)

This records the boundary directed edges (bDedges) plus a mapping of the boundary vertices to their incident faces (bvFacesMap) plus a mapping of the boundary vertices to their positions (bvLocMap). It also keeps track of all the faces and vertices. The boundary information is easily incremented for each face addition without being recalculated from scratch, and a final graph with all the new faces is easily recovered from the boundary information when there are no more updates.

makeBoundary  :: Tgraph -> Boundary
recoverGraph  :: Boundary -> Tgraph

The saving that comes from using boundaries lies in efficient incremental changes to boundary information and, of course, in avoiding the need to consider internal faces. As a further optimisation we keep track of updates in a mapping from boundary directed edges to updates, and supply a list of affected edges after an update so the update calculator (update generator) need only revise these. The boundary and mapping are combined in a force state.

type UpdateMap = Mapping Dedge Update
type UpdateGenerator = Boundary -> [Dedge] -> UpdateMap
data ForceState = ForceState 
       { boundaryState:: Boundary
       , updateMap:: UpdateMap 
       }

Forcing then involves using a specific update generator (allUGenerator) and initialising the state, then using the recursive forceAll which keeps doing updates until there are no more, before recovering the final graph.

force:: Tgraph -> Tgraph
force = forceWith allUGenerator

forceWith:: UpdateGenerator -> Tgraph -> Tgraph
forceWith uGen = recoverGraph . boundaryState . 
                 forceAll uGen . initForceState uGen

forceAll :: UpdateGenerator -> ForceState -> ForceState
initForceState :: UpdateGenerator -> Tgraph -> ForceState

In addition to force we can easily define

wholeTiles:: Tgraph -> Tgraph
wholeTiles = forceWith wholeTileUpdates 

which just uses the first forcing rule to make sure every half-tile has a matching other half.

We also have a version of force which counts to a specific number of face additions.

stepForce :: Int -> ForceState -> ForceState

This proved essential in uncovering problems of accumulated innaccuracy in calculating boundary positions (now fixed).

Some Other Experiments

Below we describe results of some experiments using the tools introduced above. Specifically: emplacements, sub-Tgraphs, incorrect tilings, and composition choices.

Emplacements

The finite number of rules used in forcing are based on local boundary vertex and edge information only. We may be able to improve on this by considering a composition and forcing at the next level up before decomposing and forcing again. This thus considers slightly broader local information. In fact we can iterate this process to all the higher levels of composition. Some graphs produce an empty graph when composed so we can regard those as maximal compositions. For example composeG fool produces an empty graph.

The idea now is to take an arbitrary graph and apply (composeG . force) repeatedly to find its maximally composed graph, then to force the maximal graph before applying (force . decomposeG) repeatedly back down to the starting level (so the same number of decompositions as compositions).

We call the function emplace, and call the result the emplacement of the starting graph as it shows a region of influence around the starting graph.

With earlier versions of forcing when we had fewer rules, emplace g often extended force g for a Tgraph g. This allowed the identification of some new rules. Since adding the new rules we have not yet found graphs with different results from force and emplace. [Update: We now have an example where force includes more than emplace].

Sub-Tgraphs

In figure 18 on the left we have a four times decomposed dart dartD4 followed by two sub-Tgraphs brokenDart and badlyBrokenDart which are constructed by removing faces from dartD4 (but retaining the connectedness condition and the no crossing boundaries condition). These all produce the same forced result (depicted middle row left in figure 15).

However, if we do compositions without forcing first we find badlyBrokenDart fails because it produces a graph with crossing boundaries after 3 compositions. So composeG on its own is not always safe, where safe means guaranteed to produce a valid Tgraph from a valid correct Tgraph.

In other experiments we tried force on Tgraphs with holes and on incomplete boundaries around a potential hole. For example, we have taken the boundary faces of a forced, 5 times decomposed dart, then removed a few more faces to make a gap (which is still a valid Tgraph). This is shown at the top in figure 19. The result of forcing reconstructs the complete original forced graph. The bottom figure shows an intermediate stage after 2200 face additions. The gap cannot be closed off to make a hole as this would create a crossing boundary, but the channel does get filled and eventually closes the gap without creating a hole.

Incorrect Tilings

When we say a Tgraph g is a correct graph (respectively: incorrect graph), we mean g represents a correct tiling (respectively: incorrect tiling). A simple example of an incorrect graph is a kite with a dart on each side (called a mistake by Penrose) shown on the left of figure 20.

*Main> mistake
Tgraph { vertices = [1,2,4,3,5,6,7,8]
       , faces = [RK (1,2,4),LK (1,3,2),RD (3,1,5)
                 ,LD (4,6,1),LD (3,5,7),RD (4,8,6)
                 ]
       }

If we try to force (or emplace) this graph it produces an error in construction which is detected by the test for conflicting edge types (a phiEdge sharing with a non-phiEdge).

*Main> force mistake
Tgraph {vertices = *** Exception: doUpdate:(incorrect tiling)
Conflicting new face RK (11,1,6)
with neighbouring faces
[RK (9,1,11),LK (9,5,1),RK (1,2,4),LK (1,3,2),RD (3,1,5),LD (4,6,1),RD (4,8,6)]
in boundary
Boundary ...

In figure 20 on the right, we see that after successfully constructing the two whole kites on the top dart short edges, there is an attempt to add an RK on edge (1,6). The process finds an existing edge (1,11) in the correct direction for one of the new edges so tries to add the erroneous RK (11,1,6) which fails a noConflicts test.

So it is certainly true that incorrect graphs may fail on forcing, but forcing cannot create an incorrect graph from a correct graph.

If we apply decomposeG to mistake it produces another incorrect graph (which is similarly detected if we apply force), but will nevertheless still compose back to mistake if we do not try to force.

Interestingly, though, the incorrectness of a graph is not always preserved by decomposeG. If we start with mistake1 which is mistake with just two of the half darts (and also an incorrect tiling) we still get a similar failure on forcing, but decomposeG mistake1 is no longer incorrect. If we apply composeG to the result or force then composeG the mistake is thrown away to leave just a kite (see figure 21). This is an example where composeG is not a left inverse to either decomposeG or (force . decomposeG).

Composing with Choices

We know that unknowns indicate possible choices (although some choices may lead to incorrect graphs). As an experiment we introduce

makeChoices :: Tgraph -> [Tgraph]

which produces alternatives for the 2 choices of each of unknowns (prior to composing). This uses forceLDB which forces an unknown to be a largeDartBase by adding an appropriate joined half dart at the node, and forceLKC which forces an unknown to be a largeKiteCentre by adding a half dart and a whole kite at the node (making up the 3 pieces for a larger half kite).

Figure 22 illustrates the four choices for composing fool this way. The top row has the four choices of makeChoices fool (with the fool shown embeded in red in each case). The bottom row shows the result of applying composeG to each choice.

In this case, all four compositions are correct tilings. The problem is that, in general, some of the choices may lead to incorrect tilings. More specifically, a choice of one unknown can determine what other unknowns have to become with constraints such as

• a and b have to be opposite choices
• a and b have to be the same choice
• a and b cannot both be largeKiteCentres
• a and b cannot both be largeDartBases

This analysis of constraints on unknowns is not trivial. The potential exponential results from choices suggests we should compose and force as much as possible and only consider unknowns of a maximal graph.

For calculating the emplacement of a graph, we first find the forced maximal graph before decomposing. We could also consider using makeChoices at this top step when there are unknowns, i.e a version of emplace which produces these alternative results (emplaceChoices)

The result of emplaceChoices is illustrated for foolD in figure 23. The first force and composition is unique producing the fool level at which point we get 4 alternatives each of which compose further as previously illustrated in figure 22. Each of these are forced, then decomposed and forced, decomposed and forced again back down to the starting level. In figure 23 foolD is overlaid on the 4 alternative results. What they have in common is (as you might expect) emplace foolD which equals force foolD and is the graph shown on the right of figure 11.

Future Work

I am collaborating with Stephen Huggett who suggested the use of graphs for exploring properties of the tilings. We now have some tools to experiment with but we would also like to complete some formalisation and proofs. For example, we do not know if force g always produces the same result as emplace g. [Update (August 2022): We now have an example where force g strictly includes emplace g].

It would also be good to establish that g is incorrect iff force g fails.

We have other conjectures relating to subgraph ordering of Tgraphs and Galois connections to explore.

by readerunner at November 22, 2022 10:43 AM

WebAssembly backend merged into GHC

Tweag has been working on a GHC WebAssembly backend for some time. Recently, the WebAssembly backend merge request has landed in GHC, and is on course to appear in the upcoming 9.6 release series. This post will give a quick demonstration of how to try it out locally, and explain what comes in this patch and what will be coming next.

Playing with WASM locally

If you’re using nix on x86_64-linux, compiling a Haskell program to a self-contained wasm module is as simple as:

$ nix shell https://gitlab.haskell.org/ghc/ghc-wasm-meta/-/archive/master/ghc-wasm-meta-master.tar.gz
$ echo 'main = putStrLn "hello world"' > hello.hs
$ wasm32-wasi-ghc hello.hs -o hello.wasm
[1 of 2] Compiling Main             ( hello.hs, hello.o )
[2 of 2] Linking hello.wasm
$ wasmtime ./hello.wasm
hello world

There’s also a non-nix installation script. Check the ghc-wasm-meta repo’s README for details.

What’s interesting about the example above? It doesn’t need any companion JavaScript code, and runs on a variety of wasm engines that support wasi, including but not limited to: wasmtime, wasmedge, wasmer and wasm3. Compared to the legacy asterius project, there are also a few other serious benefits:

• The killer feature is being able to use GHC’s own RTS code for garbage collection and other runtime functionality. The GHC RTS is way more robust, feature-complete and performant than asterius’s legacy JavaScript runtime. Lots of Haskell features that never worked in asterius (e.g. STM or profiling) now work out of the box.
• It has proper support for compiling and linking C/C++ code. Terms and conditions apply here, but there’s still a high chance the cbits in your packages will work out of the box.
• Since it uses LLVM for linking, the linking step is orders of magnitudes faster than asterius, which uses a custom object format and linking logic.
• GHC CI tests a program that uses the GHC API to parse a Haskell module. ghc is a big package and depends on everything in the boot libraries, so even having only a part of GHC frontend working in pure wasm is already pretty cool, and it certainly provides more assurance than a simple “hello world”. asterius never had ghc in its boot libraries.

What is in this merge request

The GHC wasm backend merge request’s commit history is carefully structured to contain mostly small and easy to review patches. The changeset can be roughly grouped into:

• Enhancing the build system, making it aware of the wasm32-wasi target, and avoid compiling stuff not supported on that target
• Avoiding the usage of POSIX features not supported on wasm32-wasi – various places need to be patched, like the RTS, base or unix
• Doing various other RTS fixes, for issues that didn’t break other GHC targets by pure luck
• Enhancing the GHC driver with certain wasm-specific logic – most of the time due to the need to workaround some upstream issues in LLVM
• Modeling the wasm structured control flow, and implementing the algorithm to translate arbitrary Cmm control flow graphs to it – this part of the work was done by my colleague Norman Ramsey, and well explained in his ICFP 2022 paper
• Implementing the wasm native code generator (NCG), which translates Cmm to assembly code – unlike NCGs for other targets, the wasm NCG uses a dependently-typed IR to preserve type safety of the wasm value stack, and this has proved to be helpful in catching some errors early on when writing the NCG
• Serving the binary distributions as CI artifacts, and there’s already some basic testing

GHC is a rapidly evolving project, and merging the wasm backend does not make it immune to potential future breakages. For me, it’s not just an honor to implement wasm support, but also a personal commitment to maintain it, prevent bit-rotting, and make sure that the bus factor of this work goes beyond 1 in the future. This is made possible by Tweag’s long term support.

What comes next

JavaScript FFI

asterius had a rich JavaScript FFI implementation, allowing one to import JavaScript functions into Haskell, pass arbitrary JavaScript values as first-class Haskell values, and export Haskell functions to be called by JavaScript. Furthermore, the JavaScript async functions worked naturally with the Haskell threading system, so that when a Haskell thread is blocked on an async JavaScript call, the runtime executes other threads instead of blocking completely.

This is the first of asterius main features that I plan to port to GHC’s wasm backend. You don’t pay for JavaScript if you don’t use it. We’ve already gained good experience with wasm/js interoperability, but this time I will need to do non-trivial refactorings in the GHC RTS storage manager and scheduler to achieve the same. So this will take some time and may not make it into GHC 9.6.1.

Template Haskell

asterius had limited support for Template Haskell. Template Haskell requires dynamically linking Haskell code, but how dynamic linking is supposed to work in wasm is still unclear, so asterius cheated by doing static linking each time a TH splice was evaluated. Since the runtime heap state isn’t preserved between splice evals, when the TH splices are stateful, this approach won’t work, but it’s been proven to work surprisingly well for a lot of TH splices in the wild.

I plan to add Template Haskell support for GHC’s wasm backend in a similar way. Pure TH splices (e.g. generating optics for datatypes) are likely to work, and work much faster than asterius thanks to the much improved linking performance. But splices with side effects (e.g. gitrev that needs to spawn a git subprocess), may not work if the side effect isn’t a supported WASI operation.

Since implementing proper dynamic linking isn’t planned yet, ghci wouldn’t work in GHC’s wasm backend in the near future.

More things to come

There are also other things planned in addition to the above features, including but not limited to:

• Using the GHC issue tracker for bugfixes/feature planning and discussions, for better transparency of my work
• Running the full GHC testsuite and nofib benchmarks
• Supporting cross-compiling to wasm from more host systems
• Wasm-related patches to common Hackage dependencies, or a Hackage overlay for wasm

November 22, 2022 12:00 AM

Seeking new Stackage Curator

The Stackage Curator team is responsible for ongoing maintenance tasks for Stackage: creating builds, adding manual bounds, merging pull requests, and more. The responsibilities and general workflow are described in detail in the curators document, but in short:

• There are a total of 8 curators
• Each curator takes a one-week slot in rotation
• During that week, the curator reviews incoming PRs, ensures Stackage Nightly builds, and puts out an LTS release

I am planning on stepping down from my position as one of the Stackage Curators. With personal and work responsibilities, I simply don't have the time to dedicate to my curator responsibilities. What time I do have available I intend to devote instead to higher level topics, such as toolchain fixes.

And thus this blog post: I'm putting out a call for a new Stackage Curator to join the team. As a Stackage Curator, you're providing a valuable service to the entire Haskell community of helping keeping builds running and packages moving forward. You'll also have more impact on deciding when Stackage makes steps forwards to new versions of GHC and other dependencies.

If you're interested in joining the curator team, please fill out this form.

Thank you

Now seems as good a time as any to say this. I want to express a huge thank you to the entire Haskell community that have been part of Stackage, and in particular to the Stackage Curator team. By raw number of contributors (742 at time of writing), it is the most active project I've ever started. And I never could have kept it running without the rest of the curator team to shoulder the burden. Adam, Alexey, Chris, Dan, Jens, Joe, and Mihai: it's been a pleasure being a curator with you. Thank you for everything, and I'm looking forward to continued involvement on my reduced schedule.

November 21, 2022 12:00 AM

LTS 20 release for ghc-9.2 and Nightly now on ghc-9.4

Stackage LTS 20 has been released

The Stackage team is very happy to announce the first Stackage LTS version 20 snapshot has been released this week, based on GHC stable version 9.2.5.

LTS 20 includes many package changes, and is the first LTS release with over 3000 packages!! Thank you for all the nightly contributions that made this possible.

If your package is missing from LTS 20 and builds there, you can easily request to have it added using our straightforward process: just open a github issue in the lts-haskell project and following the steps in the template.

Stackage Nightly updated to ghc-9.4.3

At the same time we are also excited to have moved Stackage Nightly to GHC 9.4.3 now!

Almost 500 Nightly packages had to be disabled as part of the upgrade to 9.4. Please help to update your packages to build with ghc-9.4 and get them back into Stackage Nightly, thank you!

Big thank you to the community for all your help and support, and do keep the contributions coming!

(Note for Linux users of older glibc < 2.32: at the time of writing stack setups for ghc-9.4 default to the fedora33 bindist which uses glibc-2.32. Some possible workarounds are mentioned in this issue though the Stackage team has not verified the suggestions.)

November 19, 2022 02:00 PM

Funding GHC, Cabal and HLS maintenance

tl;dr Please get in touch if you can help fund development of the core Haskell tools.

Ever since it was founded in 2008, Well-Typed has supported the development and maintenance of the Glasgow Haskell Compiler (GHC) as an open-source project, supplying expert Haskellers to work on essential tasks such as triaging and diagnosing bugs, improving performance, and managing releases. More recently we have expanded our work to include maintenance of the Cabal build tool and the Haskell Language Server (HLS).

We would love to be able to spend more engineering time improving GHC, Cabal and HLS, but we need funding. If your company uses Haskell and might be able to contribute to the future of Haskell development, please contact us!

For many years work on GHC was funded by Microsoft Research. It is currently supported by GitHub via the Haskell Foundation, IOG, and a small number of other commercial sponsors. In addition, Cabal maintenance is supported by IOG, and recently the HLS Open Collective has begun supporting HLS release management. We are very grateful to the sponsors for making our work possible.

Today, the GHC/HLS maintenance team consists of Ben Gamari, Andreas Klebinger, Matthew Pickering, Zubin Duggal and Sam Derbyshire. Cabal maintenance is undertaken by Mikolaj Konarski.

We post regular activity reports from the GHC team to give an idea of the kind of work being undertaken. Besides regular maintenance work, we have recently been collaborating with Hasura on debugging and developer tooling and working on improving HLS performance on behalf of Mercury. We have previously implemented major features for clients, such as the nonmoving garbage collector.

We can offer:

• Significantly reduced rates for sponsoring the work of the GHC, Cabal and HLS teams

• Development of specific features or bug fixes

• Expert support with use of Haskell development tools at your company (e.g. reducing build times or improving the developer experience for your engineers)

Of course, the GHC development community is much bigger than one company. Our approach has always been to support the fantastic volunteers who work on GHC, so the maintenance fund primarily covers activities for which recruiting volunteers is difficult. Implementing new language features is sometimes feasible as an academic research project or fun to do as a hobby, but fixing old bugs is less so!

The part our team plays is clearly recognised by core GHC developers:

I really appreciate the skill, collegiality, and effectiveness of the team at Well Typed.

– Simon Peyton Jones

As a wishing-I-were-more-frequent GHC contributor, I just want to say how much I appreciate the work this team is doing. Over the past year or so (maybe a little longer?), this team has expanded significantly and has become more systematized. The effect is simply wonderful. I no longer worry that GHC tickets get lost, and the responsiveness is excellent.

– Richard Eisenberg

If you might be able to help fund this important work, why not get in touch today?

by adam at November 18, 2022 12:00 AM

JupyterWith Next

JupyterWith has been around for several years with growing popularity. Over the years, we found that researchers struggled with the Nix language and jupyterWith API. Since researchers are our primary target audience, we decided to improve the usability of jupyterWith.

Today, we are proud to announce the release of a new version! The new simplified API makes jupyterWith easier to use and provides more options for creating kernels.

What is jupyterWith?

JupyterLab is a web-based interactive development environment for notebooks, code, and data. These notebooks can be shared with other users and the residing code can be rerun providing repeatability.

The Jupyter ecosystem allows users to produce and repeat research and results, but it lacks in facilitating reproducible results. There may not appear to be a difference between repeatable and reproducible, but there is a meaningful difference; reproducibility guarantees that our code and results will be exactly the same while repeatability does not.

While many Jupyter kernels are available as Python packages, just as many are not (e.g. haskell and julia). Projects such as PDM and JupyterLab Requirements can create reproducible environments but are restricted to the Python kernels.

jupyterWith was announced in early 2019 and provides a Nix-based framework for declarative and reproducible JupyterLab environments with configurable kernels. It actively supports over a dozen kernels and provides example setups and notebooks for users to try out. jupyterWith can create entirely reproducible JupyterLab environments for any kernel.

Why jupyterWith?

If you can run an experiment multiple times in the same environment and get to the same conclusion, you have repeatability. In our case, running the same code on the same machine should give the same outputs. Consider what would happen if you handed off your code to another user and they ran it on their system. Different operating systems or different versions of the same operating system may fetch different versions of the same package. Fetching the same package at different times may not return the same version due to patch or security updates. If you can guarantee the same outputs given all that has changed, then you have reproducibility.

With repeatability, we cannot guarantee that the packages and dependencies of our code will remain constant. Using jupyterWith we can give that guarantee and ensure that on any system, run by any user, and given identical inputs, the code will produce identical outputs. This guarantee is what makes our code and therefore our research reproducible.

What is new?

This release focuses on helping users quickly and easily get their project started, and making it easier to extend kernels to fit their needs.

New templates

The new version of jupyterWith provides new kernel templates which makes it easier for users to bootstrap their project using Nix flakes. They are small, easily digestible, and ready to be customized.

Better Python kernels

It used to be difficult to select particular Python packages because we were tied to nixpkgs. jupyterWith now uses Poetry and poetry2nix to install kernels that are packaged with Python and their dependencies. Poetry allows users to easily select the desired version of a package and can resolve dependencies. poetry2nix greatly simplifies the kernel files, which helps with readability and maintainability.

Better kernel definition interface

Finally, we have simplified and standardized the interfaces for kernel files. This makes it easier for users to implement completely new kernels.

Getting Started

The following code will initialize a new project directory with a flake template from the jupyterWith repository and start the JupyterLab environment. With a renewed focus on user ease, this is all that is necessary to get started.

$ mkdir my-project
$ cd my-project
$ nix flake init --template github:tweag/jupyterWith
$ nix run

Each kernel provided will generally only have the standard libraries and packages available, but there is a readme provided with the template with instructions on extending existing kernels, creating a custom kernel, and installing extensions.

Migration

If you have used jupyterWith in the past, you are probably used to seeing kernel files like the ipython kernel example below. The version of Python used and the packages available to the kernel, can be set using the python3 and packages attributes respectively.

Old interface

{
  iPython = iPythonWith {
    # Identifier that will appear on the Jupyter interface.
    name = "nixpkgs";
    # Libraries to be available to the kernel.
    packages = p: with p; [ numpy pandas ];
    # Optional definition of `python3` to be used.
    # Useful for overlaying packages.
    python3 = pkgs.python3Packages;
    # Optional value to true that ignore file collisions inside the packages environment
    ignoreCollisions = false;
  };
}

The new interface is similar but there are a few key differences. All kernels are provided through availableKernels and the kernels are named by the language rather than the kernel project name. For example, before there was iPythonWith and iHaskellWith, and now it is availableKernels.python and availableKernels.haskell. The version of Python uses is passed through the python attribute and additional packages are provided with the extraPackages attribute. There is one new attribute, editablePackageSources, which is used by poetry2nix, to add packages to the environment in editable mode.

New interface!

{
  pkgs,
  availableKernels,
  kernelName,
}:
availableKernels.python.override {
  name = "python-with-numpy"; # must be unique
  displayName = "python with numpy"; # name that appears in JupyterLab Web UI
  python = pkgs.python3;
  extraPackages = ps: [ ps.numpy ];
  editablePackageSources = {};
}

Both of these are still subject to the package versions available in nixpkgs. However, with Poetry, we can create a completely custom kernel with a pyproject.toml file and specify exactly which package versions we want. The full details are available in the How To and Tutorials sections of the documentation.

Conclusion

Usability has been improved, but there is much more to do. The next major items on the roadmap include:

• Updating and improving the flake templates.
• Updating and improving documentation on configuring existing kernels and packaging new kernels.
• Providing better MacOS support.
• Adding new and improving existing kernels.
• Create a website indexing kernels that can be used and configured in jupyterWith.

Join us in contributing to the project. You can find the repository here.

November 17, 2022 12:00 AM

Staged programming with typeclasses

Staged programming consists of evaluating parts of a program at compile time for greater efficiency at runtime, as some computations would have already been executed or made more efficient during compilation. The poster child for staged programming is the exponential function: to compute a^b, if b is known at compile time, a^b can be replaced by b explicit multiplications. Staged programming allows you to write a^5, but have the expression compile to a*a*a*a*a.

In Haskell, the traditional way to do staged programming is to reach for Template Haskell. Template Haskell is, after all, designed for this purpose and gives you strong guarantees that the produced code is indeed a*a*a*a*a, as desired. On the other hand it does feel a little heavyweight and programmers, in practice, tend to avoid exposing Template Haskell in their interfaces.

In this blog post, I want to present another way to do staged programming that is more lightweight, and feels more like a native Haskell solution, but, in exchange, offers fewer guarantees. At its core, what is needed for staged programming is to distinguish between what is statically known and what is dynamically known. In Template Haskell, static and dynamic information is classified by whether an expression is within a quotation or not. But there is another way to signal statically-known information in Haskell: types.

This is what we are going to do in this blog post: passing statically-known arguments at the type level. I’ve used this technique in linear-base.

Natural numbers at the type level

Haskell offers a native kind Nat of type-level natural numbers. We could pass the (statically known) exponent as Nat, in fact we eventually will, but it is difficult to consume numbers of kind Nat because GHC doesn’t know enough about them (for instance, GHC doesn’t know that n+1 is equivalent to 1+n).

Instead, we will use an inductive encoding of the natural numbers: the Peano encoding.

data Peano
  = Z         -- zero
  | S Peano   -- successor of another peano number

In this encoding, 3 is written S (S (S Z)).

Normally, Peano would live at the type level, and both Z and S would live at the term level (they’re data constructors after all). But thanks to the DataKinds extension – which allows data constructors to be promoted to types – we can also use Peano as the kind of type-level Z and S.

Now let’s return to the power function. We will first create a typeclass RecurseOnPeano, that will contain the power function (and that could host any other recursive metaprogramming function that operates on Peanos):

class RecurseOnPeano (n :: Peano) where
  power :: Int -> Int

The power function only needs one term-level parameter: the number that will be multiplied by itself n times. Indeed, the exponent is already “supplied” as a type-level parameter n. In fact, the signature of the power function outside the typeclass would be:

power :: forall (n :: Peano). RecurseOnPeano n => Int -> Int

At a call site, the type-level parameter n will be supplied to the function through a type application, using the dedicated @ symbol (e.g. power @(S (S Z)) 4). It isn’t possible to omit the type parameter n at a call site because there is no way for GHC to deduce it from the type of a term-level parameter of the function. So we need to enable the AllowAmbiguousTypes extension.

The implementation of the power function will be defined through two instances of the RecurseOnPeano typeclass – one for the base case (n = Z), and one for the recursive case (n = S n') – as one would do in a term-level recursive function.

The first instance is relatively straightforward as x^0 = 1 for every positive integer x:

instance RecurseOnPeano Z where
  power _ = 1

For the second instance we want to write power @(S n) x = x * power @n x. But to use power @n x, n needs to fulfill the RecurseOnPeano constraint too. In the end, that yields:

instance RecurseOnPeano n => RecurseOnPeano (S n) where
  power x = x * power @n x

We now have a first working example:

-- <<<<<<<<<<<<< file CompileRecurse.hs >>>>>>>>>>>>>

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module CompileRecurse where
import GHC.TypeLits

data Peano = Z | S Peano

class RecurseOnPeano (n :: Peano) where
  power :: Int -> Int

instance RecurseOnPeano Z where
  power _ = 1
  {-# INLINE power #-}
instance RecurseOnPeano n => RecurseOnPeano (S n) where
  power x = x * power @n x
  {-# INLINE power #-}

-- <<<<<<<<<<<<< file Main.hs >>>>>>>>>>>>>

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
module Main where
import CompileRecurse

main :: IO ()
main = print $ power @(S (S (S Z))) 2  -- this should print 8

Many languages extensions are required for this example to work:

• KindSignatures permits the syntax (n :: Peano) to restrict the RecurseOnPeano class to types of the Peano kind.
• TypeApplications gives the @type syntax to supply type-level parameters.
• DataKinds allows us to promote the Peano data type to the kind level.
• ScopedTypeVariables is needed to be able to refer to n in the body of power in the second instance of RecurseOnPeano.
• AllowAmbiguousTypes is needed when we declare a typeclass function in which the term-level parameters (if there are any) are not sufficient to infer the type-level parameters (and thus require an explicit type application at the call site).

I also added {-# INLINE #-} pragmas on the power implementations, because we indeed want GHC to inline these to achieve our initial goal. For such a simple example, GHC would inline them by default, but it’s better to be explicit about our intent here.

You can now validate that the power @(S (S (S Z))) 2 encoding for 2^3 indeed prints 8 on the terminal.

From Peano type-level integers to GHC Nats

Writing S (S (S Z)) is not very convenient. We would definitely prefer to write 3 instead. And that is possible, if we allow a bit more complexity in our code.

Number literals, such as 3, when used at the type level are of kind Nat from GHC.TypeLits.

Unfortunately, if we completely replace our home-made Peanos with GHC Nats, we will run into some issues of overlapping instances in the RecurseOnPeano typeclass.¹

A solution can be found by using the {-# OVERLAPPING #-} and {-# OVERLAPPABLE #-} pragmas, but it is quite fragile: instance selection is no longer driven by types or structure but rather by a manual override. And the rules for such an override are rather complex, especially when more than two instances are involved; in the case at hand, we might want to add a third instance with a specific implementation for n = 1.

Instead, we will add a type family (that is, a function from types to types) to convert from Nats to Peanos, and add an auxiliary function power' that will take a type-level Nat instead of a type-level Peano:

-- <<<<<<<<<<<<< add to file CompileRecurse.hs >>>>>>>>>>>>>

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}

type family NatToPeano n where
  NatToPeano 0 = Z
  NatToPeano n = S (NatToPeano (n - 1))

-- 'RecurseOnPeano (NatToPeano n) =>' means that the ¨Peano equivalent of n
-- must be an instance of RecurseOnPeano to get access to 'power'
power' :: forall (n :: Nat). (RecurseOnPeano (NatToPeano n)) => Int -> Int
power' = power @(NatToPeano n)

-- <<<<<<<<<<<<< change in file Main.hs >>>>>>>>>>>>>

main = print $ power' @3 2  -- this should still print 8

Our function is still working as expected, and is now more convenient to use!

A look under the hood

Our initial goal was to unroll the power' function at compile time. Let’s check whether this promise holds.

We will create a new test file test/CompileRecurseTests.hs and set specific GHC options so that we can take a look at the generated Core² code for our project:

{-# OPTIONS_GHC -O -ddump-simpl -dsuppress-all -dsuppress-uniques -ddump-to-file #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
module Main where

import CompileRecurse

myFunc :: Int -> Int
myFunc x = power' @3 x + 1

main :: IO ()
main = return ()

The following GHC flags are used:

• -O enables optimizations in GHC.
• -ddump-simpl requests the Core code after the output of the simplifier.
• -dsuppress-all and -dsuppress-uniques reduce the verbosity of the output (otherwise, searching for a specific piece of code would become very tedious).
• Finally, -ddump-to-file asks for the output to be written to a file in the build directory.

With the above options, compiling and running the test suite creates a file CompileRecurseTests.dump-simpl deep down in the build tree.³ If we ignore all the lines about $trModule, we get:

-- RHS size: {terms: 12, types: 3, coercions: 0, joins: 0/0}
myFunc
  = \ x -> case x of { I# x1 -> I# (+# (*# x1 (*# x1 x1)) 1#) }

I# is the “boxing” constructor for integers, that is, the one taking an unboxed integer (Int#) and creating a Haskell Int (an integer behind a pointer). +# and *# are the equivalent of arithmetic functions + and * for unboxed integers Int#.

We can see that myFunc

• takes an Int,
• unboxes its value,
• makes the 2 product operations corresponding to the inlined power' @3 x,
• adds 1, and finally,
• boxes the result once again to produce an Int.

There is no mention of power' here, so the function has been successfully inlined!

Inspection testing

Checking manually whether or not the inlining has happened – by looking through the .dump-simpl file after every change – is really impractical. Instead, it is possible to use the inspection-testing and tasty-inspection-testing libraries to automate such a process.

To do this, we simply need to introduce a function myFunc' – corresponding to what we expect to be the optimized and inlined form of myFunc – and then we check that both myFunc and myFunc' result in the same generated Core code by using the specific === comparison operator (and a little bit of Template Haskell too):

{-# OPTIONS_GHC -O -dno-suppress-type-signatures -fplugin=Test.Tasty.Inspection.Plugin #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}

module Main where

import Test.Tasty
import Test.Tasty.Inspection
import CompileRecurse

myFunc :: Int -> Int
myFunc x = power' @3 x + 1

myFunc' :: Int -> Int
myFunc' x = x * (x * x) + 1

main :: IO ()
main = defaultMain . testGroup "Inspection testing of power'" $
  [ $(inspectTest $ 'myFunc === 'myFunc') ]

Running the test suite gives:

Inspection testing of power'
  myFunc === myFunc': OK

All 1 tests passed (0.01s)

If both functions didn’t result in the same generated Core code – e.g. if we wrote (x * x) * x + 1 instead of x * (x * x) + 1 in myFunc' – we would get:

Inspection testing of power'
  myFunc === myFunc': FAIL
    LHS:
        [ ... ]
        myFunc
          = \ (x [Dmd=<S,1*U(U)>] :: Int) ->
              case x of { I# x1 -> I# (+# (*# x1 (*# x1 x1)) 1#) }
    RHS:
        [ ... ]
        myFunc'
          = \ (x [Dmd=<S,1*U(U)>] :: Int) ->
              case x of { I# x -> I# (+# (*# (*# x x) x) 1#) }

1 out of 1 tests failed (0.01s)
typeclass-blogpost> Test suite inspection-tests failed

In this way, the correct inlining of power' can be checked automatically after each change to the codebase!

Conclusion

This was a brief introduction to staged programming in Haskell, leveraging the type (and typeclass) system as a lightweight alternative to Template Haskell. The technique detailed in this article has been implemented in real-world contexts to create variadic functions like printf, and I hope that you will find many other useful applications for it!

I would like to give a special thank you to Arnaud Spiwack who both taught me this technique in the first place, and then helped me to greatly improve this blog post.

---

1. In short, this is because GHC can’t distinguish between the base and recursive instances with Nats as easily as it can with Peanos↩
2. Core is the main intermediate language used inside GHC.↩
3. In my case, the full path was: .stack-work/dist/x86_64-linux-nix/Cabal-3.4.1.0/build/compile-recurse-tests/compile-recurse-tests-tmp/test/CompileRecurseTests.dump-simpl.↩

November 15, 2022 12:00 AM

Why my video calls sucked (and how I fixed it)

A few years ago, I wrote a blog post about how I set up the networking in our house following some major construction. I was really excited about how much better the internet would be. No more WiFi dead zones, and a wired connection to my computer to provide extra speed and stability to my office. Overall, the results were great. Speed test anywhere in my house showed I was getting the full 500mbps promised by my cable company. However, not everything was working as expected:

• Video calls stuttered, a lot. The most egregious and confusing behavior was that, during a call, I would continue to see the video moving while people went silent for between 10 and 20 seconds.
• My kids complained off-and-on about problems in online games (Minecraft in this case), and had trouble talking with friends over Discord audio chat.

If you're looking for a summary "try this if you're having trouble," here are my three recommendations:

• Diagnosis: try tethering to your smartphone instead of using the internet in your house and see if the behavior is better. You'll almost certainly have slower speeds, but video calls and gaming may be more consistent.
• Stop gap measure: try running a VPN of some kind and see if that improves the situation. One possibility is trying out Cloudflare Warp. This helped significantly for me, but wasn't perfect.
• Real fix for the underlying problem: buy a new router, connect it to the modem/router from your Internet Service Provider (ISP), and put the modem into bridge mode.

The rest of this blog post will try to explain what the problem is. We're going to get into the technicals, but I'm hoping the content will make sense to anyone with basic experience on the internet, not just networking engineers.

Finally, it's worth calling out two coworkers for their involvement in this story. First is Niklas Hambüchen, who years ago warned me of the perils of ISP-provided routers. I should have listened to him then. The second is Neil Mayhew, who not only helped me debug this along the way, but also accidentally gave me the clue I needed to isolate the problem.

Analyzing the problem

If you're suffering from the problems I describe above, it can be incredibly frustrating. Not only do video calls turn into a source of endless pain and miscommunication, but no one will believe you. Call the ISP, and they'll tell you your speed tests are fine. Same with hardware manufacturers, operating systems, and the video software itself in most cases. Nothing sees the problem. You know something is broken, but you're essentially told you're crazy.

The big hints to me that something more complicated was happening under the surface was which things worked well and which didn't. Watch some videos online? No problem at all. Browse websites? Fine. Massive downloads (pretty common in my line of work)? Incredibly fast. The fact that calls and gaming were broken was the first indication something was weird.

The final puzzle piece hit a few weeks ago. The aforementioned Neil had told me for a while how great VR gaming was, especially a game called Echo Arena, and so we ordered an Oculus. I loaded up the game, went into the lobby... and timed out. I tried that a few more times, and it kept happening. Then I tried using my phone as a mobile hotspot, and the game worked perfectly.

Before I explain why that was so important, we have to talk about a few lower level details of networks.

Packets, addresses, and ports

We often use terms like "connecting" to a website. In a physical sense, that doesn't happen. When I go to YouTube.com, I don't have a physical cable, radio signal, or any other physical manifestation of a connection between my computer and some computer at YouTube headquarters. Instead, the way the internet works is a series of computers that connect to each other and pass data around to each other. This is known as routing.

Every computer on a network has an Internet Protocol (IP) address. These are numbers that look like 192.168.54.32. You've probably seen them at some point. The basic idea of routing traffic is I say to the next computer in the line "hey, I want to talk to a computer with that address." The next computer may have connections to 5 other computers, and it knows which of those computers is closest to that IP address. It figures this out using a routing table. The data then "hops" from that computer to the next one, from there to another computer, and so on until it reaches its destination.

But like I said, there aren't any "connections." Instead, internet traffic is made up of a bunch of "packets." You can think of these as envelopes. They have an IP address on the outside, and a small amount of data inside. When you "connect" to another computer, you're actually sending a bunch of these packets over the network. The computers in the middle route your traffic by looking at the outside of the envelope (called the header). And your packets make it to their destination.

One other thing to keep in mind. Each computer can talk to lots of other computers at the same time. Each computer may provide different ways to talk to it (known as protocols, such as the web, or email, or video calling). To allow a single computer to do all these things at the same time, we have one more important number: the port number. This is a number between 1 and 65,536, and tells the computer which "connection" traffic is trying to use. When you send a packet, your header includes the destination IP address and destination port number. It also includes the source IP address and source port number. This allows the other computer to respond to you.

Packet loss, UDP, and TCP

OK, one more topic to learn. There are actual physical mechanisms that control networks. It could be a network cable, a WiFi signal, a statelite connection to Starlink, or the 4G cellular signal on your phone. They all share one thing in common: they can lose data. Maybe you're driving through a tunnel and the cell signal is interrupted. Maybe you live in my neighborhood, and the cable company still hasn't properly protected their cables from water and you lose internet every time it rains. Whatever the case, and for whatever reason, it's entirely possible to lose some of the data. This is known as packet loss.

There are two basic approaches in networking to dealing with packet loss, each with their own advantages and disadvantages.

• User Datagram Protocol, or UDP, is a protocol that works as a "fire and forget" message. I send data to the other side, and I have no guarantees of if it arrived or the order it will arrive in (maybe packet 513 will get there before packet 512). Maybe the same packet will get received multiple times. No one knows.
• Transmission Control Protocol, or TCP, is what people normally think of as a "connection" on the internet. TCP adds a bunch of bookkeeping rules to address the limitations of UDP. It makes sure packets arrive in the correct order, resending them if they didn't get to the other side. It makes sure the order of packets is correct. And it lets you know if the other side breaks the connection.

You may be wondering: why in the world would anyone ever use UDP? It sounds terrible! Overall, TCP is more commonly used for sure, because most people need those guarantees most of the time. But there are some use cases where UDP is far superior. (And finally this weird tangent will connect back to the beginning of the blog post.) UDP is great when:

• You don't actually need every single bit of data to arrive on the other side.
• You care much more about raw speed than other factors.

There are two great examples of this:

1. Audio calls! It turns out that if you take a stream of audio, you can break it down into a whole bunch of tiny data packets containing a slice of time. Then you can send them over the network. If one of those packets is lost, the other side can usually understand what you said from all the other audio packets. And having to add in the delays imposed by TCP to ensure all the data arrives would impose more delays, causing audio calls to become "laggy," or to be more technical, would introduce latency.
2. Gaming. In lots of video games, we don't need to have every single bit of data about what the user did. There are ways to write gaming protocols that say things like "don't tell me the user pressed up for 5 seconds, tell me their new position." If one of those updates gets lost, it's no big deal, the next update will give the newer position. You may "glitch" a bit in the game and jump around, but again, overall, the speed is more important than every piece of data.

There are other examples of UDP being superior, but I won't bother covering them here, because now we know enough to see what was happening in my house.

What's in a router?

It turns out that Echo Arena, that game I tried playing, was communicating with the server over UDP. And for whatever reason, it was more sensitive to the breakage in my house than other things like video calls and Minecraft. It turns out, the router in our house was mishandling UDP packets.

Most people get a router from their cable, DSL, or fiberoptic company when they pay them for internet access. But this device generally is not just a router. It's actually doing three different jobs most of the time, and we need to separate those out:

1. Modem. The term modem means a device that converts one kind of physical connection into a network connection. Cable modems, for example, convert the TV cable wires already running into your house into a network signal, something they weren't originally designed for. Fiber modems will convert the fiberoptic light-based signals into a network signal. DSL does the same with phone lines. Even old-school dial-up modems are simply using audio over the phone line for the same purpose.
2. Wireless access point. You can connect to your "router" by plugging in a network cable to the back and connecting that to your computer. But most people these days are using a WiFi signal instead. A wireless access point is the translator between WiFi signals and your wired network. In the case of your modem/wireless router combo, it's built into the device, but you could use an external one. (And this is a great way to extend the range of your wireless network if you need to.)
3. Router. Before we get into that though, there are two more things we need to learn about IP addresses:

• There are some IP addresses that have been reserved as "private," meaning they can be used inside people's homes or businesses, but can't go on the internet. This includes anything that starts with 10. or 192.168.. If those look familiar... just wait a second, we'll get to it.
• There are only 4 billion IP addresses possible. That may seem like a lot, but it turns out that it isn't nearly enough for all the people, servers, Internet of Things devices, and everything else that wants to be on the internet. We have an IP address shortage.

  • Side note: the current common IP address standard is called IPv4, and is what I'm referring to. There's a new standard, called IPv6, that totally solves this problem by introducing an insane number of addresses. To get a sense of how big:

    340,282,366,920,938,463,463,374,607,431,768,211,456, which is approximately 340 undecillion addresses...

    So we could assign an IPV6 address to EVERY ATOM ON THE SURFACE OF THE EARTH, and still have enough addresses left to do another 100+ earths.

Unfortunately, IPv6 is having trouble taking off, so we're stuck with IPv4 and a shortage of IP addresses. And this is where your router comes in. Its job is to get a public IP address from your ISP, and then create a local network inside your house. It does this by a few different technologies:

• The router creates a private IP address for itself. This is commonly 192.168.0.1, or 192.168.1.1, or something along those lines.
• It runs something called a DHCP server that lets other computers on the network ask for a new IP address and connection information. It will hand out private addresses like 192.168.1.27.
• And finally, the part we care about the most: your router does Network Address Translation, or NAT, to convert your packets from private to public addresses.

What's in a NAT?

Let's break this down. Suppose you're trying to connect to a website like youtube.com. Your computer will look up (using a different system called DNS which I'm not covering right now) that website's IP address. For example, I just got the address 172.217.18.14 when looking up www.youtube.com. I want to connect to it as a secure website (HTTPS), and the standard port number for that is 443. My computer knows its own private IP address (let's say it's 192.168.1.27), and randomly chooses an unused port number (let's say 4001). Then my computer makes a packet that looks like:

• Destination IP: 172.217.18.14
• Destination port: 443
• Source IP: 192.168.1.27
• Source port: 4001
• Data: please start a TCP connection with me

Then, it sends that packet to my router so the router can pass that packet on to the rest of the internet. However, as it stands right now, that packet will be blocked, because private IP addresses are not allowed on the internet. And that's a good thing, because lots of computers in the world have the IP address 192.168.1.27, and YouTube wouldn't know which comptuer to send it to.

Instead, the router translates the network address (e.g., NAT). The router has some public IP address it got from my ISP, let's say 82.20.63.76. It will then translate the header on the packet above to say:

• Source IP: 82.20.63.76
• Source port: 54542 (we'll come back to why this is different in a moment)

The router has to remember that it did this translation, and it sends off the packet to the internet. Eventually YouTube receives the request, processes it, and sends out a packet of its own that looks like this:

• Destination IP: 82.20.63.76
• Destination port: 54542
• Source IP: 172.217.18.14
• Source port: 443
• Data: OK, starting a TCP connection

The router receives this packet, notices the destination port, and remembers "hey, I remember that 192.168.1.27 should get these." It then replaces the destination IP and port with:

• Destination IP: 192.168.1.27
• Destination port: 4001

It then sends that data into the local network inside my house, where my computer receives it, and thinks it's talking directly to YouTube.

Side point: why did the router change from 4001 to 54542? Because other computers in my network may also be using source port 4001, and the router needs to distinguish which computer should receive these packets.

This is a horribly ugly hacky workaround for not having enough IP addresses. But it (mostly) works just fine, and the entire internet is built on it right now.

If you want to see evidence of this happening, check your local computers settings and see what IP address it thinks it has. Then compare with the number you get from https://whatsmyip.com/. That website is seeing the IP address from the router, not from your local computer, and so you'll almost certainly get two different numbers.

About that "mostly"

I said this all mostly works. Let's start with TCP. With TCP, there's a whole protocol of how to connect over TCP. The router understands this, looks at the headers and the data, and remembers the mapping between the original source IP/port and the new source port. Almost every router under the sun handles this situation really well.

Unfortunately, the situation isn't as good for UDP. That's because there's no real "connection." UDP is just a bunch of packets. Good routers handle UDP really well, keep track of the mappings, and intelligently decide when a source port has been unused for long enough that it's allowed to forget about it.

And that brings me to my video call problems. The router included with the modem from my ISP sucks. It would forget about these mappings at the wrong time. The result would be that, in the middle of a call, the UDP packets carrying the audio from the other side would suddenly get "stuck" on the router and not get sent to my computer. Eventually, the router would remember a new port mapping and the call would resume. But I'd lose 10-20 seconds of audio while that happened.

For various technical reasons that I'm no expert at and aren't really relevant, the video data in calls often goes over TCP instead of UDP, and that's why I would continue to see the video move while people went silent.

Similarly, the kids could play Minecraft for a while before packet loss ensued and they'd get sent to "limbo." Discord calls would work until they'd glitch for a bit. And finally, the final puzzle piece: Echo Arena detected the situation much faster than anything else and simply refused to play at all.

The solution

With the problem identified, the solution is simple: don't use the router in the modem I got from my ISP. I bought a new router, plugged it into the modem, and switched the modem into "bridge mode." This disables the router functionality in the modem. Now my shiny new router got a public IP address and could send data directly to the internet. It's responsible for giving out IP addresses in my house and doing all the NAT work. And since it's a good router, it does this all correctly. With this device installed, video calls instantly became near-perfect, my kids stopped complaining about Minecraft, and I could play Echo Arena (which I still suck at, but hey, that's what I get for writing blog posts instead of practicing my video game skills).

In my case, I already had Wireless Access Points (WAPs) throughout the house, so I did not need a wireless router. Instead, I bought an ER605 from TP-Link. I've been very happy with the EAP245 WAPs I got from TP-Link before, and this is part of the same business class of devices. However, if you don't have your own WAPs, it's probably a better idea to get a wireless router, which includes both router and WAP functionality.

Anyway, I hope that explanation is helpful to someone else. When discussing with Neil, he pointed out how sad it is that many people in the world are probably affected by this crappy-internet problem and have no way of diagnosing it themselves. (Hell, I'm a network engineer and it took about three years for me to figure it out!) Good luck to all!

November 14, 2022 12:00 AM

IO Scotfest: The Age of Voltaire - Nov 18-19

IOHK/IOG will be hosting a meeting at Edinburgh next week. Available online, plus an in-person meetup for folk near Edinburgh.

Let’s celebrate the dawning of a new era for #Cardano together. Join us for a virtual event that will showcase the community’s achievements over the last 5 years & discuss IOG’s vision for the future of Cardano. Learn more: https://lnkd.in/g2bzZEtR

 

by Philip Wadler (noreply@blogger.com) at November 12, 2022 12:11 PM

Addenda to recent articles 202210

I haven't done one of these in a while. And there have been addenda. I thought hey, what if I ask Git to give me a list of commits from October that contain the word ‘Addendum’. And what do you know, that worked pretty well. So maybe addenda summaries will become a regular thing again, if I don't forget by next month.

Most of the addenda resulted in separate followup articles, which I assume you will already have seen. ([1] [2] [3]) I will not mention this sort of addendum in future summaries.

• In my discussion of lazy search in Haskell I had a few versions that used do-notation in the list monad, but eventually abandoned it n favor of explicit concatMap. For example:

        s nodes = nodes ++ (s $ concatMap childrenOf nodes)
  

  I went back to see what this would look like with do notation:

        s nodes = (nodes ++) . s $ do
            n <- nodes
            childrenOf n
  

  Meh.

• Regarding the origin of the family name ‘Hooker’, I rejected Wiktionary's suggestion that it was an occupational name for a maker of hooks, and speculated that it might be a fisherman. I am still trying to figure this out. I asked about it on English Language Stack Exchange but I have not seen anything really persuasive yet. One of the answers suggests that it is a maker of hooks, spelled hocere in earlier times.

  (I had been picturing wrought-iron hooks for hanging things, and wondered why the occupational term for a maker of these wasn't “Smith”. But the hooks are supposedly clothes-fastening hooks, made of bone or some similar finely-workable material. )

  The OED has no record of hocere, so I've asked for access to the Dictionary of Old English Corpus of the Bodleian library. This is supposedly available to anyone for noncommercial use, but it has been eight days and they have not yet answered my request.

  I will post an update, if I have anything to update.

by Mark Dominus (mjd@plover.com) at November 08, 2022 11:34 PM

GHC 9.2.5 is now available

GHC 9.2.5 is now available

Zubin Duggal - 2022-11-07

The GHC developers are happy to announce the availability of GHC 9.2.5. Binary distributions, source distributions, and documentation are available at downloads.haskell.org.

This release is primarily a bugfix release addressing a few issues found in 9.2.4. These include:

• Code generation issues in the AArch64 native code generator backend resulting in incorrect runtime results in some circumstances (#22282, #21964)
• Fixes for a number of issues with the simplifier leading to core lint errors and suboptimal performance (#21694, #21755, #22114)
• A long-standing interface-file determinism issue where full paths would leak into the interface file (#22162)
• A runtime system bug where creating empty mutable arrays resulted in a crash (#21962)
• … and a few more. See the release notes for a full accounting.

As some of the fixed issues do affect correctness users are encouraged to upgrade promptly.

We would like to thank Microsoft Azure, GitHub, IOG, the Zw3rk stake pool, Well-Typed, Tweag I/O, Serokell, Equinix, SimSpace, Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work comprise this release.

As always, do give this release a try and open a ticket if you see anything amiss.

Happy compiling,

• Zubin

by ghc-devs at November 07, 2022 12:00 AM

A map of Haskell's numeric types

I keep getting lost in the maze of Haskell's numeric types. Here's the map I drew to help myself out. (I think there might have been something like this in the original Haskell 1998 report.)

(PNG version) (Original DOT file (The SVG above is hand-edited graphviz output))

Ovals are typeclasses. Rectangles are types. Black mostly-straight arrows show instance relationships. Most of the defined functions have straightforward types like or or . The few exceptions are shown by wiggly colored arrows.

Basic plan

After I had meditated for a while on this picture I began to understand the underlying organization. All numbers support and . And there are three important properties numbers might additionally have:

• Ord : ordered; supports etc.
• Fractional : supports division
• Enum: supports ‘pred’ and ‘succ’

Integral types are both Ord and Enum, but they are not Fractional because integers aren't closed under division.

Floating-point and rational types are Ord and Fractional but not Enum because there's no notion of the ‘next’ or ‘previous’ rational number.

Complex numbers are numbers but not Ord because they don't admit a total ordering. That's why Num plus Ord is called Real: it's ‘real’ as constrasted with ‘complex’.

More stuff

That's the basic scheme. There are some less-important elaborations:

Real plus Fractional is called RealFrac.

Fractional numbers can be represented as exact rationals or as floating point. In the latter case they are instances of Floating. The Floating types are required to support a large family of functions like and π.

You can construct a Ratio a type for any a; that's a fraction whose numerators and denominators are values of type a. If you do this, the Ratio a that you get is a Fractional, even if a wasn't one. In particular, Ratio Integer is called Rational and is (of course) Fractional.

Shuff that don't work so good

Complex Int and Complex Rational look like they should exist, but they don't really. Complex a is only an instance of Num when a is floating-point. This means you can't even do 3 :: Complex Int — there's no definition of fromInteger. You can construct values of type Complex Int, but you can't do anything with them, not even addition and subtraction. I think the root of the problem is that Num requires an abs function, and for complex numbers you need the sqrt function to be able to compute abs.

Complex Int could in principle support most of the functions required by Integral (such as div and mod) but Haskell forecloses this too because its definition of Integral requires Real as a prerequisite.

You are only allowed to construct Ratio a if a is integral. Mathematically this is a bit odd. There is a generic construction, called the field of quotients, which takes a ring and turns it into a field, essentially by considering all the formal fractions (where ), and with considered equivalent to exactly when . If you do this with the integers, you get the rational numbers; if you do it with a ring of polynomials, you get a field of rational functions, and so on. If you do it to a ring that's already a field, it still works, and the field you get is trivially isomorphic to the original one. But Haskell doesn't allow it.

I had another couple of pages written about yet more ways in which the numeric class hierarchy is a mess (the draft title of this article was "Haskell's numbers are a hot mess") but I'm going to cut the scroll here and leave the hot mess for another time.

[ Addendum: Updated SVG and PNG to version 1.1. ]

by Mark Dominus (mjd@plover.com) at November 05, 2022 01:12 AM

GHC 9.4.3 released

GHC 9.4.3 released

bgamari - 2022-11-03

The GHC developers are happy to announce the availability of GHC 9.4.3. Binary distributions, source distributions, and documentation are available at downloads.haskell.org.

This release is primarily a bugfix release addressing a few issues found in 9.4.2. These include:

• An issue where recursively calls could be speculatively evaluated, resulting in non-termination (#20836)
• A code generation issue in the AArch64 native code generator backend resulting in incorrect runtime results in some circumstances (#22282)
• A crash on Darwin when running executables compiled with IPE support (#22080)
• A long-standing interface-file determinism issue where full paths would leak into the interface file (#22162)
• A bug in the process library where file handles specified as NoStream would still be usable in the child (process#251)

Note that, as GHC 9.4 is the first release series where the release artifacts are all generated by our new Hadrian build system, it is possible that there will be packaging issues. If you enounter trouble while using a binary distribution, please open a ticket. Likewise, if you are a downstream packager, do consider migrating to Hadrian to run your build; the Hadrian build system can be built using cabal-install, stack, or the in-tree bootstrap script. See the accompanying blog post for details on migrating packaging to Hadrian.

We would also like to emphasize that GHC 9.4 must be used in conjunction with Cabal-3.8 or later. This is particularly important for Windows users due to changes in GHC’s Windows toolchain.

We would like to thank Microsoft Azure, GitHub, IOG, the Zw3rk stake pool, Well-Typed, Tweag I/O, Serokell, Equinix, SimSpace, Haskell Foundation, and other anonymous contributors whose on-going financial and in-kind support has facilitated GHC maintenance and release management over the years. Finally, this release would not have been possible without the hundreds of open-source contributors whose work comprise this release.

As always, do give this release a try and open a ticket if you see anything amiss.

Happy Haskelling,

• Ben

by ghc-devs at November 03, 2022 12:00 AM

Break Gently with Pattern Synonyms

This is a really brief post to call out a nice trick for providing users a nice migration message when you delete a constructor in a sum type.

The Problem

You have a sum type, and you want to delete a redundant constructor to refactor things.

data Foo 
    = Bar Int 
    | Baz Char
    | Quux Double

That Quux is double trouble. But if we simply delete it, then users will get a Constructor not found: Quux. This isn’t super helpful. They’ll have to go find where Quux came from, what package defined it, and then go see if there’s a Changelog. If not, then they’ll have to dig through the Git history to see what’s going on. This isn’t a fun workflow.

But, let’s say you really need end users to migrate off Quux. So we’re interested in giving a compile error that has more information than Constructor not in scope.

Here’s what some calling code looks like:

blah :: Foo -> Int
blah x = case x of
    Bar i -> i
    Baz c -> fromEnum c
    Quux a -> 3

will give the output:

/home/matt/patsyn.hs:24:5: error:
    Not in scope: data constructor ‘Quux’
   |
24 |     Quux a -> 3
   |     ^^^^
Failed, no modules loaded.

Fortunately, we can make this nicer.

GHC gives us a neat trick called PatternSynonyms. They create constructor-like things that we can match on and construct with, but that are a bit smarter.

Matching

Let’s redefine Quux as a pattern synonym on Foo. We’ll also export it as part of the datatype definition.

{-# language PatternSynonyms, ViewPatterns #-}

module Wow (Foo (.., Quux)) where

data Foo
    = Bar Int
    | Baz Char

pattern Quux :: a -> Foo
pattern Quux i <- (const Nothing -> Just i)

This does something tricky: we always throw away the input with the ViewPattern, and we can summon whatever we want in the left hand side. This allows us to provide whatever a is needed to satisfy the type. This match will never succeed - so Quux behavior will never happen.

Now, we get a warning for the match:

[1 of 1] Compiling Main             ( /home/matt/patsyn.hs, interpreted )

/home/matt/patsyn.hs:25:5: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In a case alternative: Quux a -> ...
   |
25 |     Quux a -> 3
   |     ^^^^^^^^^^^
Ok, one module loaded.

But an error for constructing:

[1 of 1] Compiling Main             ( /home/matt/patsyn.hs, interpreted )

/home/matt/patsyn.hs:28:10: error:
    • non-bidirectional pattern synonym ‘Quux’ used in an expression
    • In the expression: Quux 3
      In an equation for ‘blargh’: blargh = Quux 3
   |
28 | blargh = Quux 3
   |          ^^^^
Failed, no modules loaded.

So we need to construct with it, too. We can modify the pattern synonym by providing a where, and specifying how to construct with it. Since we’re intending to prevent folks from using it, we’ll just use undefined.

pattern Quux :: a -> Foo
pattern Quux i <- (const Nothing -> Just i) where
    Quux _ = undefined

With this, we get just the warning about a redundant pattern match. Now it’s time to step up our game by providing a message to the end user.

Warnings

GHC gives us the ability to write {-# WARNING Quux "migrate me pls" #-}. This can make sense if we expect that the runtime behavior of a program won’t be changed by our pattern synonym.

So let’s write a warning:

pattern Quux :: a -> Foo
pattern Quux i <- (const Nothing -> Just i) where
    Quux _ = undefined

{-# WARNING 
  Quux 
    "Please migrate away from Quux in some cool manner. \
    \See X resource for migration tips." 
  #-}

Now, when compiling, we’ll see the warnings:

/home/matt/patsynimp.hs:11:5: warning: [-Wdeprecations]
    In the use of data constructor ‘Quux’ (imported from PatSyn):
    "Please migrate away from Quux in some cool manner. See X resource for migration tips."
   |
11 |     Quux _ -> 3
   |     ^^^^

/home/matt/patsynimp.hs:11:5: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In a case alternative: Quux _ -> ...
   |
11 |     Quux _ -> 3
   |     ^^^^^^^^^^^

/home/matt/patsynimp.hs:14:10: warning: [-Wdeprecations]
    In the use of data constructor ‘Quux’ (imported from PatSyn):
    "Please migrate away from Quux in some cool manner. See X resource for migration tips."
   |
14 | blargh = Quux (3 :: Int)
   |          ^^^^

But this may not be good enough. We may want to give them an error, so they can’t build.

TypeError

base defines a type TypeError, which GHC treats specially - it raises a type error. This isn’t generally useful, but can be great for marking branches of a type family or type class instance as “impossible.” The error message can be fantastic for guiding folks towards writing correct code.

PatternSynonyms can have two sets of constraints: the first is required when constructing, and the second is provided when matching. So let’s just put an error in the first and see what happens:

pattern Quux
    :: (TypeError ('Text "please migrate ..."))
    => ()
    => a -> Foo
pattern Quux i <- (const Nothing -> Just i) where
    Quux _ = undefined

Unfortunately, GHC blows up immediately while compiling the synonym!

[1 of 2] Compiling PatSyn           ( PatSyn.hs, interpreted )

PatSyn.hs:20:1: error: please migrate ...
   |
20 | pattern Quux
   | ^^^^^^^^^^^^...
Failed, no modules loaded.

We can’t even -fdefer-type-errors this one. Are we hosed?

What about the second position? Same problem. We can’t put a bare TypeError in there at all.

Fortunately, we can have a lil’ bit of laziness by introducing it as a constraint.

class DeferredError
instance (TypeError ('Text "please migrate ...")) => DeferredError

pattern Quux
    :: DeferredError
    => DeferredError
    => a -> Foo
pattern Quux i <- (const Nothing -> Just i) where
    Quux _ = undefined

This actually does give us a warning now - at the const Nothing -> Just i line, we have a deferred type error.

This gives us the error behavior we want!

/home/matt/patsynimp.hs:14:10: error:
    • please migrate ...
    • In the expression: Quux (3 :: Int)
      In an equation for ‘blargh’: blargh = Quux (3 :: Int)
   |
14 | blargh = Quux (3 :: Int)
   |          ^^^^^^^^^^^^^^^
Failed, one module loaded.

We only get the one error - but if we delete it, we can see the other error:

[2 of 2] Compiling Main             ( /home/matt/patsynimp.hs, interpreted )

/home/matt/patsynimp.hs:11:5: error:
    • please migrate ...
    • In the pattern: Quux _
      In a case alternative: Quux _ -> 3
      In the expression:
        case x of
          Bar i -> i
          Baz c -> fromEnum c
          Quux _ -> 3
   |
11 |     Quux _ -> 3
   |     ^^^^^^
Failed, one module loaded.

What’s fun is that we can actually provide two different messages. Constructing something will give both error messages, and pattern matching only uses the “required” constraint.

This should make it much easier for end users to migrate to new versions of your library.

Final Code and Errors

{-# language PatternSynonyms #-}
{-# language KindSignatures #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language ViewPatterns #-}
{-# language MultiParamTypeClasses #-}
{-# language UndecidableInstances #-}
{-# language DataKinds #-}

{-# OPTIONS_GHC -fdefer-type-errors #-}

module PatSyn where

import Prelude
import GHC.Exts
import GHC.TypeLits

data Foo
    = Bar Int
    | Baz Char

class DeferredError (a :: ErrorMessage)
instance (TypeError a) => DeferredError a

pattern Quux
    :: DeferredError ('Text "please migrate (required constraint)")
    => DeferredError ('Text "please migrate (provided constraint)")
    => a -> Foo
pattern Quux i <- (const Nothing -> Just i) where
    Quux _ = undefined

Matching a constructor:

[2 of 2] Compiling Main             ( /home/matt/patsynimp.hs, interpreted )

/home/matt/patsynimp.hs:11:5: error:
    • please migrate (required constraint)
    • In the pattern: Quux _
      In a case alternative: Quux _ -> 3
      In the expression:
        case x of
          Bar i -> i
          Baz c -> fromEnum c
          Quux _ -> 3
   |
11 |     Quux _ -> 3
   |     ^^^^^^
Failed, one module loaded.

Using a constructor:

[2 of 2] Compiling Main             ( /home/matt/patsynimp.hs, interpreted )

/home/matt/patsynimp.hs:14:10: error:
    • please migrate (required constraint)
    • In the expression: Quux (3 :: Int)
      In an equation for ‘blargh’: blargh = Quux (3 :: Int)
   |
14 | blargh = Quux (3 :: Int)
   |          ^^^^^^^^^^^^^^^

/home/matt/patsynimp.hs:14:10: error:
    • please migrate (provided constraint)
    • In the expression: Quux (3 :: Int)
      In an equation for ‘blargh’: blargh = Quux (3 :: Int)
   |
14 | blargh = Quux (3 :: Int)
   |          ^^^^^^^^^^^^^^^
Failed, one module loaded.

November 02, 2022 12:00 AM

Emoji for U.S. presidents

Content warning: something here to offend almost everyone

A while back I complained that there were no emoji portraits of U.S. presidents. Not that there a Chester A. Arthur portrait would see a lot of use. But some of the others might come in handy.

I couldn't figure them all out. I have no idea what a Chester Arthur emoji would look like. And I assigned 🧔� to all three of Garfield, Harrison, and Hayes, which I guess is ambiguous but do you really need to be able to tell the difference between Garfield, Harrison, and Hayes? I don't think you do. But I'm pretty happy with most of the rest.

George Washington	💵
John Adams
Thomas Jefferson	📜
James Madison
James Monroe
John Quincy Adams	�
Andrew Jackson
Martin Van Buren	🌷
William Henry Harrison	🪦
John Tyler
James K. Polk
Zachary Taylor
Millard Fillmore	⛽
Franklin Pierce
James Buchanan
Abraham Lincoln	�
Andrew Johnson	💩
Ulysses S. Grant	�
Rutherford B. Hayes	🧔�
James Garfield	🧔�
Chester A. Arthur
Grover Cleveland	🔂
Benjamin Harrison	🧔�
Grover Cleveland	🔂
William McKinley
Theodore Roosevelt	🧸
William Howard Taft	�
Woodrow Wilson	�
Warren G. Harding	🫖
Calvin Coolidge	🙊
Herbert Hoover	⛺
Franklin D. Roosevelt	👨�🦽
Harry S. Truman	�
Dwight D. Eisenhower	🪖
John F. Kennedy	�
Lyndon B. Johnson	🗳�
Richard M. Nixon	�
Gerald R. Ford	�
Jimmy Carter	🥜
Ronald Reagan	💸
George H. W. Bush	👻
William J. Clinton	�
George W. Bush	�
Barack Obama	🇰🇪
Donald J. Trump	�
Joseph R. Biden	🕶�

Honorable mention: Benjamin Franklin �

Dishonorable mention: J. Edgar Hoover 👚

If anyone has better suggestions I'm glad to hear them. Note that I considered, and rejected � for Lincoln because it doesn't look like his actual hat. And I thought maybe McKinley should be �� but since they changed the name of the mountain back I decided to save it in case we ever elect a President Denali.

(Thanks to Liam Damewood for suggesting Harding, and to Colton Jang for Clinton's saxophone.)

[ Addendum 20221106: Twitter user Simon suggests emoji for UK prime ministers. ]

[ Addendum 20221108: Rasmus Villemoes makes a good suggestion of 😼 for Garfield. I had considered this angle, but abandoned it because there was no way to be sure that the cat would be orange, overweight, or grouchy. Also the 🧔� thing is funnier the more it is used. But I had been unaware that there is CAT FACE WITH WRY SMILE until M. Villemoes brought it to my attention, so maybe. (Had there been an emoji resembling a lasagna I would have chosen it instantly.) ]

[ Addendum 20221108: January First-of-May has suggested 🌷 for Maarten van Buren, a Dutch-American whose first language was not English but Dutch. Let it be so! ]

by Mark Dominus (mjd@plover.com) at October 31, 2022 09:50 PM

Spooky Masks and Async Exceptions

Everyone loves Haskell because it makes concurrent programming so easy! forkIO is great, and you’ve got STM and MVar and other fun tools that are pleasant to use.

Well, then you learn about asynchronous exceptions. The world seems a little scarier - an exception could be lurking around any corner! Anyone with your ThreadId could blast you with a killThread or throwTo and you would have no idea what happened.

The async library hides a lot of this from you by managing the forkIO and throwTo stuff for you. It also makes it easy to wait on a thread to finish, and receive exceptions that the forked thread died with. Consider how nice the implementation of timeout is here:

timeout :: Int -> IO a -> IO (Maybe a)
timeout microseconds action = do
  withAsync (Just <$> action) $ \a0 ->
  withAsync (Nothing <$ threadDelay microseconds) $ \a1 ->
      either id id <$> waitEither a0 a1

The async library uses asynchronous exceptions to signal that a thread must die. The withAsync function guarantees that the forked thread is killed off when the inner action is complete. So timeout will fork a thread to run Just <$> action, and then fork another thread to threadDelay. waitEither accepts an Async a and an Async b and returns an IO (Either a b) - whichever one finishes first determines the return type. If threadDelay finishes first, then we get a Right Nothing as the return, and exits. This spells doom for the action thread.

But if our brave hero is able to escape before the deadline, it’s the threadDelay that gets killed!

Indeed, this is a specialization of race :: IO a -> IO b -> IO (Either a b), which runs two IO actions in separate threads. The first to complete returns the value, and the remaining thread is sacrificed to unspeakable horrors.

But, you really shouldn’t catch or handle async exceptions yourself. GHC uses them to indicate “you really need to shut down extremely quickly, please handle your shit right now.” ThreadKilled is used to end a thread’s execution, and UserInterrupt means that you got a SIGINT signal and need to stop gracefully. The async package uses AsyncCancelled to, well, cancel threads. However, the base package’s Control.Exception has a footgun: if you catch-all-exceptions by matching on SomeException, then you’ll catch these async exceptions too!

Now, you should pretty much never be catching SomeException, unless you really really know what you’re doing. But I see it all the time:

import Control.Exception (catch)

blah = 
    Just <$> coolThing 
        `catch` \(SomeException e) -> do
            reportException e
            pure Nothing

If coolThing receives a ThreadKilled or an AsyncCancelled or UserInterrupt or anything else from throwTo, it’ll catch it, report it, and then your program will continue running. Then the second Ctrl-C comes from the user, and your program halts immediately without running any cleanup. This is pretty dang bad! You really want your finally calls to run.

You search for a bit, and you find the safe-exceptions package. It promises to make things a lot nicer by not catching async exceptions by default. So our prior code block, with just a change in import, becomes much safer:

import Control.Exception.Safe (catch)

blah = 
    Just <$> coolThing 
        `catch` \(SomeException e) -> do
            reportException e
            pure Nothing

This code will no longer catch and report an async exception. However, the blocks in your finally and bracket for cleanup will run!

Unfortunately, the safe-exceptions library (and the unliftio package which uses the same behavior), have a dark secret…

*thunder claps in the distance, as rain begins to fall*

… they wear spooky masks while cleaning! WowowoOOOoOoOooOooOOooOooOOo

No, really, they do something like this:

bracket provide cleanup action = 
    Control.Exception.bracket
        provide
        (\a -> 
            Control.Exception.uninterruptibleMask_ $ 
                cleanup a)
        action

This code looks pretty innocuous. It even says that it’s good! “Your cleanup function is guaranteed not to be interrupted by an asynchronous exception.” So if you’re cleaning things up, and BAMM a vampire ThreadKills you, you’ll finish your cleanup before rethrowing. This might just be all you need to make it out of the dungeon alive.

Behind the sweet smile and innocent demeanor of the safe-exceptions package, though, is a dark mystery - and a vendetta for blood. Well, maybe not blood, but I guess “intercompatibility of default expectations”?

A Nightmare Scenario: Night of the Living Deadlock

Once, a brave detective tried to understand how slow the database was. But in her studies, she accidentally caused the the entire app to deadlock and become an unkillable zombie?!

There are three actors in this horror mystery. Mr DA, the prime suspect. Alice, our detective. And Bob, the unassuming janitor.

Mr Database Acquisition

One of the suspected villains is Mr. Database Acquisition, a known rogue. Usually, Mr. Database Acquisition works quickly and effectively, but sometimes everything stops and he’s nowhere to be found. We’re already recording how long he takes by measuring the job completion time, but if the job never finishes, we don’t know anything.

The database connection is provided from a resource-pool Pool, which is supposed to be thread safe and guarantee resource allocation. But something seems shady about it…

Alice

Alice is a performance engineer and lead detective. She’s interested in making the codebase faster, and to do so, she sets up inspection points to log how long things are taking.

Alice cleverly sets up a phantom detective - a forked thread that occasionally checks in on Mr Database.

withAcquisitionTimer
    :: (IO () -> IO r) -> IO r
withAcquisitionTimer action = do
    timeSpent <- newIORef 0
    let tracker = 
            forever $ do
                threadDelay 1000
                timeSpent <- atomicModifyIORef' timeSpent (\a -> (a+1000, a+1000))
                recordMetric runningWait timeSpent

        report = do
            elapsed <- readIORef timeSpent
            recordMetric totalWait elapsed

    withAsync (tracker `finally` report) $ \a ->
        action (cancel a)

The actual implementation is a bit more robust and sensible, but this gets the gist across. Pretend we’re in a campy low budget horror movie.

The tracker thread wakes up every millisecond to record how long we’re waiting, and continues running until the thread is finally cancelled, or killed with an async exception, or the action finishes successfully, or if a regular exception causes action to exit early. withAsync will cancel the tracker thread, ensuring that we don’t leak threads. Part of cancel’s API is that it doesn’t return until the thread is totally, completely, certainly dead - so when withAsync returns, you’re guaranteed that the thread is dead.

Alice sets the tracker up for every database acquisition, and waits to see what’s really going on.

Bob, the Janitor

theSceneOfTheCrime =
    bracket 
        (runDB startProcess) 
        (\processId -> runDB (closeProcess processId)) 
        $ \processId -> do
            doWorkWith processId
            {- ... snip ... -}

There’s a great big mess - it appears that someone was thrown from a high building! Foul play is suspected from the initial detective work. But after the excitement dies down, the janitor, Bob, is left to clean up the mess.

One of the perks of being a janitor is protection from all sorts of evil. While you’re cleaning stuff up, nothing spooky can harm you - no async exceptions are allowd. You might expect there’s a loophole here, but it’s fool proof. It’s such a strong protection that the janitor is even able to bestow it upon anyone that works for him to help clean up.

Bob begins cleaning up by recording the work he’s doing in the database. To do this, he requests a database connection from Mr Database. However, this provides Mr Database with the same protections: no one can kill him, or anyone that works for him!

Now, by the particular and odd rules of this protection magic, you don’t have to know that someone is working for you. So the phantom tracker that Alice set up is similarly extended this protection.

Mr Database provides the database connection to Bob in a prompt manner, and Bob completes his task. However, when Bob attempts to release the database back, he can’t! The database connection is permanently stuck to his hand. Mr Database can’t accept it back and put it in the pool, and he can’t continue to his next job. The entire application comes grinding to a halt, as no one can access the database.

What kind of bizarre curse is this?

The Gift of Safety

withAsync wants to be safe - it wants to guarantee that the forked thread is killed when the block exits. It accomplishes this by effectively doing:

withAsync thread action = 
    bracket
        (async thread)
        uninterruptibleCancel
        action

async forks the thread and prepares the Async:

async action = do
   var <- newEmptyTMVarIO
   threadId <- mask $ \restore ->
          forkIO $ try (restore action) >>= atomically . putTMVar var
   return Async 
      { asyncThreadId = threadId 
      , _asyncWait = readTMVar var
      }

async is careful to mask the forkIO call, which ensures that the forked thread is masked. That allows action to receive async exceptions, but outside of action, it’s guaranteed that if try succeeds, then the atomically . putTMVar var also succeeds. Since try will catch async exceptions, this means that the async exception will definitely be registered in the putTMVar call.

uninterruptibleCancel cancels the thread in an uninterruptible state. cancel waits for the thread to complete - either with an exception or a real value.

Meanwhile, bracket is also cursed with safety:

module UnliftIO.Exception where

bracket make clean action = 
    withRunInIO $ \runInIO ->
        Control.Exception.bracket
            (runInIO make)
            (\a -> uninterruptibleMask_ $ runInIO $ clean a)
            (\a -> runInIO $ action a)

The Curse of Two Gifts

Unspeakable magical rules dictate that two gifts form a curse, under the usual laws for associativity and commutativity.

To understand what’s going on, we start by inlining the bracket.

crimeSceneCleanedUp =
    withRunInIO $ \runInIO ->
    bracket
        (runInIO $ runDB createProcess)
        (\pid -> 
            uninterruptibleMask_ $ do
                runInIO $ runDB $ do
                    closeProcess pid
        )
        _stuff

We know that the make and action managed to complete, so we’re interested in the cleanup. Let’s expand runDB annd omit some noise:

crimeSceneCleanedUp =
    withRunInIO $ \runInIO ->
           
                                       
                 
            uninterruptibleMask_ $ do
                runInIO $ do
                    sqlPool <- getSqlPool
                    withAcquisitionTimer $ \stop ->
                        flip runSqlPool sqlPool $ do
                            stop 
                            closeProcess pid

Hmm! That withAcqusitionTimer is new! Enhance!!

crimeSceneCleanedUp =
    withRunInIO $ \runInIO ->
           
                                       
                 
            uninterruptibleMask_ $ do
                runInIO $ do
                    sqlPool <- getSqlPool
                    
                    withAsync (task `finally` record) $ \async ->
                        flip runSqlPool sqlPool $ do
                        cancel async 
                        closeProcess pid

Uh oh. Let’s zoom in on withAsync (and get rid of some indentation):

crimeSceneCleanedUp =
    uninterruptibleMask_ $ do
        sqlPool <- getSqlPool
        
        bracket 
            (async (task `finally` record))
            (uninterruptibleCancel)
            $ \async ->
            flip runSqlPool sqlPool $ do
                cancel async 
                closeProcess pid

One more level!

crimeSceneCleanedUp =
    uninterruptibleMask_ $ do
        sqlPool <- getSqlPool
        
        bracket 
            (do
                var <- newEmptyTMVarIO
                threadId <- mask $ \restore ->
                    forkIO $ do
                        eres <- try $ restore $ 
                            task `finally` record 
                        atomically $ putTMVar var eres
                return Async 
                    { asyncThreadId = threadId 
                    , _asyncWait = readTMVar var
                    }
            uninterruptibleCancel
            $ \async ->
            flip runSqlPool sqlPool $ do
                cancel async 
                closeProcess pid

Uh oh. forkIO inherits the masking state from the parent thread. This means that uninterruptibleMask_ state, set by bracket’s cleanup, is inherited by our forkIO.

Let’s zoom back out on that async call and inline the task…

crimeSceneCleanedUp =
    uninterruptibleMask_ $ do
        withAsync 
            (do
                forever $ do
                    threadDelay 1000
                    {- hmm -}
             `finally` record) $ \async ->
            {- snip -}

Ah! That’s the zombie. Reducing it to it’s most basic nature, we have:

zombie :: IO (Async a)
zombie =
    uninterruptibleMask_ $
        async $ 
            forever $ 
                threadDelay 1000

uninteruptibleMask_ means “I cannot be killed by async exceptions.” async allows the forked thread to inherit the masking state of the parent. But about half of the API of async requires that the forked thread can be killed by async exceptions. race is completely broken with unkillable Asyncs.

The solution is to use withAsyncWithUnmask:

safeWithAsync thread action =
    withAsyncWithUnmask (\unmask -> unmask thread) action

This unmasks the child thread, revealing it to be an imposter all along.

And I would have ~gotten away with it~ never exited and consumed all resources, if it weren’t for you danged kids!!!

The unmasked phantom thread, free from it’s curse of safety, was killed and returned to the phantom aether to be called upon in other sorcery.

October 29, 2022 12:00 AM

GHC activities report: August-September 2022

This is the fourteenth edition of our GHC activities report, which describes the work on GHC and related projects that we are doing at Well-Typed. The current edition covers roughly the months of August and September 2022. You can find the previous editions collected under the ghc-activities-report tag.

A bit of background: One aspect of our work at Well-Typed is to support GHC and the Haskell core infrastructure. Several companies, including IOHK and GitHub via the Haskell Foundation, are providing us with funding to do this work. We are also working with Hasura on better debugging tools and improvements to HLS. We are very grateful on behalf of the whole Haskell community for the support these companies provide.

If you are interested in also contributing funding to ensure we can continue or even scale up this kind of work, please get in touch.

Of course, GHC is a large community effort, and Well-Typed’s contributions are just a small part of this. This report does not aim to give an exhaustive picture of all GHC work that is ongoing, and there are many fantastic features currently being worked on that are omitted here simply because none of us are currently involved in them in any way. Furthermore, the aspects we do mention are still the work of many people. In many cases, we have just been helping with the last few steps of integration. We are immensely grateful to everyone contributing to GHC!

Team

The current GHC team consists of Ben Gamari, Andreas Klebinger, Matthew Pickering, Zubin Duggal and Sam Derbyshire. Many others within Well-Typed are contributing to GHC more occasionally.

Releases

• August and September were quiet months due to holidays and now our attention is turning to the forthcoming 9.4.3, 9.2.5 releases and 9.6 branch.

• Zubin has been preparing GHC 9.2.5 and backporting critical runtime performance fixes like #21755 to the branch.

Driver

• Matt finished an extension to interface files which allows the whole core program to be stored in an interface file. This improves restart times of GHCi and can massively improve compilation times of projects involving many Template Haskell splices. (!7502)

• Matt investigated a number of issues to do with interface file determinism and added some CI jobs to try to check that we are producing deterministic interfaces. (!8895)

Compiler performance

• Andreas investigated the benefit of being less aggressive in pruning specializations in #18532, where it turned out the current behaviour is already optimal.

• Andreas investigated GHC and core lint performance in #22200. This resulted in !9055 where a few key improvements improved compile times for builds using -dcore-lint by ~15% in the common case and ~30% in edge cases.

• Matt did another round of space usage investigation and fixed a number of leaks in the simplifier. These changes are most obvious when compiling very large modules. The fixes focused on making sure we didn’t retain old bindings across simplifier passes. (#22102, !8896)

Typechecker

• Sam improved how GHC picks Given quantified constraints when trying to solve a Wanted constraint, by picking the quantified constraint with the weakest precondition (if one exists). This fixes #22216 and #22223.

Error messages

• Sam finalised and landed a patch adding error codes to error messages (!8849). All errors and warnings that GHC emits using the new diagnostic infrastructure now come with an associated unique code, e.g. error: [GHC-53633] Pattern match is redundant. These can then be used for looking up documentation, for example in the Haskell Error Index. This is part of a Haskell Foundation proposal.

Code generation

• Andreas changed the tag inference pass to apply in a few more situations in !8747. In particular, code returning variables that are statically known to be properly tagged, as well as dataToTag, benefit from this change and will produce more efficient code.

• Ben and Andreas fixed code generation bug #21968 which sometimes caused incorrect results when compiling without optimization.

• Andreas fixed #22042 where GHC sometimes produced invalid bytecode inside GHCi.

• Ben fixed a bug in code generation for intMulMayOflo# on AArch64 (#21624) and updated test-primops to exercise the affected codepath.

• Ben fixed a bug in code generation on x86_64 (#21968) where under some conditions a switch discriminator could clobber a live value.

• Ben fixed a bug in the LLVM code generator which would break GHC-generated initializers. (#22019)

Core-to-Core pipeline

• Andreas investigated #21960 about regressions in the 9.2/9.4 point releases. They were tracked back to the simple fix for #21694. Simon Peyton Jones provided a more robust solution in !8862.

• Andreas identified #22075 where GHC would sometimes enter a infinite loop while compiling a program involving recursive top level bindings which Simon Peyton Jones then fixed in !8905.

Runtime system

• Ben fixed an bug in newArrayArray# in 9.2 where zero-sized arrays would integer underflow when initializing the card array. (#21962)
• Ben continued work in teaching the runtime linker about constructor/deconstructor priorities, improving reliability of interoperation with C++ code. (#21947)
• Ben diagnosed and fixed a bug in the nonmoving collector where objects could be inappropriately scavenged. (#21885)

Profiling

• Ben reworked GHC’s handling of IPE information, significantly reducing the on-disk size and improving initialization efficiency. (!8868)

Libraries

• Ben finished and merged his thread introspection branch, allowing user programs to enumerate the threads of a program and query the label, state, and stack of each. (!2816)
• Ben reworked the exception provenance proposal and rewrote his prototype implementation.

Packaging

• Ben fixed a number of packaging issues (#21901, #21965, #21713, #21974, #21506, #21956, #21988, #21976, #21974) and worked to improve CI to ensure that such regressions are caught in the future.

• Matt fixed a number of packaging issues to do with Hackage documentation and added CI jobs which generate documentation suitable for upload to Hackage. (!8846, !8841)

Hadrian

• Matt improved Hadrian build times by increasing the amount of parallelism available. On a full build the total time is 75% of the time before these patches. (!8879)
• Sam made some improvements to Hadrian bootstrapping on Windows.

Infrastructure

• Ben worked to fix various CI issues (#21986) and began work on testing cross-compilers under CI. (#21480)
• Ben finished his work removing the make build system from GHC’s source tree, dropping over 10kLoC from the repository. (#17527)
• Ben looked into the feasibility of notarizing macOS binary distributions. (#17418)

by ben, andreask, matthew, zubin, sam at October 27, 2022 12:00 AM

Domains, Sets, Traversals and Applicatives

Last time I looked at free monoids, and noticed that in Haskell lists don't really cut it. This is a consequence of laziness and general recursion. To model a language with those properties, one needs to use domains and monotone, continuous maps, rather than sets and total functions (a call-by-value language with general recursion would use domains and strict maps instead).

This time I'd like to talk about some other examples of this, and point out how doing so can (perhaps) resolve some disagreements that people have about the specific cases.

The first example is not one that I came up with: induction. It's sometimes said that Haskell does not have inductive types at all, or that we cannot reason about functions on its data types by induction. However, I think this is (techincally) inaccurate. What's true is that we cannot simply pretend that that our types are sets and use the induction principles for sets to reason about Haskell programs. Instead, one has to figure out what inductive domains would be, and what their proof principles are.

Fortunately, there are some papers about doing this. The most recent (that I'm aware of) is Generic Fibrational Induction. I won't get too into the details, but it shows how one can talk about induction in a general setting, where one has a category that roughly corresponds to the type theory/programming language, and a second category of proofs that is 'indexed' by the first category's objects. Importantly, it is not required that the second category is somehow 'part of' the type theory being reasoned about, as is often the case with dependent types, although that is also a special case of their construction.

One of the results of the paper is that this framework can be used to talk about induction principles for types that don't make sense as sets. Specifically:

 
newtype Hyp = Hyp ((Hyp -> Int) -> Int)
 

the type of "hyperfunctions". Instead of interpreting this type as a set, where it would effectively require a set that is isomorphic to the power set of its power set, they interpret it in the category of domains and strict functions mentioned earlier. They then construct the proof category in a similar way as one would for sets, except instead of talking about predicates as subsets, we talk about sub-domains instead. Once this is done, their framework gives a notion of induction for this type.

This example is suitable for ML (and suchlike), due to the strict functions, and sort of breaks the idea that we can really get away with only thinking about sets, even there. Sets are good enough for some simple examples (like flat domains where we don't care about ⊥), but in general we have to generalize induction itself to apply to all types in the 'good' language.

While I haven't worked out how the generic induction would work out for Haskell, I have little doubt that it would, because ML actually contains all of Haskell's data types (and vice versa). So the fact that the framework gives meaning to induction for ML implies that it does so for Haskell. If one wants to know what induction for Haskell's 'lazy naturals' looks like, they can study the ML analogue of:

 
data LNat = Zero | Succ (() -> LNat)
 

because function spaces lift their codomain, and make things 'lazy'.

----

The other example I'd like to talk about hearkens back to the previous article. I explained how foldMap is the proper fundamental method of the Foldable class, because it can be massaged to look like:

 
foldMap :: Foldable f => f a -> FreeMonoid a
 

and lists are not the free monoid, because they do not work properly for various infinite cases.

I also mentioned that foldMap looks a lot like traverse:

 
foldMap  :: (Foldable t   , Monoid m)      => (a -> m)   -> t a -> m
traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
 

And of course, we have Monoid m => Applicative (Const m), and the functions are expected to agree in this way when applicable.

Now, people like to get in arguments about whether traversals are allowed to be infinite. I know Ed Kmett likes to argue that they can be, because he has lots of examples. But, not everyone agrees, and especially people who have papers proving things about traversals tend to side with the finite-only side. I've heard this includes one of the inventors of Traversable, Conor McBride.

In my opinion, the above disagreement is just another example of a situation where we have a generic notion instantiated in two different ways, and intuition about one does not quite transfer to the other. If you are working in a language like Agda or Coq (for proving), you will be thinking about traversals in the context of sets and total functions. And there, traversals are finite. But in Haskell, there are infinitary cases to consider, and they should work out all right when thinking about domains instead of sets. But I should probably put forward some argument for this position (and even if I don't need to, it leads somewhere else interesting).

One example that people like to give about finitary traversals is that they can be done via lists. Given a finite traversal, we can traverse to get the elements (using Const [a]), traverse the list, then put them back where we got them by traversing again (using State [a]). Usually when you see this, though, there's some subtle cheating in relying on the list to be exactly the right length for the second traversal. It will be, because we got it from a traversal of the same structure, but I would expect that proving the function is actually total to be a lot of work. Thus, I'll use this as an excuse to do my own cheating later.

Now, the above uses lists, but why are we using lists when we're in Haskell? We know they're deficient in certain ways. It turns out that we can give a lot of the same relevant structure to the better free monoid type:

 
newtype FM a = FM (forall m. Monoid m => (a -> m) -> m) deriving (Functor)
 
instance Applicative FM where
  pure x = FM ($ x)
  FM ef < *> FM ex = FM $ \k -> ef $ \f -> ex $ \x -> k (f x)
 
instance Monoid (FM a) where
  mempty = FM $ \_ -> mempty
  mappend (FM l) (FM r) = FM $ \k -> l k <> r k
 
instance Foldable FM where
  foldMap f (FM e) = e f
 
newtype Ap f b = Ap { unAp :: f b }
 
instance (Applicative f, Monoid b) => Monoid (Ap f b) where
  mempty = Ap $ pure mempty
  mappend (Ap l) (Ap r) = Ap $ (<>) < $> l < *> r
 
instance Traversable FM where
  traverse f (FM e) = unAp . e $ Ap . fmap pure . f
 

So, free monoids are Monoids (of course), Foldable, and even Traversable. At least, we can define something with the right type that wouldn't bother anyone if it were written in a total language with the right features, but in Haskell it happens to allow various infinite things that people don't like.

Now it's time to cheat. First, let's define a function that can take any Traversable to our free monoid:

 
toFreeMonoid :: Traversable t => t a -> FM a
toFreeMonoid f = FM $ \k -> getConst $ traverse (Const . k) f
 

Now let's define a Monoid that's not a monoid:

 
data Cheat a = Empty | Single a | Append (Cheat a) (Cheat a)
 
instance Monoid (Cheat a) where
  mempty = Empty
  mappend = Append
 

You may recognize this as the data version of the free monoid from the previous article, where we get the real free monoid by taking a quotient. using this, we can define an Applicative that's not valid:

 
newtype Cheating b a =
  Cheating { prosper :: Cheat b -> a } deriving (Functor)
 
instance Applicative (Cheating b) where
  pure x = Cheating $ \_ -> x
 
  Cheating f < *> Cheating x = Cheating $ \c -> case c of
    Append l r -> f l (x r)
 

Given these building blocks, we can define a function to relabel a traversable using a free monoid:

 
relabel :: Traversable t => t a -> FM b -> t b
relabel t (FM m) = propser (traverse (const hope) t) (m Single)
 where
 hope = Cheating $ \c -> case c of
   Single x -> x
 

And we can implement any traversal by taking a trip through the free monoid:

 
slowTraverse
  :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
slowTraverse f t = fmap (relabel t) . traverse f . toFreeMonoid $ t
 

And since we got our free monoid via traversing, all the partiality I hid in the above won't blow up in practice, rather like the case with lists and finite traversals.

Arguably, this is worse cheating. It relies on the exact association structure to work out, rather than just number of elements. The reason is that for infinitary cases, you cannot flatten things out, and there's really no way to detect when you have something infinitary. The finitary traversals have the luxury of being able to reassociate everything to a canonical form, while the infinite cases force us to not do any reassociating at all. So this might be somewhat unsatisfying.

But, what if we didn't have to cheat at all? We can get the free monoid by tweaking foldMap, and it looks like traverse, so what happens if we do the same manipulation to the latter?

It turns out that lens has a type for this purpose, a slight specialization of which is:

 
newtype Bazaar a b t =
  Bazaar { runBazaar :: forall f. Applicative f => (a -> f b) -> f t }
 

Using this type, we can reorder traverse to get:

 
howBizarre :: Traversable t => t a -> Bazaar a b (t b)
howBizarre t = Bazaar $ \k -> traverse k t
 

But now, what do we do with this? And what even is it? [1]

If we continue drawing on intuition from Foldable, we know that foldMap is related to the free monoid. Traversable has more indexing, and instead of Monoid uses Applicative. But the latter are actually related to the former; Applicatives are monoidal (closed) functors. And it turns out, Bazaar has to do with free Applicatives.

If we want to construct free Applicatives, we can use our universal property encoding trick:

 
newtype Free p f a =
  Free { gratis :: forall g. p g => (forall x. f x -> g x) -> g a }
 

This is a higher-order version of the free p, where we parameterize over the constraint we want to use to represent structures. So Free Applicative f is the free Applicative over a type constructor f. I'll leave the instances as an exercise.

Since free monoid is a monad, we'd expect Free p to be a monad, too. In this case, it is a McBride style indexed monad, as seen in The Kleisli Arrows of Outrageous Fortune.

 
type f ~> g = forall x. f x -> g x
 
embed :: f ~> Free p f
embed fx = Free $ \k -> k fx
 
translate :: (f ~> g) -> Free p f ~> Free p g
translate tr (Free e) = Free $ \k -> e (k . tr)
 
collapse :: Free p (Free p f) ~> Free p f
collapse (Free e) = Free $ \k -> e $ \(Free e') -> e' k
 

That paper explains how these are related to Atkey style indexed monads:

 
data At key i j where
  At :: key -> At key i i
 
type Atkey m i j a = m (At a j) i
 
ireturn :: IMonad m => a -> Atkey m i i a
ireturn = ...
 
ibind :: IMonad m => Atkey m i j a -> (a -> Atkey m j k b) -> Atkey m i k b
ibind = ...
 

It turns out, Bazaar is exactly the Atkey indexed monad derived from the Free Applicative indexed monad (with some arguments shuffled) [2]:

 
hence :: Bazaar a b t -> Atkey (Free Applicative) t b a
hence bz = Free $ \tr -> runBazaar bz $ tr . At
 
forth :: Atkey (Free Applicative) t b a -> Bazaar a b t
forth fa = Bazaar $ \g -> gratis fa $ \(At a) -> g a
 
imap :: (a -> b) -> Bazaar a i j -> Bazaar b i j
imap f (Bazaar e) = Bazaar $ \k -> e (k . f)
 
ipure :: a -> Bazaar a i i
ipure x = Bazaar ($ x)
 
(>>>=) :: Bazaar a j i -> (a -> Bazaar b k j) -> Bazaar b k i
Bazaar e >>>= f = Bazaar $ \k -> e $ \x -> runBazaar (f x) k
 
(>==>) :: (s -> Bazaar i o t) -> (i -> Bazaar a b o) -> s -> Bazaar a b t
(f >==> g) x = f x >>>= g
 

As an aside, Bazaar is also an (Atkey) indexed comonad, and the one that characterizes traversals, similar to how indexed store characterizes lenses. A Lens s t a b is equivalent to a coalgebra s -> Store a b t. A traversal is a similar Bazaar coalgebra:

 
  s -> Bazaar a b t
    ~
  s -> forall f. Applicative f => (a -> f b) -> f t
    ~
  forall f. Applicative f => (a -> f b) -> s -> f t
 

It so happens that Kleisli composition of the Atkey indexed monad above (>==>) is traversal composition.

Anyhow, Bazaar also inherits Applicative structure from Free Applicative:

 
instance Functor (Bazaar a b) where
  fmap f (Bazaar e) = Bazaar $ \k -> fmap f (e k)
 
instance Applicative (Bazaar a b) where
  pure x = Bazaar $ \_ -> pure x
  Bazaar ef < *> Bazaar ex = Bazaar $ \k -> ef k < *> ex k
 

This is actually analogous to the Monoid instance for the free monoid; we just delegate to the underlying structure.

The more exciting thing is that we can fold and traverse over the first argument of Bazaar, just like we can with the free monoid:

 
bfoldMap :: Monoid m => (a -> m) -> Bazaar a b t -> m
bfoldMap f (Bazaar e) = getConst $ e (Const . f)
 
newtype Comp g f a = Comp { getComp :: g (f a) } deriving (Functor)
 
instance (Applicative f, Applicative g) => Applicative (Comp g f) where
  pure = Comp . pure . pure
  Comp f < *> Comp x = Comp $ liftA2 (< *>) f x
 
btraverse
  :: (Applicative f) => (a -> f a') -> Bazaar a b t -> Bazaar a' b t
btraverse f (Bazaar e) = getComp $ e (c . fmap ipure . f)
 

This is again analogous to the free monoid code. Comp is the analogue of Ap, and we use ipure in traverse. I mentioned that Bazaar is a comonad:

 
extract :: Bazaar b b t -> t
extract (Bazaar e) = runIdentity $ e Identity
 

And now we are finally prepared to not cheat:

 
honestTraverse
  :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)
honestTraverse f = fmap extract . btraverse f . howBizarre
 

So, we can traverse by first turning out Traversable into some structure that's kind of like the free monoid, except having to do with Applicative, traverse that, and then pull a result back out. Bazaar retains the information that we're eventually building back the same type of structure, so we don't need any cheating.

To pull this back around to domains, there's nothing about this code to object to if done in a total language. But, if we think about our free Applicative-ish structure, in Haskell, it will naturally allow infinitary expressions composed of the Applicative operations, just like the free monoid will allow infinitary monoid expressions. And this is okay, because some Applicatives can make sense of those, so throwing them away would make the type not free, in the same way that even finite lists are not the free monoid in Haskell. And this, I think, is compelling enough to say that infinite traversals are right for Haskell, just as they are wrong for Agda.

For those who wish to see executable code for all this, I've put a files here and here. The latter also contains some extra goodies at the end that I may talk about in further installments.

[1] Truth be told, I'm not exactly sure.

[2] It turns out, you can generalize Bazaar to have a correspondence for every choice of p

 
newtype Bizarre p a b t =
  Bizarre { bizarre :: forall f. p f => (a -> f b) -> f t }
 

hence and forth above go through with the more general types. This can be seen here.

by Dan Doel at October 24, 2022 05:47 PM

Free Monoids in Haskell

It is often stated that Foldable is effectively the toList class. However, this turns out to be wrong. The real fundamental member of Foldable is foldMap (which should look suspiciously like traverse, incidentally). To understand exactly why this is, it helps to understand another surprising fact: lists are not free monoids in Haskell.

This latter fact can be seen relatively easily by considering another list-like type:

 
data SL a = Empty | SL a :> a
 
instance Monoid (SL a) where
  mempty = Empty
  mappend ys Empty = ys
  mappend ys (xs :> x) = (mappend ys xs) :> x
 
single :: a -> SL a
single x = Empty :> x
 

So, we have a type SL a of snoc lists, which are a monoid, and a function that embeds a into SL a. If (ordinary) lists were the free monoid, there would be a unique monoid homomorphism from lists to snoc lists. Such a homomorphism (call it h) would have the following properties:

 
h [] = Empty
h (xs <> ys) = h xs <> h ys
h [x] = single x
 

And in fact, this (together with some general facts about Haskell functions) should be enough to define h for our purposes (or any purposes, really). So, let's consider its behavior on two values:

 
h [1] = single 1
 
h [1,1..] = h ([1] <> [1,1..]) -- [1,1..] is an infinite list of 1s
          = h [1] <> h [1,1..]
 

This second equation can tell us what the value of h is at this infinite value, since we can consider it the definition of a possibly infinite value:

 
x = h [1] <> x = fix (single 1 <>)
h [1,1..] = x
 

(single 1 ) is a strict function, so the fixed point theorem tells us that x = ⊥.

This is a problem, though. Considering some additional equations:

 
[1,1..] <> [n] = [1,1..] -- true for all n
h [1,1..] = ⊥
h ([1,1..] <> [1]) = h [1,1..] <> h [1]
                   = ⊥ <> single 1
                   = ⊥ :> 1
                   ≠ ⊥
 

So, our requirements for h are contradictory, and no such homomorphism can exist.

The issue is that Haskell types are domains. They contain these extra partially defined values and infinite values. The monoid structure on (cons) lists has infinite lists absorbing all right-hand sides, while the snoc lists are just the opposite.

This also means that finite lists (or any method of implementing finite sequences) are not free monoids in Haskell. They, as domains, still contain the additional bottom element, and it absorbs all other elements, which is incorrect behavior for the free monoid:

 
pure x <> ⊥ = ⊥
h ⊥ = ⊥
h (pure x <> ⊥) = [x] <> h ⊥
                = [x] ++ ⊥
                = x:⊥
                ≠ ⊥
 

So, what is the free monoid? In a sense, it can't be written down at all in Haskell, because we cannot enforce value-level equations, and because we don't have quotients. But, if conventions are good enough, there is a way. First, suppose we have a free monoid type FM a. Then for any other monoid m and embedding a -> m, there must be a monoid homomorphism from FM a to m. We can model this as a Haskell type:

 
forall a m. Monoid m => (a -> m) -> FM a -> m
 

Where we consider the Monoid m constraint to be enforcing that m actually has valid monoid structure. Now, a trick is to recognize that this sort of universal property can be used to define types in Haskell (or, GHC at least), due to polymorphic types being first class; we just rearrange the arguments and quantifiers, and take FM a to be the polymorphic type:

 
newtype FM a = FM { unFM :: forall m. Monoid m => (a -> m) -> m }
 

Types defined like this are automatically universal in the right sense. [1] The only thing we have to check is that FM a is actually a monoid over a. But that turns out to be easily witnessed:

 
embed :: a -> FM a
embed x = FM $ \k -> k x
 
instance Monoid (FM a) where
  mempty = FM $ \_ -> mempty
  mappend (FM e1) (FM e2) = FM $ \k -> e1 k <> e2 k
 

Demonstrating that the above is a proper monoid delegates to instances of Monoid being proper monoids. So as long as we trust that convention, we have a free monoid.

However, one might wonder what a free monoid would look like as something closer to a traditional data type. To construct that, first ignore the required equations, and consider only the generators; we get:

 
data FMG a = None | Single a | FMG a :<> FMG a
 

Now, the proper FM a is the quotient of this by the equations:

 
None :<> x = x = x :<> None
x :<> (y :<> z) = (x :<> y) :<> z
 

One way of mimicking this in Haskell is to hide the implementation in a module, and only allow elimination into Monoids (again, using the convention that Monoid ensures actual monoid structure) using the function:

 
unFMG :: forall a m. Monoid m => FMG a -> (a -> m) -> m
unFMG None _ = mempty
unFMG (Single x) k = k x
unFMG (x :<> y) k = unFMG x k <> unFMG y k
 

This is actually how quotients can be thought of in richer languages; the quotient does not eliminate any of the generated structure internally, it just restricts the way in which the values can be consumed. Those richer languages just allow us to prove equations, and enforce properties by proof obligations, rather than conventions and structure hiding. Also, one should note that the above should look pretty similar to our encoding of FM a using universal quantification earlier.

Now, one might look at the above and have some objections. For one, we'd normally think that the quotient of the above type is just [a]. Second, it seems like the type is revealing something about the associativity of the operations, because defining recursive values via left nesting is different from right nesting, and this difference is observable by extracting into different monoids. But aren't monoids supposed to remove associativity as a concern? For instance:

 
ones1 = embed 1 <> ones1
ones2 = ones2 <> embed 1
 

Shouldn't we be able to prove these are the same, becuase of an argument like:

 
ones1 = embed 1 <> (embed 1 <> ...)
      ... reassociate ...
      = (... <> embed 1) <> embed 1
      = ones2
 

The answer is that the equation we have only specifies the behavior of associating three values:

 
x <> (y <> z) = (x <> y) <> z
 

And while this is sufficient to nail down the behavior of finite values, and finitary reassociating, it does not tell us that infinitary reassociating yields the same value back. And the "... reassociate ..." step in the argument above was decidedly infinitary. And while the rules tell us that we can peel any finite number of copies of embed 1 to the front of ones1 or the end of ones2, it does not tell us that ones1 = ones2. And in fact it is vital for FM a to have distinct values for these two things; it is what makes it the free monoid when we're dealing with domains of lazy values.

Finally, we can come back to Foldable. If we look at foldMap:

 
foldMap :: (Foldable f, Monoid m) => (a -> m) -> f a -> m
 

we can rearrange things a bit, and get the type:

 
Foldable f => f a -> (forall m. Monoid m => (a -> m) -> m)
 

And thus, the most fundamental operation of Foldable is not toList, but toFreeMonoid, and lists are not free monoids in Haskell.

[1]: What we are doing here is noting that (co)limits are objects that internalize natural transformations, but the natural transformations expressible by quantification in GHC are already automatically internalized using quantifiers. However, one has to be careful that the quantifiers are actually enforcing the relevant naturality conditions. In many simple cases they are.

by Dan Doel at October 24, 2022 05:47 PM

Fast Circular Substitution

Emil Axelsson and Koen Claessen wrote a functional pearl last year about Using Circular Programs for Higher-Order Syntax.

About 6 months ago I had an opportunity to play with this approach in earnest, and realized we can speed it up a great deal. This has kept coming up in conversation ever since, so I've decided to write up an article here.

In my bound library I exploit the fact that monads are about substitution to make a monad transformer that manages substitution for me.

Here I'm going to take a more coupled approach.

To have a type system with enough complexity to be worth examining, I'll adapt Dan Doel's UPTS, which is a pure type system with universe polymorphism. I won't finish the implementation here, but from where we get it should be obvious how to finish the job.

Unlike Axelsson and Claessen I'm not going to bother to abstract over my name representation.

To avoid losing the original name from the source, we'll just track names as strings with an integer counting the number of times it has been 'primed'. The name is purely for expository purposes, the real variable identifier is the number. We'll follow the Axelsson and Claessen convention of having the identifier assigned to each binder be larger than any one bound inside of it. If you don't need he original source names you can cull them from the representation, but they can be useful if you are representing a syntax tree for something you parsed and/or that you plan to pretty print later.

 
data Name = Name String Int
   deriving (Show,Read)
 
hint :: Name -> String
hint (Name n _) = n
 
nameId :: Name -> Int
nameId (Name _ i) = i
 
instance Eq Name where
  (==) = (==) `on` nameId
 
instance Ord Name where
  compare = compare `on` nameId
 
prime :: String -> Int -> Name
prime n i = Name n (i + 1)
 

So what is the language I want to work with?

 
type Level = Int
 
data Constant
  = Level
  | LevelLiteral {-# UNPACK #-} !Level
  | Omega
  deriving (Eq,Ord,Show,Read,Typeable)
 
data Term a
  = Free a
  | Bound {-# UNPACK #-} !Name
  | Constant !Constant
  | Term a :+ {-# UNPACK #-} !Level
  | Max  [Term a]
  | Type !(Term a)
  | Lam   {-# UNPACK #-} !Name !(Term a) !(Term a)
  | Pi    {-# UNPACK #-} !Name !(Term a) !(Term a)
  | Sigma {-# UNPACK #-} !Name !(Term a) !(Term a)
  | App !(Term a) !(Term a)
  | Fst !(Term a)
  | Snd !(Term a)
  | Pair !(Term a) !(Term a) !(Term a)
  deriving (Show,Read,Eq,Ord,Functor,Foldable,Traversable,Typeable)
 

That is perhaps a bit paranoid about remaining strict, but it seemed like a good idea at the time.

We can define capture avoiding substitution on terms:

 
subst :: Eq a => a -> Term a -> Term a -> Term a
subst a x y = y >>= \a' ->
  if a == a'
    then x
    else return a'
 

Now we finally need to implement Axelsson and Claessen's circular programming trick. Here we'll abstract over terms that allow us to find the highest bound value within them:

 
class Bindable t where
  bound :: t -> Int
 

and instantiate it for our Term type

 
instance Bindable (Term a) where
  bound Free{}        = 0
  bound Bound{}       = 0 -- intentional!
  bound Constant{}    = 0
  bound (a :+ _)      = bound a
  bound (Max xs)      = foldr (\a r -> bound a `max` r) 0 xs
  bound (Type t)      = bound t
  bound (Lam b t _)   = nameId b `max` bound t
  bound (Pi b t _)    = nameId b `max` bound t
  bound (Sigma b t _) = nameId b `max` bound t
  bound (App x y)     = bound x `max`  bound y
  bound (Fst t)       = bound t
  bound (Snd t)       = bound t
  bound (Pair t x y)  = bound t `max` bound x `max` bound y
 

As in the original pearl we avoid traversing into the body of the binders, hence the _'s in the code above.

Now we can abstract over the pattern used to create a binder in the functional pearl, since we have multiple binder types in this syntax tree, and the code would get repetitive.

 
binder :: Bindable t =>
  (Name -> t) ->
  (Name -> t -> r) ->
  String -> (t -> t) -> r
binder bd c n e = c b body where
  body = e (bd b)
  b = prime n (bound body)
 
lam, pi, sigma :: String -> Term a -> (Term a -> Term a) -> Term a
lam s t   = binder Bound (`Lam` t) s
pi s t    = binder Bound (`Pi` t) s
sigma s t = binder Bound (`Sigma` t) s
 

We may not always want to give names to the variables we capture, so let's define:

lam_, pi_, sigma_ :: Term a -> (Term a -> Term a) -> Term a
lam_   = lam "_"
pi_    = pi "_"
sigma_ = sigma "_"

Now, here's the interesting part. The problem with Axelsson and Claessen's original trick is that every substitution is being handled separately. This means that if you were to write a monad for doing substitution with it, it'd actually be quite slow. You have to walk the syntax tree over and over and over.

We can fuse these together by making a single pass:

 
instantiate :: Name -> t -> IntMap t -> IntMap t
instantiate = IntMap.insert . nameId
 
rebind :: IntMap (Term b) -> Term a -> (a -> Term b) -> Term b
rebind env xs0 f = go xs0 where
  go = \case
    Free a       -> f a
    Bound b      -> env IntMap.! nameId b
    Constant c   -> Constant c
    m :+ n       -> go m :+ n
    Type t       -> Type (go t)
    Max xs       -> Max (fmap go xs)
    Lam b t e    -> lam   (hint b) (go t) $ \v ->
      rebind (instantiate b v env) e f
    Pi b t e     -> pi    (hint b) (go t) $ \v ->
      rebind (instantiate b v env) e f
    Sigma b t e  -> sigma (hint b) (go t) $ \v ->
      rebind (instantiate b v env) e f
    App x y      -> App (go x) (go y)
    Fst x        -> Fst (go x)
    Snd x        -> Snd (go x)
    Pair t x y   -> Pair (go t) (go x) (go y)
 

Note that the Lam, Pi and Sigma cases just extend the current environment.

With that now we can upgrade the pearl's encoding to allow for an actual Monad in the same sense as bound.

 
instance Applicative Term where
  pure = Free
  (< *>) = ap
 
instance Monad Term where
  return = Free
  (>>=) = rebind IntMap.empty
 

To show that we can work with this syntax tree representation, let's write an evaluator from it to weak head normal form:

First we'll need some helpers:

 
apply :: Term a -> [Term a] -> Term a
apply = foldl App
 
rwhnf :: IntMap (Term a) ->
  [Term a] -> Term a -> Term a
rwhnf env stk     (App f x)
  = rwhnf env (rebind env x Free:stk) f
rwhnf env (x:stk) (Lam b _ e)
  = rwhnf (instantiate b x env) stk e
rwhnf env stk (Fst e)
  = case rwhnf env [] e of
  Pair _ e' _ -> rwhnf env stk e'
  e'          -> Fst e'
rwhnf env stk (Snd e)
  = case rwhnf env [] e of
  Pair _ _ e' -> rwhnf env stk e'
  e'          -> Snd e'
rwhnf env stk e
  = apply (rebind env e Free) stk
 

Then we can start off the whnf by calling our helper with an initial starting environment:

 
whnf :: Term a -> Term a
whnf = rwhnf IntMap.empty []
 

So what have we given up? Well, bound automatically lets you compare terms for alpha equivalence by quotienting out the placement of "F" terms in the syntax tree. Here we have a problem in that the identifiers we get assigned aren't necessarily canonical.

But we can get the same identifiers out by just using the monad above:

 
alphaEq :: Eq a => Term a -> Term a -> Bool
alphaEq = (==) `on` liftM id
 

It makes me a bit uncomfortable that our monad is only up to alpha equivalence and that liftM swaps out the identifiers used throughout the entire syntax tree, and we've also lost the ironclad protection against exotic terms.

But overall, this is a much faster version of Axelsson and Claessen's trick and it can be used as a drop-in replacement for something like bound in many cases, and unlike bound, it lets you use HOAS-style syntax for constructing lam, pi and sigma terms.

With pattern synonyms you can prevent the user from doing bad things as well. Once 7.10 ships you'd be able to use a bidirectional pattern synonym for Pi, Sigma and Lam to hide the real constructors behind. I'm not yet sure of the "best practices" in this area.

Here's the code all in one place:

[Download Circular.hs]

Happy Holidays,
-Edward

by Edward Kmett at October 24, 2022 05:47 PM

On the unsafety of interleaved I/O

One area where I'm at odds with the prevailing winds in Haskell is lazy I/O. It's often said that lazy I/O is evil, scary and confusing, and it breaks things like referential transparency. Having a soft spot for it, and not liking most of the alternatives, I end up on the opposite side when the topic comes up, if I choose to pick the fight. I usually don't feel like I come away from such arguments having done much good at giving lazy I/O its justice. So, I thought perhaps it would be good to spell out my whole position, so that I can give the best defense I can give, and people can continue to ignore it, without costing me as much time in the future. :)

So, what's the argument that lazy I/O, or unsafeInterleaveIO on which it's based, breaks referential transparency? It usually looks something like this:

 
swap (x, y) = (y, x)
 
setup = do
  r1 < - newIORef True
  r2 <- newIORef True
  v1 <- unsafeInterleaveIO $ do writeIORef r2 False ; readIORef r1
  v2 <- unsafeInterleaveIO $ do writeIORef r1 False ; readIORef r2
  return (v1, v2)
 
main = do
  p1 <- setup
  p2 <- setup
  print p1
  print . swap $ p2
 

I ran this, and got:

(True, False)
(True, False)

So this is supposed to demonstrate that the pure values depend on evaluation order, and we have broken a desirable property of Haskell.

First a digression. Personally I distinguish the terms, "referential transparency," and, "purity," and use them to identify two desirable properties of Haskell. The first I use for the property that allows you to factor your program by introducing (or eliminating) named subexpressions. So, instead of:

 
f e e
 

we are free to write:

 
let x = e in f x x
 

or some variation. I have no argument for this meaning, other than it's what I thought it meant when I first heard the term used with respect to Haskell, it's a useful property, and it's the best name I can think of for the property. I also (of course) think it's better than some of the other explanations you'll find for what people mean when they say Haskell has referential transparency, since it doesn't mention functions or "values". It's just about equivalence of expressions.

Anyhow, for me, the above example is in no danger of violating referential transparency. There is no factoring operation that will change the meaning of the program. I can even factor out setup (or inline it, since it's already named):

 
main = let m = setup
        in do p1 < - m
              p2 <- m
              print p1
              print . swap $ p2
 

This is the way in which IO preserves referential transparency, unlike side effects, in my view (note: the embedded language represented by IO does not have this property, since otherwise p1 could be used in lieu of p2; this is why you shouldn't spend much time writing IO stuff, because it's a bad language embedded in a good one).

The other property, "purity," I pull from Amr Sabry's paper, What is a Purely Functional Language? There he argues that a functional language should be considered "pure" if it is an extension of the lambda calculus in which there are no contexts which observe differences in evaluation order. Effectively, evaluation order must only determine whether or not you get an answer, not change the answer you get.

This is slightly different from my definition of referential transparency earlier, but it's also a useful property to have. Referential transparency tells us that we can freely refactor, and purity tells us that we can change the order things are evaluated, both without changing the meaning of our programs.

Now, it would seem that the original interleaving example violates purity. Depending on the order that the values are evaluated, opponents of lazy I/O say, the values change. However, this argument doesn't impress me, because I think the proper way to think about unsafeInterleaveIO is as concurrency, and in that case, it isn't very strange that the results of running it would be non-deterministic. And in that case, there's not much you can do to prove that the evaluation order is affecting results, and that you aren't simply very unlucky and always observing results that happen to correspond to evaluation order.

In fact, there's something I didn't tell you. I didn't use the unsafeInterleaveIO from base. I wrote my own. It looks like this:

 
unsafeInterleaveIO :: IO a -> IO a
unsafeInterleaveIO action = do
  iv < - new
  forkIO $
    randomRIO (1,5) >>= threadDelay . (*1000) >>
    action >>= write iv
  return . read $ iv
 

iv is an IVar (I used ivar-simple). The pertinent operations on them are:

 
new :: IO (IVar a)
write :: IVar a -> a -> IO ()
read :: IVar a -> a
 

new creates an empty IVar, and we can write to one only once; trying to write a second time will throw an exception. But this is no problem for me, because I obviously only attempt to write once. read will block until its argument is actually is set, and since that can only happen once, it is considered safe for read to not require IO. [1]

Using this and forkIO, one can easily write something like unsafeInterleaveIO, which accepts an IO a argument and yields an IO a whose result is guaranteed to be the result of running the argument at some time in the future. The only difference is that the real unsafeInterleaveIO schedules things just in time, whereas mine schedules them in a relatively random order (I'll admit I had to try a few times before I got the 'expected' lazy IO answer).

But, we could even take this to be the specification of interleaving. It runs IO actions concurrently, and you will be fine as long as you aren't attempting to depend on the exact scheduling order (or whether things get scheduled at all in some cases).

In fact, thinking of lazy I/O as concurrency turns most spooky examples into threading problems that I would expect most people to consider rather basic. For instance:

• Don't pass a handle to another thread and close it in the original.
• Don't fork more file-reading threads than you have file descriptors.
• Don't fork threads to handle files if you're concerned about the files being closed deterministically.
• Don't read from the same handle in multiple threads (unless you don't care about each thread seeing a random subsequence of the stream).

And of course, the original example in this article is just non-determinism introduced by concurrency, but not of a sort that requires fundamentally different explanation than fork. The main pitfall, in my biased opinion, is that the scheduling for interleaving is explained in a way that encourages people to try to guess exactly what it will do. But the presumption of purity (and the reordering GHC actually does based on it) actually means that you cannot assume that much more about the scheduling than you can about my scheduler, at least in general.

This isn't to suggest that lazy I/O is appropriate for every situation. Sometimes the above advice means that it is not appropriate to use concurrency. However, in my opinion, people are over eager to ban lazy I/O even for simple uses where it is the nicest solution, and justify it based on the 'evil' and 'confusing' ascriptions. But, personally, I don't think this is justified, unless one does the same for pretty much all concurrency.

I suppose the only (leading) question left to ask is which should be declared unsafe, fork or ivars, since together they allow you to construct a(n even less deterministic) unsafeInterleaveIO?

[1] Note that there are other implementations of IVar. I'd expect the most popular to be in monad-par by Simon Marlow. That allows one to construct an operation like read, but it is actually less deterministic in my construction, because it seems that it will not block unless perhaps you write and read within a single 'transaction,' so to speak.

In fact, this actually breaks referential transparency in conjunction with forkIO:

 
deref = runPar . get
 
randomDelay = randomRIO (1,10) >>= threadDelay . (1000*)
 
myHandle m = m `catch` \(_ :: SomeExpression) -> putStrLn "Bombed"
 
mySpawn :: IO a -> IO (IVar a)
mySpawn action = do
  iv < - runParIO new
  forkIO $ randomDelay >> action >>= runParIO . put_ iv
  return iv
 
main = do
  iv < - mySpawn (return True)
  myHandle . print $ deref iv
  randomDelay
  myHandle . print $ deref iv
 

Sometimes this will print "Bombed" twice, and sometimes it will print "Bombed" followed by "True". The latter will never happen if we factor out the deref iv however. The blocking behavior is essential to deref maintaining referential transparency, and it seems like monad-par only blocks within a single runPar, not across multiples. Using ivar-simple in this example always results in "True" being printed twice.

It is also actually possible for unsafeInterleaveIO to break referential transparency if it is implemented incorrectly (or if the optimizer mucks with the internals in some bad way). But I haven't seen an example that couldn't be considered a bug in the implementation rather than some fundamental misbehavior. And my reference implementation here (with a suboptimal scheduler) suggests that there is no break that isn't just a bug.

by Dan Doel at October 24, 2022 05:47 PM

Categories of Structures in Haskell

In the last couple posts I've used some 'free' constructions, and not remarked too much on how they arise. In this post, I'd like to explore them more. This is going to be something of a departure from the previous posts, though, since I'm not going to worry about thinking precisely about bottom/domains. This is more an exercise in applying some category theory to Haskell, "fast and loose".

(Advance note: for some continuous code to look at see this file.)

First, it'll help to talk about how some categories can work in Haskell. For any kind k made of * and (->), [0] we can define a category of type constructors. Objects of the category will be first-class [1] types of that kind, and arrows will be defined by the following type family:

 
newtype Transformer f g = Transform { ($$) :: forall i. f i ~> g i }
 
type family (~>) :: k -> k -> * where
  (~>) = (->)
  (~>) = Transformer
 
type a < -> b = (a -> b, b -> a)
type a < ~> b = (a ~> b, b ~> a)
 

So, for a base case, * has monomorphic functions as arrows, and categories for higher kinds have polymorphic functions that saturate the constructor:

 
  Int ~> Char = Int -> Char
  Maybe ~> [] = forall a. Maybe a -> [a]
  Either ~> (,) = forall a b. Either a b -> (a, b)
  StateT ~> ReaderT = forall s m a. StateT s m a -> ReaderT s m a
 

We can of course define identity and composition for these, and it will be handy to do so:

 
class Morph (p :: k -> k -> *) where
  id :: p a a
  (.) :: p b c -> p a b -> p a c
 
instance Morph (->) where
  id x = x
  (g . f) x = g (f x)
 
instance Morph ((~>) :: k -> k -> *)
      => Morph (Transformer :: (i -> k) -> (i -> k) -> *) where
  id = Transform id
  Transform f . Transform g = Transform $ f . g
 

These categories can be looked upon as the most basic substrates in Haskell. For instance, every type of kind * -> * is an object of the relevant category, even if it's a GADT or has other structure that prevents it from being nicely functorial.

The category for * is of course just the normal category of types and functions we usually call Hask, and it is fairly analogous to the category of sets. One common activity in category theory is to study categories of sets equipped with extra structure, and it turns out we can do this in Haskell, as well. And it even makes some sense to study categories of structures over any of these type categories.

When we equip our types with structure, we often use type classes, so that's how I'll do things here. Classes have a special status socially in that we expect people to only define instances that adhere to certain equational rules. This will take the place of equations that we are not able to state in the Haskell type system, because it doesn't have dependent types. So using classes will allow us to define more structures that we normally would, if only by convention.

So, if we have a kind k, then a corresponding structure will be σ :: k -> Constraint. We can then define the category (k,σ) as having objects t :: k such that there is an instance σ t. Arrows are then taken to be f :: t ~> u such that f "respects" the operations of σ.

As a simple example, we have:

 
  k = *
  σ = Monoid :: * -> Constraint
 
  Sum Integer, Product Integer, [Integer] :: (*, Monoid)
 
  f :: (Monoid m, Monoid n) => m -> n
    if f mempty = mempty
       f (m <> n) = f m <> f n
 

This is just the category of monoids in Haskell.

As a side note, we will sometimes be wanting to quantify over these "categories of structures". There isn't really a good way to package together a kind and a structure such that they work as a unit, but we can just add a constraint to the quantification. So, to quantify over all Monoids, we'll use 'forall m. Monoid m => ...'.

Now, once we have these categories of structures, there is an obvious forgetful functor back into the unadorned category. We can then look for free and cofree functors as adjoints to this. More symbolically:

 
  Forget σ :: (k,σ) -> k
  Free   σ :: k -> (k,σ)
  Cofree σ :: k -> (k,σ)
 
  Free σ ⊣ Forget σ ⊣ Cofree σ
 

However, what would be nicer (for some purposes) than having to look for these is being able to construct them all systematically, without having to think much about the structure σ.

Category theory gives a hint at this, too, in the form of Kan extensions. In category terms they look like:

  p : C -> C'
  f : C -> D
  Ran p f : C' -> D
  Lan p f : C' -> D

  Ran p f c' = end (c : C). Hom_C'(c', p c) ⇒ f c
  Lan p f c' = coend (c : c). Hom_C'(p c, c') ⊗ f c

where ⇒ is a "power" and ⊗ is a copower, which are like being able to take exponentials and products by sets (or whatever the objects of the hom category are), instead of other objects within the category. Ends and coends are like universal and existential quantifiers (as are limits and colimits, but ends and coends involve mixed-variance).

Some handy theorems relate Kan extensions and adjoint functors:

  if L ⊣ R
  then L = Ran R Id and R = Lan L Id

  if Ran R Id exists and is absolute
  then Ran R Id ⊣ R

  if Lan L Id exists and is absolute
  then L ⊣ Lan L Id

  Kan P F is absolute iff forall G. (G . Kan P F) ~= Kan P (G . F)

It turns out we can write down Kan extensions fairly generally in Haskell. Our restricted case is:

 
  p = Forget σ :: (k,σ) -> k
  f = Id :: (k,σ) -> (k,σ)
 
  Free   σ = Ran (Forget σ) Id :: k -> (k,σ)
  Cofree σ = Lan (Forget σ) Id :: k -> (k,σ)
 
  g :: (k,σ) -> j
  g . Free   σ = Ran (Forget σ) g
  g . Cofree σ = Lan (Forget σ) g
 

As long as the final category is like one of our type constructor categories, ends are universal quantifiers, powers are function types, coends are existential quantifiers and copowers are product spaces. This only breaks down for our purposes when g is contravariant, in which case they are flipped. For higher kinds, these constructions occur point-wise. So, we can break things down into four general cases, each with cases for each arity:

 
newtype Ran0 σ p (f :: k -> *) a =
  Ran0 { ran0 :: forall r. σ r => (a ~> p r) -> f r }
 
newtype Ran1 σ p (f :: k -> j -> *) a b =
  Ran1 { ran1 :: forall r. σ r => (a ~> p r) -> f r b }
 
-- ...
 
data RanOp0 σ p (f :: k -> *) a =
  forall e. σ e => RanOp0 (a ~> p e) (f e)
 
-- ...
 
data Lan0 σ p (f :: k -> *) a =
  forall e. σ e => Lan0 (p e ~> a) (f e)
 
data Lan1 σ p (f :: k -> j -> *) a b =
  forall e. σ e => Lan1 (p e ~> a) (f e b)
 
-- ...
 
data LanOp0 σ p (f :: k -> *) a =
  LanOp0 { lan0 :: forall r. σ r => (p r -> a) -> f r }
 
-- ...
 

The more specific proposed (co)free definitions are:

 
type family Free   :: (k -> Constraint) -> k -> k
type family Cofree :: (k -> Constraint) -> k -> k
 
newtype Free0 σ a = Free0 { gratis0 :: forall r. σ r => (a ~> r) -> r }
type instance Free = Free0
 
newtype Free1 σ f a = Free1 { gratis1 :: forall g. σ g => (f ~> g) -> g a }
type instance Free = Free1
 
-- ...
 
data Cofree0 σ a = forall e. σ e => Cofree0 (e ~> a) e
type instance Cofree = Cofree0
 
data Cofree1 σ f a = forall g. σ g => Cofree1 (g ~> f) (g a)
type instance Cofree = Cofree1
 
-- ...
 

We can define some handly classes and instances for working with these types, several of which generalize existing Haskell concepts:

 
class Covariant (f :: i -> j) where
  comap :: (a ~> b) -> (f a ~> f b)
 
class Contravariant f where
  contramap :: (b ~> a) -> (f a ~> f b)
 
class Covariant m => Monad (m :: i -> i) where
  pure :: a ~> m a
  join :: m (m a) ~> m a
 
class Covariant w => Comonad (w :: i -> i) where
  extract :: w a ~> a
  split :: w a ~> w (w a)
 
class Couniversal σ f | f -> σ where
  couniversal :: σ r => (a ~> r) -> (f a ~> r)
 
class Universal σ f | f -> σ where
  universal :: σ e => (e ~> a) -> (e ~> f a)
 
instance Covariant (Free0 σ) where
  comap f (Free0 e) = Free0 (e . (.f))
 
instance Monad (Free0 σ) where
  pure x = Free0 $ \k -> k x
  join (Free0 e) = Free0 $ \k -> e $ \(Free0 e) -> e k
 
instance Couniversal σ (Free0 σ) where
  couniversal h (Free0 e) = e h
 
-- ...
 

The only unfamiliar classes here should be (Co)Universal. They are for witnessing the adjunctions that make Free σ the initial σ and Cofree σ the final σ in the relevant way. Only one direction is given, since the opposite is very easy to construct with the (co)monad structure.

Free σ is a monad and couniversal, Cofree σ is a comonad and universal.

We can now try to convince ourselves that Free σ and Cofree σ are absolute Here are some examples:

 
free0Absolute0 :: forall g σ a. (Covariant g, σ (Free σ a))
               => g (Free0 σ a) < -> Ran σ Forget g a
free0Absolute0 = (l, r)
 where
 l :: g (Free σ a) -> Ran σ Forget g a
 l g = Ran0 $ \k -> comap (couniversal $ remember0 . k) g
 
 r :: Ran σ Forget g a -> g (Free σ a)
 r (Ran0 e) = e $ Forget0 . pure
 
free0Absolute1 :: forall (g :: * -> * -> *) σ a x. (Covariant g, σ (Free σ a))
               => g (Free0 σ a) x < -> Ran σ Forget g a x
free0Absolute1 = (l, r)
 where
 l :: g (Free σ a) x -> Ran σ Forget g a x
 l g = Ran1 $ \k -> comap (couniversal $ remember0 . k) $$ g
 
 r :: Ran σ Forget g a x -> g (Free σ a) x
 r (Ran1 e) = e $ Forget0 . pure
 
free0Absolute0Op :: forall g σ a. (Contravariant g, σ (Free σ a))
                 => g (Free0 σ a) < -> RanOp σ Forget g a
free0Absolute0Op = (l, r)
 where
 l :: g (Free σ a) -> RanOp σ Forget g a
 l = RanOp0 $ Forget0 . pure
 
 r :: RanOp σ Forget g a -> g (Free σ a)
 r (RanOp0 h g) = contramap (couniversal $ remember0 . h) g
 
-- ...
 

As can be seen, the definitions share a lot of structure. I'm quite confident that with the right building blocks these could be defined once for each of the four types of Kan extensions, with types like:

 
freeAbsolute
  :: forall g σ a. (Covariant g, σ (Free σ a))
  => g (Free σ a) < ~> Ran σ Forget g a
 
cofreeAbsolute
  :: forall g σ a. (Covariant g, σ (Cofree σ a))
  => g (Cofree σ a) < ~> Lan σ Forget g a
 
freeAbsoluteOp
  :: forall g σ a. (Contravariant g, σ (Free σ a))
  => g (Free σ a) < ~> RanOp σ Forget g a
 
cofreeAbsoluteOp
  :: forall g σ a. (Contravariant g, σ (Cofree σ a))
  => g (Cofree σ a) < ~> LanOp σ Forget g a
 

However, it seems quite difficult to structure things in a way such that GHC will accept the definitions. I've successfully written freeAbsolute using some axioms, but turning those axioms into class definitions and the like seems impossible.

Anyhow, the punchline is that we can prove absoluteness using only the premise that there is a valid σ instance for Free σ and Cofree σ. This tends to be quite easy; we just borrow the structure of the type we are quantifying over. This means that in all these cases, we are justified in saying that Free σ ⊣ Forget σ ⊣ Cofree σ, and we have a very generic presentations of (co)free structures in Haskell. So let's look at some.

We've already seen Free Monoid, and last time we talked about Free Applicative, and its relation to traversals. But, Applicative is to traversal as Functor is to lens, so it may be interesting to consider constructions on that. Both Free Functor and Cofree Functor make Functors:

 
instance Functor (Free1 Functor f) where
  fmap f (Free1 e) = Free1 $ fmap f . e
 
instance Functor (Cofree1 Functor f) where
  fmap f (Cofree1 h e) = Cofree1 h (fmap f e)
 

And of course, they are (co)monads, covariant functors and (co)universal among Functors. But, it happens that I know some other types with these properties:

 
data CoYo f a = forall e. CoYo (e -> a) (f e)
 
instance Covariant CoYo where
  comap f = Transform $ \(CoYo h e) -> CoYo h (f $$ e)
 
instance Monad CoYo where
  pure = Transform $ CoYo id
  join = Transform $ \(CoYo h (CoYo h' e)) -> CoYo (h . h') e
 
instance Functor (CoYo f) where
  fmap f (CoYo h e) = CoYo (f . h) e
 
instance Couniversal Functor CoYo where
  couniversal tr = Transform $ \(CoYo h e) -> fmap h (tr $$ e)
 
newtype Yo f a = Yo { oy :: forall r. (a -> r) -> f r }
 
instance Covariant Yo where
  comap f = Transform $ \(Yo e) -> Yo $ (f $$) . e
 
instance Comonad Yo where
  extract = Transform $ \(Yo e) -> e id
  split = Transform $ \(Yo e) -> Yo $ \k -> Yo $ \k' -> e $ k' . k
 
instance Functor (Yo f) where
  fmap f (Yo e) = Yo $ \k -> e (k . f)
 
instance Universal Functor Yo where
  universal tr = Transform $ \e -> Yo $ \k -> tr $$ fmap k e
 

These are the types involved in the (co-)Yoneda lemma. CoYo is a monad, couniversal among functors, and CoYo f is a Functor. Yo is a comonad, universal among functors, and is always a Functor. So, are these equivalent types?

 
coyoIso :: CoYo < ~> Free Functor
coyoIso = (Transform $ couniversal pure, Transform $ couniversal pure)
 
yoIso :: Yo < ~> Cofree Functor
yoIso = (Transform $ universal extract, Transform $ universal extract)
 

Indeed they are. And similar identities hold for the contravariant versions of these constructions.

I don't have much of a use for this last example. I suppose to be perfectly precise, I should point out that these uses of (Co)Yo are not actually part of the (co-)Yoneda lemma. They are two different constructions. The (co-)Yoneda lemma can be given in terms of Kan extensions as:

 
yoneda :: Ran Id f < ~> f
 
coyoneda :: Lan Id f < ~> f
 

But, the use of (Co)Yo to make Functors out of things that aren't necessarily is properly thought of in other terms. In short, we have some kind of category of Haskell types with only identity arrows---it is discrete. Then any type constructor, even non-functorial ones, is certainly a functor from said category (call it Haskrete) into the normal one (Hask). And there is an inclusion functor from Haskrete into Hask:

             F
 Haskrete -----> Hask
      |        /|
      |       /
      |      /
Incl  |     /
      |    /  Ran/Lan Incl F
      |   /
      |  /
      v /
    Hask

So, (Co)Free Functor can also be thought of in terms of these Kan extensions involving the discrete category.

To see more fleshed out, loadable versions of the code in this post, see this file. I may also try a similar Agda development at a later date, as it may admit the more general absoluteness constructions easier.

[0]: The reason for restricting ourselves to kinds involving only * and (->) is that they work much more simply than data kinds. Haskell values can't depend on type-level entities without using type classes. For *, this is natural, but for something like Bool -> *, it is more natural for transformations to be able to inspect the booleans, and so should be something more like forall b. InspectBool b => f b -> g b.

[1]: First-class types are what you get by removing type families and synonyms from consideration. The reason for doing so is that these can't be used properly as parameters and the like, except in cases where they reduce to some other type that is first-class. For example, if we define:

 
type I a = a
 

even though GHC will report I :: * -> *, it is not legal to write Transform I I.

by Dan Doel at October 24, 2022 05:47 PM

How to correctly cache build-time dependencies using Nix

caching

Professional Nix users often create a shared cache of Nix build products so that they can reuse build products created by continuous integration (CI). For example, CI might build Nix products for each main development branch of their project or even for every pull request and it would be nice if those build products could be shared with all developers via a cache.

However, uploading build products to a cache is a little non-trivial if you don’t already know the “best� solution, which is the subject of this post.

The solution described in this post is:

• Simple

  It only takes a few lines of Bash code because we use the Nix command-line interface idiomatically

• Efficient

  It is very cheap to compute which build products to upload and requires no additional builds nor an exorbitant amount of disk space

• Accurate

  It uploads the build products that most people would intuitively want to upload

Note: Throughout this post I will be using the newer Nix command-line interface and flakes, which requires either adding this line to your nix.conf file:

extra-experimental-features = nix-command flakes

… and restarting your Nix daemon (if you have a multi-user Nix installation), or alternatively adding these flags to the beginning of all nix commands throughout this post:

$ nix --option extra-experimental-features 'nix-command flakes' …

Wrong solution #0

As a running example, suppose that our CI builds a top-level build product using a command like this:

$ nix build .#example

The naïve way to upload that to the cache would be:

$ nix store sign --key-file "${KEY_FILE}" --recursive .#example

$ nix copy --to s3://cache.example.com .#example

Note: You will need to generate a KEY_FILE using the nix-store --generate-binary-cache-key command if you haven’t already. For more details, see the following documentation from the manual:

Click to expand to see the documentation

Operation --generate-binary-cache-key
   Synopsis
       nix-store --generate-binary-cache-key key-name secret-key-file
       public-key-file

   Description
       This command generates an Ed25519 key pair (http://ed25519.cr.yp.to/)
       that can be used to create a signed binary cache. It takes three
       mandatory parameters:

       1.     A key name, such as cache.example.org-1, that is used to look up
              keys on the client when it verifies signatures. It can be
              anything, but it’s suggested to use the host name of your cache
              (e.g.  cache.example.org) with a suffix denoting the number of the
              key (to be incremented every time you need to revoke a key).

       2.     The file name where the secret key is to be stored.

       3.     The file name where the public key is to be stored.

That seems like a perfectly reasonable thing to do, right? However, the problem with that is that it is incomplete, meaning that the cache would still be missing several useful build products that developers would expect to be there.

Specifically, the above command only copies the “run-time� dependencies of our build product whereas most developers expect the cache to also include “build-time� dependencies, and I’ll explain the distinction between the two.

Run-time vs. Build-time

Many paths in the /nix/store are not “validâ€� in isolation. They typically depend on other paths within the /nix/store.

For example, suppose that I build the GNU hello package, like this:

$ nix build nixpkgs#hello

I can query all of the other paths within the /nix/storethat the hello package transitively depends on at run-time using this command:

$ nix-store --query --requisites ./result
/nix/store/jzid7pfrhv6gpiwqbx6763v0g9c3bdzb-libobjc-11.0.0
/nix/store/9rb5qaba71mkgfgd8wfqg03cmi46xarg-apple-framework-CoreFoundation-11.0>
/nix/store/akjp4x41jjx5hzgzrschwqzr8qfsdpys-hello-2.12.1

… or I can print the same information in tree form like this:

$ nix-store --query --tree ./result
/nix/store/akjp4x41jjx5hzgzrschwqzr8qfsdpys-hello-2.12.1
└───/nix/store/9rb5qaba71mkgfgd8wfqg03cmi46xarg-apple-framework-CoreFoundation-11.0.0
    └───/nix/store/jzid7pfrhv6gpiwqbx6763v0g9c3bdzb-libobjc-11.0.0

On my macOS machine, it has two run-time dependencies (other than itself) within the /nix/store: libobjc and apple-framework-CoreFoundation-11.0.

Note: there might be other run-time dependencies, because I believe Nixpkgs support for macOS requires some impure system dependencies, but I’m not an expert on this so I could be wrong.

These are called “run-timeâ€� dependencies because we cannot run our hello executable without them.

Nix prevents us from getting into situations where a /nix/store path is missing its run-time dependencies. For example, if I were to nix copy the hello build product to any cache, then Nix would perform the following steps, in order:

• Copy libobjc to the cache

  … since that has no dependencies

• Copy apple-framework-CoreFoundation to the cache

  … since its libobjc dependency is now satisfied within the cache

• Copy hello to the cache

  … since its apple-framework-CoreFoundation dependency is now satisfied within the cache

However, Nix also has a separate notion of “build-timeâ€� dependencies, which are dependencies that we need to in order to build the hello package.

Note: The reason we’re interested in build-time dependencies for our project is that we want developers to be able to rebuild the project if they make any changes to the source code. If we were to only cache the run-time dependencies of our project that wouldn’t cache the development environment that developers need.

In order to query these dependencies I need to first get the “derivationâ€� (.drv file) for hello:

$ DERIVATION="$(nix path-info --derivation nixpkgs#hello)"

$ declare -p DERIVATION
typeset DERIVATION=/nix/store/4a78f0s4p5h2sbcrrzayl5xas2i7zq1m-hello-2.12.1.drv

You can think of a derivation file as a build recipe that contains instructions for how to build the corresponding build product (the hello package in this case).

I can query the direct dependencies of that derivation using this command:

$ nix-store --query --references "${DERIVATION}"
/nix/store/9krlzvny65gdc8s7kpb6lkx8cd02c25b-default-builder.sh
/nix/store/labgzlb16svs1z7z9a6f49b5zi8hb11s-bash-5.1-p16.drv
/nix/store/cdk3pz11mvhqpphr0197wwmzhqppn7rl-stdenv-darwin.drv
/nix/store/hwymznwkd1kgf5ldcldjl9bnc1wz2azb-hello-2.12.1.tar.gz.drv

Many of these dependencies are themselves derivations (.drv files), meaning that they represent other packages that Nix might have to build or fetch from a cache.

Note: the .drv files are actually not the build-time dependencies, but rather the instructions for building them. You can convert any .drv file to the matching product it is supposed to build using the same nix build command, like this:

$ nix build /nix/store/labgzlb16svs1z7z9a6f49b5zi8hb11s-bash-5.1-p16.drv

Does that mean that these build-time dependencies are on our machine if we built nixpkgs#hello? Not necessarily. In fact, in all likelihood the nixpkgs#hello build was cached, meaning that nix build nixpkgs#hello only downloaded helloand its run-time dependencies and no build-time dependencies were required nor installed by Nix.

However, I could in principle force Nix to build the hello package instead of downloading it from a cache, like this:

$ nix build nixpkgs#hello --rebuild

… and that would download the direct build-time dependencies of the hello package in order to rebuild the package.

Wrong solution #1

By this point you might suppose that you have enough information to come up with a better set of /nix/store paths to cache. Your solution might look like this:

• Get the derivation for the top-level build product

• Get the direct build-time dependencies of that derivation

• Build the top-level build product and its direct build-time dependencies

• Cache the top-level build product and its direct build-time dependencies

In other words, something like this Nix code:

$ DERIVATION="$(nix path-info --derivation "${BUILD}")"

$ DEPENDENCIES=($(nix-store --query --references "${DERIVATION}"))

$ nix build "${BUILD}" "${DEPENDENCIES[@]}"

$ nix store sign --key-file "${KEY_FILE}" --recursive "${BUILD}" "${DEPENDENCIES[@]}"

$ nix copy --to "${CACHE}" "${BUILD}" "${DEPENDENCIES[@]}"

This is better, but still not good enough!

The problem with this solution is that it only works well if your dependencies never change and you only modify your top-level project. If you upgrade or patch any of your direct build-time dependencies then you need to have their build-time dependencies cached so that you can quickly rebuild them.

In fact, going two layers deep is still not enough; in practice you can’t easily anticipate in advance how deep in the build-time dependency tree you might need to patch or upgrade things. For example, you might need to patch or upgrade your compiler, which is really deep in your build-time dependency tree.

Wrong solution #2

Okay, so maybe we can try to build and cache all of our build-time dependencies?

Wrong again. There are way too many of them. You can query them by replacing --references with --requisites and you’ll a giant list of results, even for “smallâ€� packages. For example:

$ DERIVATION=$(nix path-info --derivation nixpkgs#hello)

$ nix-store --query --requisites "${DERIVATION}"
/nix/store/8djp1rizc1dblv8svnb0mpa0c3lwvc17-drop-comments.patch
/nix/store/9krlzvny65gdc8s7kpb6lkx8cd02c25b-default-builder.sh
/nix/store/3glray2y14jpk1h6i599py7jdn3j2vns-mkdir.drv
/nix/store/50ql5q0raqkcydmpi6wqvnhs9hpdgg5f-cpio.drv
/nix/store/81xahsrhpn9mbaslgi5sz7gsqra747d4-unpack-bootstrap-tools-aarch64.sh
/nix/store/fzbk4fnbjqhr0l1scx5fspsx5najbrbm-bootstrap-tools.cpio.bz2.drv
/nix/store/gxzl4vmccqj89yh7kz62frkxzgdpkxmp-sh.drv
… 🌺 500+ derivations later 🌺 …
/nix/store/i0zc5mm4vpj3lviyydb9s73j53mypkrg-nghttp2-1.49.0.drv
/nix/store/w37b5s734m53gxnzqyb5v0v98mhdfg2i-coreutils-9.1.drv
/nix/store/mmsrbggvzn6rwlx1ijw90sw3wvhzj18j-openssl-3.0.5.drv
/nix/store/n7iibs6b818v402j0yczf4mgy73sbzpv-libssh2-1.10.0.drv
/nix/store/z074ki54p77r7db3wsgxh9p18f67xnv8-curl-7.85.0.drv
/nix/store/hwymznwkd1kgf5ldcldjl9bnc1wz2azb-hello-2.12.1.tar.gz.drv
/nix/store/4a78f0s4p5h2sbcrrzayl5xas2i7zq1m-hello-2.12.1.drv

Click to expand and see the full list of build-time dependencies

/nix/store/8djp1rizc1dblv8svnb0mpa0c3lwvc17-drop-comments.patch
/nix/store/9krlzvny65gdc8s7kpb6lkx8cd02c25b-default-builder.sh
/nix/store/3glray2y14jpk1h6i599py7jdn3j2vns-mkdir.drv
/nix/store/50ql5q0raqkcydmpi6wqvnhs9hpdgg5f-cpio.drv
/nix/store/81xahsrhpn9mbaslgi5sz7gsqra747d4-unpack-bootstrap-tools-aarch64.sh
/nix/store/fzbk4fnbjqhr0l1scx5fspsx5najbrbm-bootstrap-tools.cpio.bz2.drv
/nix/store/gxzl4vmccqj89yh7kz62frkxzgdpkxmp-sh.drv
/nix/store/pjbpvdy0gais8nc4sj3kwpniq8mgkb42-bzip2.drv
/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv
/nix/store/1i5y55x4b4m9qkx5dqbmr1r6bvrqbanw-multiple-outputs.sh
/nix/store/59jmzisg8fkm9c125fw384dqq1np602l-move-docs.sh
/nix/store/bnj8d7mvbkg3vdb07yz74yhl3g107qq5-patch-shebangs.sh
/nix/store/cickvswrvann041nqxb0rxilc46svw1n-prune-libtool-files.sh
/nix/store/ckzrg0f0bdyx8rf703nc61r3hz5yys9q-builder.sh
/nix/store/fyaryjvghbkpfnsyw97hb3lyb37s1pd6-move-lib64.sh
/nix/store/g8xg0i02aqwhgxwd2vnp5ax3d6lrkg1v-strip.sh
/nix/store/jngr4r80x5jn482ckqrfh08ljrx1k86f-setup.sh
/nix/store/kd4xwxjpjxi71jkm6ka0np72if9rm3y0-move-sbin.sh
/nix/store/kxw6q8v6isaqjm702d71n2421cxamq68-make-symlinks-relative.sh
/nix/store/m54bmrhj6fqz8nds5zcj97w9s9bckc9v-compress-man-pages.sh
/nix/store/ngg1cv31c8c7bcm2n8ww4g06nq7s4zhm-set-source-date-epoch-to-latest.sh
/nix/store/wlwcf1nw2b21m4gghj70hbg1v7x53ld8-reproducible-builds.sh
/nix/store/nbxwxwqwcr9rrmxb6gb532f18102815x-bootstrap-stage0-stdenv-darwin.drv
/nix/store/ycwm35msmsdi2qgjax1slmjffsmwy8am-write-mirror-list.sh
/nix/store/i65va14cylqc74y80ksgnrsaixk39mmh-mirrors-list.drv
/nix/store/lphxcbw5wqsjskipaw1fb8lcf6pm6ri6-builder.sh
/nix/store/bgp77z9z42x35vmwyfywqaiqsmnb3ffa-patchutils-0.3.3.tar.xz.drv
/nix/store/3lhw0v2wyzimzl96xfsk6psfmzh38irh-bash51-007.drv
/nix/store/3p62kw9mpkcp0grhirfn46i9afhqf0c9-bash51-015.drv
/nix/store/3za6mykjk49sr616w80lvmy5xcmbkrp3-bash51-006.drv
/nix/store/5lv0fbn6ajwdzw04nz88cc0qqrgrvnp1-bash51-016.drv
/nix/store/4dq81yma6drk9701h17h64zx47r7p5n8-utils.sh
/nix/store/ds0q1li2i96dy7yp6n8zkbakz7m7d5l8-bootstrap-stage0-stdenv-darwin.drv
/nix/store/vcbpmcxpir9nyy480vx5sxb4pm2v0dps-bootstrap-stage0-sigtool.drv
/nix/store/5xk8j72a1dddq1gxh39amgifknwb0lvm-signing-utils.drv
/nix/store/fmd71yqpgwrkdbidzxwmfasqp39zzf8r-CLTools_macOSNMOS_SDK.pkg.drv
/nix/store/ijdrwgv6kv4k17qb5jvqkbs1ccqrlalb-bootstrap-stage0-pbzx.drv
/nix/store/z727aawh6imz3hpmviqyf4zlgprfn8zf-bootstrap-stage0-cpio.drv
/nix/store/fbhkqzn4wc69pa4rvndin5h4b8k02f5c-MacOSX-SDK-11.0.0.drv
/nix/store/72fl7wcbnl6srm5dxb7xbnn20zr07011-libobjc-11.0.0.drv
/nix/store/93n8xmgm6x65mh88amw15wps3h18yqn8-bootstrap-stage0-libcxx.drv
/nix/store/cyk47lyfswsxgn7z2qnhkp0919nhdd3b-config.sub?id=6faca61810d335c7837f320733fe8e15a1431fc2.drv
/nix/store/lmdwlh09b7g3kzga0i2hprcfxszg3ghz-config.guess?id=6faca61810d335c7837f320733fe8e15a1431fc2.drv
/nix/store/9vh7qbpb8chmx5r5cswrix00hngy7vky-gnu-config-2021-01-25.drv
/nix/store/2idjp2xdckqyrdk3hd8msp4cfdi6b8if-utils.bash
/nix/store/47gspvwaxra868q4rsmva0g5nz7zac6p-add-clang-cc-cflags-before.sh
/nix/store/797k3249lr4rx8wslf7kcsa3hv6fis3x-role.bash
/nix/store/bybz12bxjbk94hm58zc70sc0xhj2dxif-add-darwin-ldflags-before.sh
/nix/store/c1vmxz359mfljs3cdimhd2fr6fw0n99s-add-hardening.sh
/nix/store/civvq4xh4p0mj04l7k73p1xbsq1rs9bc-darwin-install_name_tool-wrapper.sh
/nix/store/dk3ly72kiv27srcj1mjr5n4112vx2hfk-setup-hook.sh
/nix/store/khkfggnk4h14f2spsjcjrxlf8himd4vj-bootstrap-stage0-rewrite-tbd.drv
/nix/store/ff3yqdllxmlp1r8mfkfgjf671r8flf8j-libSystem-11.0.0.drv
/nix/store/gvr0mz9wfz4g0z9w6477ikywmcivk1mh-bootstrap-stage0-coreutils.drv
/nix/store/jravmbdjn0md7cnn6rbqwf3aflw72msb-post-link-sign-hook.drv
/nix/store/js1lic1bmif60d4mlffkpbvz5jim34n3-darwin-strip-wrapper.sh
/nix/store/m0ww06j4y2v3jdsabrr8n0y9d4nnvqn3-bootstrap-stage0-gnugrep.drv
/nix/store/mrzpfh0ml9k07sw019ydagbb2z1q4sxz-add-flags.sh
/nix/store/vicx6qnvvxb96y0iwnya977viira2apc-ld-wrapper.sh
/nix/store/dj5xngrf61x9isyp2r5d84h3i43wg65l-bootstrap-stage0-binutils-wrapper-.drv
/nix/store/gn1b4gh07byi8xnahgc800jznyarqin0-bootstrap-stage0-clang.drv
/nix/store/hc3z14jhqg35x5286hw5wmc3injg62fa-add-hardening.sh
/nix/store/ji2yrl1na00bwav65hh1vr0nc0s1xzvz-add-flags.sh
/nix/store/lck6bijpq64zjvmkwdi081v6wm2r8nyx-bootstrap-stage0-libcxxabi.drv
/nix/store/li62b4bvg51zikbni9xadg08za340k71-cc-wrapper.sh
/nix/store/nc4bvrgb8jxh4k1fq2zgzh4mmxqavp54-setup-hook.sh
/nix/store/xbfsjb46np040h2aph1k76iybq9rzd7x-bootstrap-stage0-compiler-rt.drv
/nix/store/cz1x2bgvnzi0qc39hjwm0ppdvqwkfybl-bootstrap-stage0-clang-wrapper-11.1.0.drv
/nix/store/00qr10y7z2fcvrp9b2m46710nkjvj55z-update-autotools-gnu-config-scripts.sh
/nix/store/qzvw98z9qwv3vasfc9lwcq0d1sgfin6v-hook.drv
/nix/store/vp49i9krzqf282vj6bqr6rxs96d2a1fv-apple-framework-CoreFoundation-11.0.0.drv
/nix/store/lkjwmgmnm4f7d3iiglxglrgll1c8vdkf-bootstrap-stage1-stdenv-darwin.drv
/nix/store/r09r8wpshjqdkx0xwkin79km812nbgp3-m4-1.4.19.tar.bz2.drv
/nix/store/7rxh71ny4xrckw1ip50hv44mylpxpd5v-gnum4-1.4.19.drv
/nix/store/h1s43lrwjjf98dmfhayn6cmax2h19qz9-bison-3.8.2.tar.gz.drv
/nix/store/85f1q5rm0qzqay7fk3935h6kvzfqdcfv-http-tiny-verify-ssl-by-default.patch
/nix/store/dm81j9qdcdr4c458pqbc9wvq9ymgzk4m-setup-hook.sh
/nix/store/mb381gpm9k5wdl37l5ad5pp8w11qzhjg-no-sys-dirs-5.31.patch
/nix/store/n315a3g9bcxlypqzbm36nzrrg40h6lcj-cpp-precomp.patch
/nix/store/ppbkcbhzwzwpqaad6whhr9qgxjvj82gj-perl-5.36.0.tar.gz.drv
/nix/store/0phjl3yzr4m1gady21l21h4brn140hjm-CVE-2022-37434.patch
/nix/store/jw5f744vn0nv6q0ms6s5q0w0kkml2a8v-fix-configure-issue-cross.patch
/nix/store/mg7z3nsc96864cfkx2jwda7wmpdn71dl-zlib-1.2.12.tar.gz.drv
/nix/store/xniqbx8mh8lx06bw267g6hkfkp2c79kn-comprehensive-crc-validation-for-wrong-implementations.patch
/nix/store/vblzwf77rk1mxxk6qjhgaqp43z36j992-zlib-1.2.12.drv
/nix/store/x0ll5lnagy6lg7hgvqb26il3qnmsqisd-sw_vers.patch
/nix/store/m9h3rw3jlzf8hapgiw29i5fjyzw7r9v4-perl-5.36.0.drv
/nix/store/5nxxxmzb23y9pzp673grmfs95jrx14rx-bison-3.8.2.drv
/nix/store/13i5k09s5g6gdkaj731rqsi1qc70khka-bootstrap-stage1-stdenv-darwin.drv
/nix/store/jik02mkz72r2f6hhxnlhp6h5f0fi89gw-expand-response-params.c
/nix/store/g9h3q3y44p4ycn8vdai1s9aw1f0s7icy-expand-response-params.drv
/nix/store/734l1nlc4d2zbksafqvp5436ynp26z3g-bash51-014.drv
/nix/store/crar8b49gsplly9x0v279bibvixmj9gc-bash51-003.drv
/nix/store/d7i8a7c8mb0qmsb1c3rj8g38m071vmaf-bash51-004.drv
/nix/store/gapa7v6rz1gzjsn1kckpb4fj07pmznw6-bash-5.1.tar.gz.drv
/nix/store/ig7d802vp43ap4ga26r2vd174h2c1bk7-bash51-010.drv
/nix/store/jj3jm1bjqnlwz4yassc9h70mwmrxy442-bash51-008.drv
/nix/store/krhwn1440gxvry5gw4wmzk6y83fm4bdw-bash51-001.drv
/nix/store/n92wsf556wqp4dbf0rxwx1b175m0vwyn-bash51-013.drv
/nix/store/nkzvvyvmckwv4a8r84iwyfbivvw05nvc-bash51-009.drv
/nix/store/nm5946y3ffkynrz67vz47ik0ygvg6byn-pgrp-pipe-5.1.patch
/nix/store/pkd2vxq8w5fhrfk6k89hi29d5ldbbj29-bash51-005.drv
/nix/store/q6jpdv2j5dh4nbsbmkzy6za1vfpb2l30-bash51-011.drv
/nix/store/w8q9jdvb96sayxyi25amd27yki283zg9-bash51-002.drv
/nix/store/wg9gacyfgldnwh3gc23nr49n4j0b58sv-bash51-012.drv
/nix/store/4kpfa2fhfdb6r9icym3q8n3w1s8mfv6z-bash-5.1-p16.drv
/nix/store/k9bkzj7nhqxnvbmz5vk8pmzxpmym0qa6-file-5.43.tar.gz.drv
/nix/store/hgps4nk9p01z9zngmbnbv42pqmzg9nhg-file-5.43.drv
/nix/store/4cmjzk8yr6i5vls5d2050p653zzdvmvp-setup-hook.sh
/nix/store/4hcdpxjmr4nh625ry840g70xp00vdf5a-2.71-fix-race.patch
/nix/store/kxdvjnq8cl9jd5g9jndhhl5a17h2xbih-autoconf-2.71.tar.xz.drv
/nix/store/irpqw60zcy00lj3hjia8gr15z984x9xn-texinfo-6.8.tar.xz.drv
/nix/store/19ndr8g629l0xzzs1x7xz4z0fbkwpgcj-xz-5.2.6.tar.bz2.drv
/nix/store/kas3n4g0jyrz3rhl1znjcxqmpyddk8sw-xz-5.2.6.drv
/nix/store/5pj1w63j668yqssrxb4dykpzpm1yhx9q-libiconv-50.tar.gz.drv
/nix/store/xrvbfm0ahaiik1vlxzn3vsp5gyhksy2n-setup-hook.sh
/nix/store/5xx3gba361rf696b27r3jfa0q7rmlyh9-libiconv-50.drv
/nix/store/ny42y6hs4p294rvnrwbmrpwzqghw2816-gettext-setup-hook.sh
/nix/store/p2fp6i7hjx9af1wbwr32k217wp2dxmiw-absolute-paths.diff
/nix/store/sihz0cdcajckxnhjm8n4p652sbd5xwxd-gettext-0.21.tar.gz.drv
/nix/store/ri729qz1iq3iqr9bdvb406izklj1fpfa-gettext-0.21.drv
/nix/store/yl6g04fsr6p9lkvccqjjl8q1xnnmw49s-fix-glibc-2.34.patch
/nix/store/v94cwmp6hs6dvrw6v4jmqk9jwl0ik75q-texinfo-6.8.drv
/nix/store/ih062232k706fpydng4xlk75fpzraxmn-autoconf-2.71.drv
/nix/store/r5kd1di71n7xk9kjvrgyy75cz0c0skay-automake-1.16.5.tar.xz.drv
/nix/store/hqf9nllss9z0i3gmi8sv9kjcm9qhvf8q-automake-1.16.5.drv
/nix/store/ipdgmqcfn56mhgmq3hv3yy5xj2kj2ri7-libtool-2.4.7.tar.gz.drv
/nix/store/06nfwja5j8c36n780jvlwjv8gs2m7i3m-gettext-1.07.tar.gz.drv
/nix/store/qf3mzpvsmkrw963xchbivcci06078n13-builder.sh
/nix/store/j7jrmh8zz3jjcdsa050f1ja19nm07vz7-perl5.36.0-gettext-1.07.drv
/nix/store/lac4y6zxaqqhyf4r60p3ag68k3ckifvv-help2man-1.49.2.tar.xz.drv
/nix/store/k9223a4j2ar7j76zpjs8fmlfl9q76a76-help2man-1.49.2.drv
/nix/store/9gns0vpn7fajyzm3w2rsdbcz9pqgfsrm-libtool-2.4.7.drv
/nix/store/ghdamd4hl6yi7jysh1x3436fj1v9yvjb-autoreconf.sh
/nix/store/8byqd66k9p5zbiggz2a9frki47xqy28r-hook.drv
/nix/store/ing5qg4q87wdvm1h455c3xn889m2bbj0-coreutils-9.1.tar.xz.drv
/nix/store/66ayp7hm682rxhlxd061fvprrmf2zx3c-gmp-6.2.1.tar.bz2.drv
/nix/store/h96aykl4imzhfapnmavplr49v43c8apx-6.2.1-CVE-2021-43618.patch
/nix/store/k49s9lr0lw5zhwsz4ni4rf2643byqrak-gmp-with-cxx-6.2.1.drv
/nix/store/jp5jbqfxjazf38w63bipqf68h7hyq4v0-coreutils-9.1.drv
/nix/store/322332kbmj7ig7ii3cwlfjcg4mf5xgz6-grep-3.7.tar.xz.drv
/nix/store/m2qc8a9c4yr5xmqck50fpzzwzpqggbbw-stacksize-detection.patch
/nix/store/qk3pnajspb378zx6c8g0anj2d7z31a88-pcre-8.45.tar.bz2.drv
/nix/store/pgzgn3knxdn335qci805a49bvlnl4ppa-pcre-8.45.drv
/nix/store/l2bbsavfww8zv5a9ncldh83c9vsz3y01-gnugrep-3.7.drv
/nix/store/1igs2sr5j99180z801426ivzzbikxi7q-CVE-2019-13232-2.patch.drv
/nix/store/1k1wn8807yizgz3ghnbd4k6zsc0dzfkr-CVE-2014-9913.patch
/nix/store/2cq4hsc1v8ylccspw8351r72s56w1fia-CVE-2015-7697.diff
/nix/store/6np2acjv1nxcg0xzsv9a76wyrpxznkna-CVE-2014-8141.diff
/nix/store/6zqn6w9rwkgfa6z1hpagnh5xhz2dag6m-CVE-2015-7696.diff
/nix/store/97d26l91h0db8h0qkmhxwi5d8shrilv6-CVE-2016-9844.patch
/nix/store/p67r2s04xw8plqs0552rc5qyj5016wxb-bzip2-1.0.8.tar.gz.drv
/nix/store/ra4ikm6b0nxgi0sil4mk3ikkingm80x0-bzip2-1.0.6.2-autoconfiscated.patch.drv
/nix/store/awrvprhqr5j0n6n8zqss2i5cyv25wis3-bzip2-1.0.8.drv
/nix/store/bqwhj80hz1z49365miaqcxp4c2mzsfp3-unzip60.tar.gz.drv
/nix/store/cciw7lgkldvx25d77cxpjhh1iw4xghd9-setup-hook.sh
/nix/store/d9b2qrrq32jzdsdx4y33inzrra5n5z5n-CVE-2014-8140.diff
/nix/store/ly8k93l59mlzlgnq679vcp54nqpi4sdc-06-initialize-the-symlink-flag.patch.drv
/nix/store/mwkywhh9wvym79lzlk8gsanw5swhfb8w-CVE-2019-13232-3.patch.drv
/nix/store/p46prhgmv7ibjh9igfkbc6zfxbbi6sk5-dont-hardcode-cc.patch
/nix/store/p55a764pi2f4kkx3adb43bxb2dnb4z6r-CVE-2018-18384.patch
/nix/store/pdcj2chp5c2gvm2jc3shbajfc62kbx1i-CVE-2014-9636.diff
/nix/store/rdkdki1f24q8mqgnbsyk7gmh28c027ks-CVE-2014-8139.diff
/nix/store/wx62rx7078a86mpimgg5gfsiisx3qk5l-CVE-2019-13232-1.patch.drv
/nix/store/zxpjddlgb46cdynbgbgq41i6k9a40wfg-unzip-6.0.drv
/nix/store/cnds925pfnac943p1f516pxwrbqy0gdi-source.drv
/nix/store/2cqnhs2ds0gn7xrq0zcwbj7gsv6l5xr7-use-etc-ssl-certs-darwin.patch
/nix/store/2yk6ab4c6j9y00g3x3cixqgi9jmgiwzd-openssl-3.0.5.tar.gz.drv
/nix/store/6hyy4ngzkxdsg71zmryvy3xkw0ydag21-openssl-disable-kernel-detection.patch
/nix/store/sq4h6bqjx12v9whvm65pjss25hg1538q-nix-ssl-cert-file.patch
/nix/store/imc07k6kg26rcam012pkgxba3mj0c0xq-openssl-3.0.5.drv
/nix/store/1ksmnsr3m6paw8gs7jp9b623agzdrqi2-add-flags.sh
/nix/store/9whvblgb7bgnmqsv7y5xqs1w8xv9aa1d-pkg-config-wrapper.sh
/nix/store/c4akajrb4jg50k72jw7zfbyv8z139ri0-setup-hook.sh
/nix/store/f4bvwqvj0y3z6blvh0knz71a8yq1c45p-requires-private.patch
/nix/store/qycyfzgf92i96ygij2b5bz27ll6mkyyw-pkg-config-0.29.2.tar.gz.drv
/nix/store/dq5y5c22p6ixswcqaxb6s0ymvi2bwmlm-pkg-config-0.29.2.drv
/nix/store/ssvy1s8p78q1jfy7bap0kl49sm8ad0m3-pkg-config-wrapper-0.29.2.drv
/nix/store/xz6rbdix12jn1bd3lydd1cagnvr94yf4-sigtool-0.1.2.drv
/nix/store/gp50m2w3aab5w1pgx9h18yky5x5jzzyq-signing-utils.drv
/nix/store/gz78khbgfz3rh5phvq1bavdp4v0bcimn-post-link-sign-hook.drv
/nix/store/zp333xdrvsgn3mjicwcbfiqd259ix6gd-MacOSX-SDK-11.0.0.drv
/nix/store/x3wxdzi7f36fnb1sryr1ifgafsycasks-libSystem-11.0.0.drv
/nix/store/v77imik30yacsdbfqkkdv0djyk1hsdgh-bootstrap-stage0-binutils-wrapper-.drv
/nix/store/6cqn1ln7v306ymslgmvcy77pbq30pjy1-bootstrap-stage0-clang-wrapper-11.1.0.drv
/nix/store/3inq067xw7bic7dy828bgjjzx54kav9v-install-shell-files.sh
/nix/store/70pf3jk5jc64jc82hqck1jx6z5l42xj3-install-shell-files.drv
/nix/store/zwlzlqvh3x2nw1421cvx2210bzz3xgfn-libev-4.33.tar.gz.drv
/nix/store/gn80i99rcc85d7l687d1jdmcm0yl51yv-libev-4.33.drv
/nix/store/h60a8qk9wqy8gbdvl9sf0qcnz63by9w4-nghttp2-1.49.0.tar.bz2.drv
/nix/store/09ba5xcaaaybqdsvljh5skzzl6blmmw4-c-ares-1.18.1.tar.gz.drv
/nix/store/l0niywhmkdqv97i8rlxzr1yqbn9k7sc1-c-ares-1.18.1.drv
/nix/store/36rbachr8ra090v3m6s86603sfp382k4-nghttp2-1.49.0.drv
/nix/store/fgr4mizzn2y712bqlk895lk8wpws27ir-dyld-433.5.tar.gz.drv
/nix/store/7c2sh9fyqz113rrpx5mdnmkk8mdrhb47-dyld-433.5.drv
/nix/store/81gwh57vnrm6qpw3gxmdmrjsp26dxi7p-find-xml-catalogs.sh
/nix/store/1vaq58n8rvn8bbr9mcm3k30zkr63480d-hook.drv
/nix/store/68bzcamhirzd95vsh05wilz8p8vfvyb6-expat-2.4.9.tar.xz.drv
/nix/store/0vyw0ywxhng31zvxqia2y23ljjmzsdj6-expat-2.4.9.drv
/nix/store/345r2zz7pgiyk91j89qlf7mhs95jrv6f-no-ldconfig.patch
/nix/store/zi0m9pfmvy5lw89x7a8x674rm99i8qiq-setup-hook.sh
/nix/store/4aakllhrfd3r87a67g0hb6r37nk4ahqf-python-setup-hook.sh.drv
/nix/store/4j7gbzbahn5by6vvck1gcpjc95k6vpz6-Python-3.10.7.tar.xz.drv
/nix/store/9m54l1bi5814x9cqznwlga7yfs5ipi6h-nuke-refs.sh
/nix/store/pm08hy0dzswr0wj3n7nczm5pbzzjxdh6-darwin-sign-fixup.sh
/nix/store/4qmyys335vfbmyx2q8ii3md77yaswsim-nuke-references.drv
/nix/store/57kclla9vza2n87xgwg1ap54d20cz6lb-fix-finding-headers-when-cross-compiling.patch
/nix/store/aafa965mg7grhivxa01mmbqksz6c3w77-python-3.x-distutils-C++.patch
/nix/store/cv1ynpzvjjr0s72jkbblbzz3ymr87lpi-0001-On-all-posix-systems-not-just-Darwin-set-LDSHARED-if.patch
/nix/store/dkb2rjyj7lwmvsn4zzwx85kx8r61nk9w-darwin-libutil.patch
/nix/store/w7hflmy5kddj6p1kvbkgag7qjs44217d-libffi-3.4.3.tar.gz.drv
/nix/store/nv7ln6adf9vv2c81rw1rv8sarp2w3dbp-libffi-3.4.3.drv
/nix/store/r112dk8w7zvdjipki58ch00m825li7fq-virtualenv-permissions.patch
/nix/store/x6aiw4vay2b63slqz5byimn0alhg5b1s-darwin-tcl-tk.patch
/nix/store/70zdg3iypjrxjyvj602ai92j36j8l4rp-python3-minimal-3.10.7.drv
/nix/store/1qrnbw8xsww3vydd71lwfp32ylgx9i8g-make-wrapper.sh
/nix/store/819fzxfwzp7zhhi4wy5nkapimkb1bsx5-die.sh
/nix/store/csphakh9ck533qnjfqmrh5ybg7amwvwv-hook.drv
/nix/store/scgakk3jkkkqfzxp5v9575163dj03c2y-hook.drv
/nix/store/8p4sgrqajxwzcm9l02m45qvpg6ncr0h9-patchutils-0.3.3.drv
/nix/store/baz2nahq7z7xxya1gi7in6a4msmvkbly-5b2d07a72670513e41b481a9d922c983a64027ca.patch.drv
/nix/store/frr6f2hq56j6b4wc0bsklaqskjsagqc0-utf8-xmlErrorFuncHandler.patch
/nix/store/vyh448kgn8qx2frx4g42f64b1akic218-libxml2-2.10.0.tar.xz.drv
/nix/store/lyl7058saady3i75h1w0177qfzfr1zf0-ncurses-6.3-20220507.tgz.drv
/nix/store/wy5amsi09scnbxgsbm1fzzq9963zlg9m-ncurses-6.3-p20220507.drv
/nix/store/x1fa0bns4szjkbb7f8bsflcxmzas41h0-4ad71c2d72beef0d10cf75aa417db10d77846f75.patch.drv
/nix/store/9gql9xbn6mfd56lxxchd0q7qzyf7cdby-libxml2-2.10.0.drv
/nix/store/1nv6k9zyc7pj74yshdzm4bmjfv6k86l9-source.drv
/nix/store/34qn4by9lqrri323ahm5vizv6bgsbhfn-006-darwin-always-set-runtime-c-flag.diff
/nix/store/chhz1kdhnql7gshwrns13lawgm75an7c-adv_cmds-119.tar.gz.drv
/nix/store/bylhfm7hj9sm4qb5n9mnsvj71xhmi6rx-flex-2.6.4.tar.gz.drv
/nix/store/vila3sxd48ha6r4yhdbfzqlvfl1jn2bw-glibc-2.26.patch.drv
/nix/store/lnb1468vfblvbc6lqgpigypspa4lzl68-flex-2.6.4.drv
/nix/store/6s064qz2lzpi1ml9z4vx0ajmk7fwafv6-bsdmake-24.tar.gz.drv
/nix/store/pps2jxig0cgkz81qwhy9gqar360mbbdb-bsdmake-24.drv
/nix/store/x1dh5wnl7pf81iq0gx0gqj6i9vnz89vv-source.drv
/nix/store/icl9b9dikbnwsrb5agnjmfryxyjnfp1n-adv_cmds-119.drv
/nix/store/6wbmq1k5x7q9lchs986bjq2qf1ip7b41-ps-adv_cmds-119.drv
/nix/store/7qslhycy1d0ag13xn4rfxfwdm8f7afb1-001-search-path.diff
/nix/store/ar1p4gcvlqf8dwbkfrcb01srbywinaj5-check-pc-files-hook.sh
/nix/store/ha21dnn4nw858g8d0wrkvhyvp7zmqgnz-setup-hook.sh
/nix/store/jmif3w9zsykc13zrhw4y8pynnnxg27zn-cmake-3.24.2.tar.gz.drv
/nix/store/k845qxmkbra9fc4628lpi0q8yjmc1sx9-005-remove-systemconfiguration-dep.diff
/nix/store/ri7qddqm02y0w2g43zqqz8lzy2pbdgrk-002-application-services.diff
/nix/store/rq41inv92jszcs5x62nc5cci5hapbjpw-003-libuv-application-services.diff
/nix/store/23dflh1nkw215df7bfyy9ml3jd5ranrw-cmake-boot-3.24.2.drv
/nix/store/c14fh88kpi7gc627s1l19gdlipfrwd59-brotli-1.0.9.drv
/nix/store/rv3w6kch2d0l70r6h3kk2r5d8ca216hz-libobjc-11.0.0.drv
/nix/store/f07bc31w87jm2rjk8zap5xyf92ach79p-apple-framework-CoreFoundation-11.0.0.drv
/nix/store/k8xvsl4226pzy73ywglgx46h7scffpjq-gnu-config-2021-01-25.drv
/nix/store/h9gslm9dppn38plwa811yr5c03s5lw9w-ICU-66108.tar.gz.drv
/nix/store/mqvcwr74dcsqlib5crdcawk16dmdgj9h-ICU-66108.drv
/nix/store/rkr3wamhhf9ha9n89yimjwyazvf3ar6j-hook.drv
/nix/store/f0qv4kz20212qcnd9wsck36zk3r8isl9-curl-7.85.0.tar.bz2.drv
/nix/store/gdqnvkbp6nnrvww108adb7nvjgrpdxzb-7.79.1-darwin-no-systemconfiguration.patch
/nix/store/3bld52y6l8fg58gaj9b937qg6m7zbm16-krb5-1.20.tar.gz.drv
/nix/store/3xk9ps0qz073k641b88swpa4fgx3hzwg-nix-ssl-cert-file.patch
/nix/store/n3vnxwsnf75gz250yayipdga4ziidwpi-openssl-1.1.1q.tar.gz.drv
/nix/store/82cq1qadbgv5d6gxb11zgkxl530wvzxj-openssl-1.1.1q.drv
/nix/store/18vddqgdxg6xcv5iws1vv7fd152rag04-bootstrap_cmds-121.tar.gz.drv
/nix/store/jyci5k74rnj58fkalyil3pj28x7xnr3m-bootstrap_cmds-121.drv
/nix/store/hj7zxy2r8ib6s6fa669kr6hqdiv4l6s1-libkrb5-1.20.drv
/nix/store/z3h1d8wp61892ydalxldvb496ar0hiz6-libssh2-1.10.0.tar.gz.drv
/nix/store/zrh6il3gp9xa58ldg40d57kwgsvljyb1-openssl_add_support_for_libressl_3_5.patch
/nix/store/yf97cpb80lyvqgd0lnq82c4qkx7kpb9f-libssh2-1.10.0.drv
/nix/store/w5683845xkfzwlp8sgbax0farj5fzhpv-curl-7.85.0.drv
/nix/store/9rkj0y4cl1sbbzndzg01crdamv4813pg-bootstrap-stage2-stdenv-darwin.drv
/nix/store/labgzlb16svs1z7z9a6f49b5zi8hb11s-bash-5.1-p16.drv
/nix/store/hvl8g8b6n8m8dk16bdavvpg31g8zmk96-bootstrap-stage2-stdenv-darwin.drv
/nix/store/9lzpvga5gm5klwg28iv1hgf01g0hpfaa-hook.drv
/nix/store/96fgzfyknjaj6fc85ai2n68qfndbps02-hook.drv
/nix/store/6wky968nz63ndx7z6kppcada8cdj4hg8-bsdmake-24.drv
/nix/store/0w9k3ah3f9c0j7k4vxka74pi07x01bbv-adv_cmds-119.drv
/nix/store/2n3wbbh9sk778vkl1lsz58inmyvk2g3r-file-5.43.drv
/nix/store/bcv1p9lpghn2l1zcw21z7401qc8fnmvr-gnu-config-2021-01-25.drv
/nix/store/47msbw943yjc7hm6d13r9jl5cz0ih9x9-hook.drv
/nix/store/24a06br9jvy87sbanym8hijfq4j2dsqm-no-threads.patch
/nix/store/4a0sl25fn3ymdmaalxwvjk6a2xajy3cb-libcxxabi-11.1.0.src.tar.xz.drv
/nix/store/ccf2fg1l77aqbw3v8hiql7a4c54dr8lh-bootstrap-stage0-clang-wrapper-11.1.0.drv
/nix/store/bhmp58x5m3lkscnxs9zwscc4rxbz7fc4-bootstrap-stage2-stdenv-darwin.drv
/nix/store/db7hhqin9klk8qx344r2b3dhb4xrfiq6-llvm-11.1.0.src.tar.xz.drv
/nix/store/il3mvxijf7cc9ys09pcblff47ia93kk2-gnu-install-dirs.patch
/nix/store/z3pj61rk5h9ffbj5anhwbp3ah2qysvqf-libcxx-11.1.0.src.tar.xz.drv
/nix/store/fg68n6bycig5c23sw8yfn7nmgbj85v6x-libcxxabi-11.1.0.drv
/nix/store/wjgikzdk0fcbldspzlkyh0dvd8wa2say-patchutils-0.3.3.drv
/nix/store/3v9a47xl4w8kc8bff4daxvbg50008imh-19bc9ea480b60b607a3e303f20c7a3a2ea553369.patch.drv
/nix/store/c9w69kl4caarcs2j84hck0icrdj9jqr6-fix-darwin-dylib-names.sh
/nix/store/g958ikb42h89wl8rgx597l5h6k9n2cfx-fix-darwin-dylib-names-hook.drv
/nix/store/ym4y16msxvvpbcsc0s829has6v8mxg56-gnu-install-dirs.patch
/nix/store/hhn96pp2rk2bq1hipcr147hqfrgh80gk-libcxx-11.1.0.drv
/nix/store/rizgpw7ndpwy12kyr03mnlhhkfwzk75a-pcre-8.45.drv
/nix/store/m1pm94jj46gsmks3d11p44qdhqml9inm-gnugrep-3.7.drv
/nix/store/r2mi8209hbvfhyhjcxy6qqvyawf8s4k3-expand-response-params.drv
/nix/store/6yjiri44dy8c8lnjn0f14w8nvgs2fhf0-bootstrap-stage3-stdenv-darwin.drv
/nix/store/dlm9y4dfkjmcqrysf37kxfhlds9r9jng-hook.drv
/nix/store/q6x1zg4xsbzw7qv3qdcq2rny1n4pr5xk-hook.drv
/nix/store/iraif23i0p01sx6qq6jkry21v7g84wvi-bootstrap-stage0-clang-wrapper-11.1.0.drv
/nix/store/wpni47ni5xf8qms83in475fyn8z2ikf6-bootstrap-stage3-stdenv-darwin.drv
/nix/store/40ri4k2mfvs5wjwry47iqv30587p1jh0-patchutils-0.3.3.drv
/nix/store/0w90wllxcb2wyjbkxjacm0m3q2wfz702-uops-CMOV16rm-noreg.diff.drv
/nix/store/09q0yxa6ixb030mkw96j2za7h8dpbpc7-dejagnu-1.6.3.tar.gz.drv
/nix/store/fk7p458jm8ra2d6zf2y4nw1ykckvmnrr-tcl8.6.11-src.tar.gz.drv
/nix/store/5z49kw0iq4qyga5zxmmhw1fh2l6jiwjz-tcl-8.6.11.drv
/nix/store/g4c3jbhc8ag6db5py0xk2sicfy0hrpmw-tcl-package-hook.sh
/nix/store/a1ipqs2qcpbqyfmxgk6yi3yyl2f6pd62-tcl-package-hook.drv
/nix/store/4vq3350zc6sqnibkqpgic2d6cvi1r9hq-substitute-all.sh
/nix/store/5241l4i852qd9imqz3jgv9rv9gv701gk-fix-cross-compilation.patch
/nix/store/dhba38jjxia0b5snjrhvcl9dbjbdb3k0-fix-cross-compilation.patch.drv
/nix/store/gdag5rjmiv9iwgj8gnibcvzic5f1kwbp-0001-enable-cross-compilation.patch.drv
/nix/store/qcmyh5mgqv62zip6gkp2xjriklpbm0xv-expect5.45.4.tar.gz.drv
/nix/store/xpdirxij63a69jk43pgajjrgmv7gaajd-hook.drv
/nix/store/iag2icih50jb6wxn15a71jy9pix7jd15-expect-5.45.4.drv
/nix/store/nharms54shj3rhwzw2ywk4alfrgm5k1m-dejagnu-1.6.3.drv
/nix/store/2hc51kpv7vkbfpifjq28jbhm49wlphzw-libffi-3.4.3.drv
/nix/store/6wv8acdd7bm7npixgr3rk86mf55fj47c-llvm-config-link-static.patch
/nix/store/9fcwwdr92g5wzpj2wxf86f0zy5mn0h1v-zlib-1.2.12.drv
/nix/store/9fd3xdcfv1dw93y99a18lw735fx8kvgy-gnu-install-dirs.patch
/nix/store/g05jynqyglkf9if6y70822l2r6y3nkj5-ncurses-6.3-p20220507.drv
/nix/store/2mys4xnihsf6r5y0sbby0y3qcn22ggjw-4ad71c2d72beef0d10cf75aa417db10d77846f75.patch.drv
/nix/store/2nyygvchsc258gkqymnbzmh741wsizrf-libiconv-50.drv
/nix/store/i68qy2hwsvqx3haf36smqi3n4lg1wavm-5b2d07a72670513e41b481a9d922c983a64027ca.patch.drv
/nix/store/w8ma9ddjcfc3l3z4ng6rlwljxiw85fhv-hook.drv
/nix/store/j4h65frq4nx4kpl06sj5c3cz2lc9fdrz-libxml2-2.10.0.drv
/nix/store/kl8l1ci2ycc6y23vkxvjhlbz2p93zp3z-polly-11.1.0.src.tar.xz.drv
/nix/store/n1sl525i7qanfd75l8s1bbqn32fasma0-dfaemitter-gcc-12.patch.drv
/nix/store/qcb7ljbcrmgdf6xv0irgvdv6rivgj3md-nvptx-gcc-12.patch.drv
/nix/store/yzac3dpyb5cyndxjl0d9nrpwqmcz18dk-b498303066a63a203d24f739b2d2e0e56dca70d1.patch.drv
/nix/store/8vqfrpgwki8j8nk9j08g04vh1iqcm9bw-llvm-11.1.0.drv
/nix/store/2jlsizsg3hsj6p10cm11fx9rshsjwwri-clang-tools-extra-11.1.0.src.tar.xz.drv
/nix/store/34zhl915l308dpa7v2786z3xgbvy6398-purity.patch
/nix/store/akc6qlr586k4r5lwmj70i0mbb8wxz709-clang-11.1.0.src.tar.xz.drv
/nix/store/v2az1r12rfivd43pvq2s0brp60n54mqa-clang-11-12-LLVMgold-path.patch
/nix/store/bhdlpz3fgkzcrh94rsp76m0n0gwb6fxx-clang-11-12-LLVMgold-path.patch.drv
/nix/store/f91k74rxz9c8miqg843jf6dfq35jhpka-fix-darwin-dylib-names-hook.drv
/nix/store/yrskcbyfm56qm4vs9dnacg8mqpqx7qwx-gnu-install-dirs.patch
/nix/store/arqis7aqh6b9p3a90idcjnr21fp1d0c4-clang-11.1.0.drv
/nix/store/79xln4yb0zql3j1zvc72yfi1y6333crl-disable-rpath.patch
/nix/store/dvdql179kllliqznwkd307bvdny2h96h-source.drv
/nix/store/5ks4wyqmh20wzz3i2yyqky7g0g8jhmsk-libtapi-1100.0.11.drv
/nix/store/aipzgrzywrh1qgw2l3bigbnnwpyr61kn-source.drv
/nix/store/fz56qb3cymbf2acghsqmdgjwwklc411f-install-shell-files.drv
/nix/store/r9iy2wdkq3w0n1hbyg92c2sqg3vcbkhl-ld-ignore-rpath-link.patch
/nix/store/3jjd65b6nyg7g30ixszjcsgb08j5mmhn-0001-Add-useless-descriptions-to-AC_DEFINE.patch
/nix/store/f3ygraph3msfdkyrqg91j7smx1c78qnd-bzip2-1.0.8.drv
/nix/store/j3frsgc0zsrg2pg7w9pqmxjh6qd01aqs-0002-Use-pkg-config-for-libxml2.patch
/nix/store/y26ic2b9n1g1cng3s68753qcxd6fvqrq-xz-5.2.6.drv
/nix/store/yqdd6m0r80c5pn3z7wc1mhn1wqmyli4i-xar-1.6.1.tar.gz.drv
/nix/store/1m30bskfc8z8r4dhb2qv9sd7jyl92srx-xar-1.6.1.drv
/nix/store/7vs1bbfsk0w6p6n5c4bqs3mp7q6n9lyd-source.drv
/nix/store/paybkfdbyh40jzyv6l5ywsbaabqy1sav-pbzx-1.0.2.drv
/nix/store/vwlpvn89jh6h45dj8q9nin0iv7rw85qb-MacOSX-SDK-11.0.0.drv
/nix/store/vb56s92027cg2c6573dahs6830fhz9xk-libobjc-11.0.0.drv
/nix/store/zr59kiajvksmks3vl1hja2ybix9z2zqk-ld-rpath-nonfinal.patch
/nix/store/ldj50kzrjbzh8dzcb7mqqa5gqsmc33v9-cctools-port-949.0.1.drv
/nix/store/0df8rz15sp4ai6md99q5qy9lf0srji5z-0001-Revert-libtool.m4-fix-nm-BSD-flag-detection.patch
/nix/store/k1cgpjsl77c8wfaq0w7n6k1i7fvxr5p8-gas-dwarf-zero-PR29451.patch
/nix/store/lgniihp1bk6mkd5nn9y5ikfim2ignr52-0001-libtool.m4-update-macos-version-detection-block.patch
/nix/store/pa83jbilxjpv5d4f62l3as4wg2fri7r7-always-search-rpath.patch
/nix/store/dqgzlxvbzq4dih9ska9k0y91sc1kv7d9-autoconf-2.69.tar.xz.drv
/nix/store/s8wb99pw1w8yspcz26zfadsy0j1k70ww-autoconf-2.69.drv
/nix/store/sqbhaaayam0xw3a3164ks1vvbrdhl9vq-deterministic.patch
/nix/store/xrw086zw3xqsvy9injgil8n2qdkvkpff-0001-Revert-libtool.m4-fix-the-NM-nm-over-here-B-option-w.patch
/nix/store/zbdl2p9amxdkr9cqjq0yv6h0mr55lm3l-binutils-2.39.tar.bz2.drv
/nix/store/zki7kfvf2f0xdksq9hp004xz1hsxklz3-texinfo-6.8.drv
/nix/store/q1kz46q80wj4bfc314g5p3sylpilpv0i-binutils-2.39.drv
/nix/store/00fij0grbvf9svcxvyk5ys51qcpmk7sa-cctools-binutils-darwin-949.0.1.drv
/nix/store/17agldwh525770zc3w11sdkpdxq8xwjy-gnu-config-2021-01-25.drv
/nix/store/0kkx3whrs8zb85qwwvl42ax99hmk0xpz-pcre-8.45.drv
/nix/store/3qkad2sv1xwngyn4gmx473mzrjhs2jx8-gnugrep-3.7.drv
/nix/store/xn8bjkw4fmyr2xvk9higd54g9s7q2kdz-gmp-with-cxx-6.2.1.drv
/nix/store/hbby7876a2qhk93hlx5ppr3jpgm1lwkl-coreutils-9.1.drv
/nix/store/vj0ai85srlbfn0yvd6mdql2nxan24naa-post-link-sign-hook.drv
/nix/store/vsd7hdcfnzn5n4q44flcdiaa2lv58d6d-signing-utils.drv
/nix/store/z4gcxwcrzc0mkx0zgha8k4jr506kgns7-expand-response-params.drv
/nix/store/vnxdn7rjmsm0naz6sgb98flh437iff1g-cctools-binutils-darwin-wrapper-949.0.1.drv
/nix/store/5gm6pb695hmb0q26cyvmm0ish0p5yig0-clang-wrapper-11.1.0.drv
/nix/store/2cw54rrcb7plvq6v5hxsm3sb42kq6fk5-bootstrap-stage3-stdenv-darwin.drv
/nix/store/3ic95d8vv23cdj4vq7634zh5zcdsda1p-normalize-var.patch
/nix/store/3m53ki7pr92hacq8mghsldg1wc4wrifm-codesign.patch
/nix/store/706qcmh667cmjwffc4vbjs9c745c7hs0-gnu-install-dirs.patch
/nix/store/skwzly3754w50q8mzdpadz8bsfmn6hs8-compiler-rt-11.1.0.src.tar.xz.drv
/nix/store/y87vwjq5v1fi0d077xqrsnkqrax3p4iz-libsanitizer-no-cyclades-11.patch
/nix/store/ylv0v02l6panidz2hkh756fz363yc68h-X86-support-extension.patch
/nix/store/1ffkl3b9gb1qyvmz2r1633vzkhd5bxn2-compiler-rt-libc-11.1.0.drv
/nix/store/9k3fqaqk3k7m510nn57ynd4ngx2x4rxs-clang-wrapper-11.1.0.drv
/nix/store/mmdgxk0mpsq2lzlja8g6mrdjzxpc3wmq-hook.drv
/nix/store/s9rdswvsx68yjwfk57vlw5a34hbjsl2v-source.drv
/nix/store/hrp64mrc7ss3zz8gfl36jfq8fj8qwk2b-libyaml-0.2.5.drv
/nix/store/y7wqq0qnhnhd6hr5d2hxl967fjssfrny-source.drv
/nix/store/vy20n6yc3nd8d1yk0sqa6cah7dpyhv9s-rewrite-tbd-20201114.drv
/nix/store/sn11j0j89hflj7snivdlxvxawvrpzp01-apple-framework-CoreFoundation-11.0.0.drv
/nix/store/aawhsgywk753j170584pf3r6rlismpi6-bootstrap-stage4-stdenv-darwin.drv
/nix/store/qwxrck5ibwhhhsgyblc711vnvw5rx2ib-bootstrap-stage4-stdenv-darwin.drv
/nix/store/bs639bs7frzx60c8bh3nyzmak49zbc3k-hook.drv
/nix/store/cfkvf8l9jw3vrvkss3c5i1ccgnp86nv6-hook.drv
/nix/store/skm4ysx9pk4nnwx75fpk9vghzc130887-perl-5.36.0.drv
/nix/store/ma5p31xpqrcyk0z70l14m7cklw2zkb5s-patchutils-0.3.3.drv
/nix/store/lapsha9pivk9wvrwlrc482i2biq06gw5-CVE-2021-38185-2.patch.drv
/nix/store/ncfbi3qgbflyph4x2ngcnz2584kykzqa-CVE-2021-38185-1.patch.drv
/nix/store/pklid951p82izlw5f06w5yvpps1zwgxw-CVE-2021-38185-3.patch.drv
/nix/store/sp2alvzdl09796wpg2wdf68akiha4d4g-fno-common-fix.patch.drv
/nix/store/zmadr12vmal7mwlgy1w4w4x70lss6j73-cpio-2.13.tar.bz2.drv
/nix/store/d54hwx5g50niakv2lpb9lkp1jjk910q1-cpio-2.13.drv
/nix/store/4yn89klg688jxj8sidmzc84hl7ndcwkm-pkg-config-0.29.2.drv
/nix/store/416vhsxki7508q1ijs8n415fqmvjxyky-pkg-config-wrapper-0.29.2.drv
/nix/store/a736nzx1nigikprmk4ignqzndmz7ls0m-gettext-0.21.drv
/nix/store/2szis9v9c9dzazajlflfdc9jl3b0pihg-gnum4-1.4.19.drv
/nix/store/gbznai4iy45kxmlnrn56fn5m0x2rlspc-texinfo-6.8.drv
/nix/store/f33p3mlclvl3hhnnjsnzw70bshn7criz-autoconf-2.71.drv
/nix/store/dw19klga9vppaq2f6lzj9h7bl4c29mga-automake-1.16.5.drv
/nix/store/hizv414b6ky026kw5f4hwgm2lbxzh08y-perl5.36.0-gettext-1.07.drv
/nix/store/ccwg6bkak9j236lc6k0n713iyn12k996-help2man-1.49.2.drv
/nix/store/jx8mci3vwqi9qv1wkbrfpjya00nl285j-file-5.43.drv
/nix/store/lahdhba85rpm60wxmhxanq1dqi8sa5kb-libtool-2.4.7.drv
/nix/store/g69zz30gq1rb85b6kdz5iidxxbwp1bda-hook.drv
/nix/store/hb2yk99cw015si2ry1l1fygp365as523-openssl-3.0.5.drv
/nix/store/cv65milx0bs2fk1xikgrgrhvkafkpqdk-xar-1.6.1.drv
/nix/store/9wfpm5alc542isr7232gg4qg5njdsgdq-unzip-6.0.drv
/nix/store/ggp35l799v2ggwsk73sz61y7wg3kpqy1-source.drv
/nix/store/msvf870j9sr6lwzakv6m263gk0r7126z-pbzx-1.0.2.drv
/nix/store/0b2hxys6lxyh567j82addkw2k36qjzgz-MacOSX-SDK-11.0.0.drv
/nix/store/0c1ijhg1cq01zcrvnhg24vhm5qn47kwd-libev-4.33.drv
/nix/store/0fqp7dz3rlrrhqjfc69wkmii3j5y0g7d-make-4.3.tar.gz.drv
/nix/store/bqlikyzhzhsjfirhzgmps9p99mhvn9az-bison-3.8.2.drv
/nix/store/c3kdwmns3lyigqqm6c4czisv0n226dy7-source.drv
/nix/store/hp3krbr0v290hwgrcskls6kk545virpz-flex-2.6.4.drv
/nix/store/mdihpwmpbkv1wg4yw03d7wy3fbs0l45w-bsdmake-24.drv
/nix/store/ln3xll7z1avhm03k3m8cdllln7wdgrrk-adv_cmds-119.drv
/nix/store/gs103r2mxcsjs3sw0ibvlnsv54qcw9q6-ps-adv_cmds-119.drv
/nix/store/94y4s4a30p8qqfg8bxr9rgwkdc9m3610-cmake-boot-3.24.2.drv
/nix/store/n91acyjrlchm0snw0w16i4683pf788ax-playtests-darwin.patch
/nix/store/vfb2ll7c9aq63mlkkvmvfq4ibiinq5nh-source.drv
/nix/store/vhp9nf4r8328m91l9l5c8fd9wlmb4bnd-fix-darwin-dylib-names-hook.drv
/nix/store/0w2r0sw68fwxqqki50mqx83iz1q6clgq-zstd-1.5.2.drv
/nix/store/4rj3r6gga5ipdfkiw9ahmrj9yr411ry6-libobjc-11.0.0.drv
/nix/store/vc3jlishkiy0qsw95smzzzr9vcgafi56-source.drv
/nix/store/jhs384scb8wk3sn9dw92khjpay91x9mg-libtapi-1100.0.11.drv
/nix/store/ylsnxqqfn3gpp0wr133z4ksj2bhklrg7-source.drv
/nix/store/z8gyza1abwd7jh3pv10r6kcrgphi2h2r-install-shell-files.drv
/nix/store/0xwx3m2lvpw92w4j45n1772f3aimskxg-cctools-port-949.0.1.drv
/nix/store/0y5flakfvnf813cwrr8rygf1jnk0gfnc-CVE-2019-13636.patch
/nix/store/4r8s8hcwyvvvnpcncps09zscqkh5qapx-no-install-statedir.patch
/nix/store/bljrd66ff2vp1zqikdfrz5x0k90kaw81-findutils-4.9.0.tar.xz.drv
/nix/store/10zrhmiqirncfbxyac8xrjg6p8mqf30k-findutils-4.9.0.drv
/nix/store/53d5wfhiifvxzgj847fva6q6py02m1g1-expand-response-params.drv
/nix/store/c2yrfg597pjcl1867pyir9jiq4fw3jl4-source.drv
/nix/store/9h8631c24qp90y7w0fvsl3c0dv8pv6pi-sigtool-0.1.2.drv
/nix/store/anpnd9wprrqhf1fdcwy96j66vb5fcsii-signing-utils.drv
/nix/store/5xzxmr5xpnqx0b0ar0kpy7kw0282a1jc-autoconf-2.69.drv
/nix/store/a921f1jk651ahri5f05gca9rwdiq3rlz-binutils-2.39.drv
/nix/store/laack7baw4rfxgvyqfrfydbn1v8zz9b6-clang-11-12-LLVMgold-path.patch.drv
/nix/store/d7h3zix26zzgdp0rzsyb19hrif8cbzmz-clang-11.1.0.drv
/nix/store/jxpxgb5hph4lw3s12g7lyqz0ci8a37ra-cctools-binutils-darwin-949.0.1.drv
/nix/store/w3hhid4crxafa1j03iq4a1y30d8p0sk2-post-link-sign-hook.drv
/nix/store/5w0k8f3ialhwr7p5g0y94zny3j74ryzn-cctools-binutils-darwin-wrapper-949.0.1.drv
/nix/store/74fhpxplxsc5qg1c67hb5picw88flx3d-libssh2-1.10.0.drv
/nix/store/76nc36kgrvhx8n9m8jz7ywrrqbcdkr48-gnu-config-2021-01-25.drv
/nix/store/9wyqdma0i671db7l4m0a3qbp6jpza2vi-tar-1.34.tar.xz.drv
/nix/store/90phqk429ip6kbi5jlm0lcg4h2xxaq2k-gnutar-1.34.drv
/nix/store/2j0fmwgm5ybgnc8jprc4ypcxw6s4r2nv-Allow_input_files_to_be_missing_for_ed-style_patches.patch
/nix/store/7mq3l9rhjbmpf06fwnrp51q6sy1l6g9j-patch-2.7.6.tar.xz.drv
/nix/store/8p3z4jsrxr5ck92iasc9bc7bmapb5mmg-CVE-2018-6951.patch
/nix/store/h2fcbw7ghgn3i4qadszdp272w4dab7ln-lzip-setup-hook.sh
/nix/store/vvciv7wkw3z9x0bj4jszb31crk0lix8y-lzip-1.23.tar.gz.drv
/nix/store/6gj38dbipcd2vbjcsv028jmpnn6bv1sz-lzip-1.23.drv
/nix/store/bv0xxgk72g693vdgs3w2w3d252hlxys9-ed-1.18.tar.lz.drv
/nix/store/lmssb21nd3zkv5gssngmk92bdf0q4h1w-ed-1.18.drv
/nix/store/npqvgz8c8w9kpj1gdma5bbn0pdkisyzp-CVE-2018-6952.patch
/nix/store/rxgi2l6jrgd5xmrrsbcv5cwi558lb36m-CVE-2019-13638-and-CVE-2018-20969.patch
/nix/store/sz6rhpf50kqh75fhqwl75q6dm6fr9xyd-CVE-2018-1000156.patch
/nix/store/aqmy225ay8m4yg51mib0bkpz3r1w2z7j-patch-2.7.6.drv
/nix/store/2k52bklbjhhq47dn35gm833vlh06fgfn-0001-No-impure-bin-sh.patch
/nix/store/6cc64ayl3fd2nc28ffw47cqsqi2bg1sn-0002-remove-impure-dirs.patch
/nix/store/avhna3r651j0frjk7jhy771za84mlh4j-gnumake-4.3.drv
/nix/store/b7mkkj1kbaxpihqh3k12s4a3viz9pdvk-hook.drv
/nix/store/dy63w31j33lknbd95fl81f24sndlgf35-source.drv
/nix/store/bl8jncx9dy4rr54cn8p1vwpf3wa01yyj-brotli-1.0.9.drv
/nix/store/rp4wqqv22pjl2235ra7ag3nb7yy0b5kr-diffutils-3.8.tar.xz.drv
/nix/store/d554acfihg4ssgij79ybd6ls0ww1p14x-diffutils-3.8.drv
/nix/store/szfjhkhmsxfyc289vz39882d3l866888-fix-error-darwin.patch
/nix/store/z8912zv98rl5yv104mf99j3k72xva3nr-libidn2-2.3.2.tar.gz.drv
/nix/store/qhs49gbxssyr8im8h2xc058gh4kdndv6-libunistring-1.0.tar.gz.drv
/nix/store/zipavm2mq94fsw09kx9mw7pi5n8xhkp4-libunistring-1.0.drv
/nix/store/gzy4kvn6djdm9b631fcm3g76pijsvvq7-libidn2-2.3.2.drv
/nix/store/hvp22x3rmpwfj6kcf0hj9dcv8lrkd4hs-clang-wrapper-11.1.0.drv
/nix/store/xhmwfi4xij5ryg9x2j0n6067ki55dscr-c-ares-1.18.1.drv
/nix/store/qpsbvsn7dl8gmlsmh474m2h9gmh8mg7i-nghttp2-1.49.0.drv
/nix/store/lwhmzpa1py1k244hfd3l026kc7r7b6ib-sed-4.8.tar.xz.drv
/nix/store/rvq62srcss99303nbgr94bq4av9kjv8q-gnused-4.8.drv
/nix/store/pid9is7y02wzdplvk6jcw2n0vfdh2y32-openssl-1.1.1q.drv
/nix/store/pz4hlrs0xa3q9knmn83v8v3wpf88iigz-bootstrap_cmds-121.drv
/nix/store/6m3w5kmj2m73nj3pakh6kaqjs2k64p5m-libkrb5-1.20.drv
/nix/store/sa6lxl61bh1wmr9rbpbyiq5wg2y5kbf2-curl-7.85.0.drv
/nix/store/vff2y41m68f5garsjmjxc0xfjrvw9pfm-setup-hook.drv
/nix/store/w99jp1rsykvc8rb09hr03c0rakw2dgzc-gzip-1.12.tar.xz.drv
/nix/store/swj6qdzryq4ln3h172s4h45wf0ks7g4j-gzip-1.12.drv
/nix/store/v994hjy8kmwi7g5li2lrpss92ldj0a54-ICU-66108.drv
/nix/store/pmxi9k28qls2yr7jhfnz3qp1fjchy64m-gawk-5.1.1.tar.xz.drv
/nix/store/x9ndmqlkrngf4jdy4zmvmal9ma7gh3z0-gawk-5.1.1.drv
/nix/store/5pfijbmkmy5kc81yzp0lpm4gpm2aq5rk-source.drv
/nix/store/zf7v9n0hxgb302wf08y762s0rhsbnqd2-source.drv
/nix/store/qr3r1g7n6xppyxb88726z7yr6r246nzd-libyaml-0.2.5.drv
/nix/store/91bfp6zivp9jq9sqq6iqq7vdpghdaffa-rewrite-tbd-20201114.drv
/nix/store/ya29pfy418vy1l0i5symnyprdb80c8ha-apple-framework-CoreFoundation-11.0.0.drv
/nix/store/cdk3pz11mvhqpphr0197wwmzhqppn7rl-stdenv-darwin.drv
/nix/store/26z459l0k3znhr99dsshkzj0il8dhwxx-perl-5.36.0.drv
/nix/store/sbcibnd6hym9c2rlbfnyhrbmlvgmsa59-stdenv-darwin.drv
/nix/store/sr9iyw9n2awaikjzvjfgwhvvn6vimf5w-pkg-config-0.29.2.drv
/nix/store/3zmkapnjbnajncxw7cix0lmj1fbspwa0-pkg-config-wrapper-0.29.2.drv
/nix/store/7dlkjg6cyd8d47qwiamxi77hld2z5360-mirrors-list.drv
/nix/store/i0zc5mm4vpj3lviyydb9s73j53mypkrg-nghttp2-1.49.0.drv
/nix/store/w37b5s734m53gxnzqyb5v0v98mhdfg2i-coreutils-9.1.drv
/nix/store/mmsrbggvzn6rwlx1ijw90sw3wvhzj18j-openssl-3.0.5.drv
/nix/store/n7iibs6b818v402j0yczf4mgy73sbzpv-libssh2-1.10.0.drv
/nix/store/z074ki54p77r7db3wsgxh9p18f67xnv8-curl-7.85.0.drv
/nix/store/hwymznwkd1kgf5ldcldjl9bnc1wz2azb-hello-2.12.1.tar.gz.drv
/nix/store/4a78f0s4p5h2sbcrrzayl5xas2i7zq1m-hello-2.12.1.drv

The above command not only lists the build-time dependencies for the hello package, but also their transitive build-time dependencies. In other words, these are all the derivations needed to build the hello package “from scratchâ€� in the absence of any cache products. We can see the complete tree of build-time dependencies like this:

$ nix-store --query --tree "${DERIVATION}"
/nix/store/4a78f0s4p5h2sbcrrzayl5xas2i7zq1m-hello-2.12.1.drv
├───/nix/store/9krlzvny65gdc8s7kpb6lkx8cd02c25b-default-builder.sh
├───/nix/store/labgzlb16svs1z7z9a6f49b5zi8hb11s-bash-5.1-p16.drv
│   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv
│   │   ├───/nix/store/3glray2y14jpk1h6i599py7jdn3j2vns-mkdir.drv
│   │   ├───/nix/store/50ql5q0raqkcydmpi6wqvnhs9hpdgg5f-cpio.drv
│   │   ├───/nix/store/81xahsrhpn9mbaslgi5sz7gsqra747d4-unpack-bootstrap-tools->
│   │   ├───/nix/store/fzbk4fnbjqhr0l1scx5fspsx5najbrbm-bootstrap-tools.cpio.bz>
│   │   ├───/nix/store/gxzl4vmccqj89yh7kz62frkxzgdpkxmp-sh.drv
│   │   └───/nix/store/pjbpvdy0gais8nc4sj3kwpniq8mgkb42-bzip2.drv
│   ├───/nix/store/3lhw0v2wyzimzl96xfsk6psfmzh38irh-bash51-007.drv
│   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv [..>
│   │   ├───/nix/store/nbxwxwqwcr9rrmxb6gb532f18102815x-bootstrap-stage0-stdenv>
│   │   │   ├───/nix/store/1i5y55x4b4m9qkx5dqbmr1r6bvrqbanw-multiple-outputs.sh
│   │   │   ├───/nix/store/59jmzisg8fkm9c125fw384dqq1np602l-move-docs.sh
│   │   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv>
│   │   │   ├───/nix/store/bnj8d7mvbkg3vdb07yz74yhl3g107qq5-patch-shebangs.sh
│   │   │   ├───/nix/store/cickvswrvann041nqxb0rxilc46svw1n-prune-libtool-files>
│   │   │   ├───/nix/store/ckzrg0f0bdyx8rf703nc61r3hz5yys9q-builder.sh
│   │   │   ├───/nix/store/fyaryjvghbkpfnsyw97hb3lyb37s1pd6-move-lib64.sh
│   │   │   ├───/nix/store/g8xg0i02aqwhgxwd2vnp5ax3d6lrkg1v-strip.sh
│   │   │   ├───/nix/store/jngr4r80x5jn482ckqrfh08ljrx1k86f-setup.sh
│   │   │   ├───/nix/store/kd4xwxjpjxi71jkm6ka0np72if9rm3y0-move-sbin.sh
│   │   │   ├───/nix/store/kxw6q8v6isaqjm702d71n2421cxamq68-make-symlinks-relat>
│   │   │   ├───/nix/store/m54bmrhj6fqz8nds5zcj97w9s9bckc9v-compress-man-pages.>
│   │   │   ├───/nix/store/ngg1cv31c8c7bcm2n8ww4g06nq7s4zhm-set-source-date-epo>
│   │   │   └───/nix/store/wlwcf1nw2b21m4gghj70hbg1v7x53ld8-reproducible-builds>
│   │   ├───/nix/store/i65va14cylqc74y80ksgnrsaixk39mmh-mirrors-list.drv
│   │   │   ├───/nix/store/7kcayxwk8khycxw1agmcyfm9vpsqpw4s-bootstrap-tools.drv>
│   │   │   ├───/nix/store/nbxwxwqwcr9rrmxb6gb532f18102815x-bootstrap-stage0-st>
│   │   │   └───/nix/store/ycwm35msmsdi2qgjax1slmjffsmwy8am-write-mirror-list.sh
│   │   └───/nix/store/lphxcbw5wqsjskipaw1fb8lcf6pm6ri6-builder.sh
…

If we were to build and cache all of these build-time dependencies then our local /nix/store and cache would explode in size. Also, we do not need to do this because there is a better solution …

Correct solution

The solution that provides the best value is to cache all transitive build-time dependencies that are present within the current /nix/store after building the top-level build product. In other words, don’t bother to predict which build-time dependencies we need; instead, empirically infer which ones to cache based on which ones Nix installed and used along the way.

This is not only more accurate, but it’s also more efficient: we don’t need to build or download anything new because we’re only caching things we already locally installed.

As a matter of fact, the nix-store command already supports this use case quite well. If you consult the documentation for the --requisites flag, you’ll find this gem:

       • --requisites; -R
         Prints out the closure (../glossary.md) of the store path paths.

         This query has one option:


         • --include-outputs Also include the existing output paths of store
           derivations, and their closures.

         This query can be used to implement various kinds of deployment. A
         source deployment is obtained by distributing the closure of a store
         derivation. A binary deployment is obtained by distributing the closure
         of an output path. A cache deployment (combined source/binary
         deployment, including binaries of build-time-only dependencies) is
         obtained by distributing the closure of a store derivation and
         specifying the option --include-outputs.

We’re specifically interested in a “cache deploymentâ€�, so we’re going to do exactly what the documentation says and use the --include-outputs flag in conjunction with the --requisites flag. In other words, the --include-outputs flag was expressly created for this use case!

So here is the simplest, but least robust, version of the script for computing the set of build-time dependencies to cache, as a Bash array:

$ # Continue reading before using this code; there's a more robust version later

$ # Optional: Perform the build if you haven't already
$ nix build "${BUILD}"

$ DERIVATION="$(nix path-info --derivation "${BUILD}")"

$ DEPENDENCIES=($(nix-store --query --requisites --include-outputs "${DERIVATION}"))

$ nix store sign --key-file "${KEY_FILE}" --recursive "${DEPENDENCIES[@]}"

$ nix copy --to "${CACHE}" "${DEPENDENCIES[@]}"

The above code is simple and clear enough to illustrate the idea, but we’re going to make a few adjustments to make this code more robust.

Specifically, we’re going to:

• Change the code to support an array of build targets

  i.e. BUILDS instead of BUILD

• Use mapfile instead of ($(…)) to create intermediate arrays

  See: SC2207

• Use xargs to handle command line length limits

… which gives us:

$ # Optional: Perform the build if you haven't already
$ echo "${BUILDS[@]}" | xargs nix build

$ mapfile -t DERIVATIONS < <(echo "${BUILDS[@]}" | xargs nix path-info --derivation)

$ mapfile -t DEPENDENCIES < <(echo "${DERIVATIONS[@]}" | xargs nix-store --query --requisites --include-outputs)

$ echo "${DEPENDENCIES[@]}" | xargs nix store sign --key-file "${KEY_FILE}" --recursive

$ echo "${DEPENDENCIES[@]}" | xargs nix copy --to "${CACHE}"

… where you:

• replace BUILDS with a Bash array containing what you want to build

  e.g. .#example or nixpkgs#hello

• replace CACHE with whatever store you use as your cache

  e.g. s3://cache.example.com

• replace KEY_FILE with the path to your cache signing key

Conclusion

That last script is the pedantically robust way to do this in Bash if you want to be super paranoid. The above script might not work in other shells, but hopefully this post was sufficiently clear that you can adapt the script to your needs.

If I made any mistakes in the above post, let me know and I can fix them.

by Gabriella Gonzalez (noreply@blogger.com) at October 24, 2022 12:26 PM