London, United Kingdom
Vincent Ambo (tazjin)
Vincent and I spent the week at Google Headquarters in London, where he and the notorious William had a week off for Hack Week. We teamed up, originally planning on writing an IPFS-backed Git-ish VCS, but after a few hours into the denotational design of such a thing we found Pijul. Which was exactly what we wanted to exist, and therefore took some steam out of our sails.
Instead, we decided to provide a language-agnostic Unison backend; an interface for the codebase manager, the backend storage machinery, and a plugin interface for interacting with languages. We got a few hours into a Haskell language plugin, before realizing GHC couldn't help us very much with the problem of disambiguating incomplete programs. Vincent went rogue and decided to provide the bindings in Rust, and so I got started on the underlying machinery. The notorious William talked about giving us Scheme bindings, but disappeared to play music during a 5 minute burrito break and we never heard from him again.
The project didn't get "all the way done" as you might say, but we had enough for a proof of concept, and it was sorta neat. All in all, it was an exceptionally fun time. Vincent was an excellent host, who showed me around the city, introduced me to some wild subcultures I'd never heard of, and together we tried to learn how to play snooker. Also a man put rice into Vincent's pocket.
Csongor Kiss (kcsongor)
Csongor and I headed down to his (and hopefully, one day, my) office at Imperial. I bullied him into working on his Unsaturated Type Families proposal, and we spent a good amount of time working through some of the particularities around their arities and backwards compatibilities.
Afterwards, we worked together on my Better Custom Type Errors proposal --- I am convinced that he and I are the two people in the world with the most experience in this stuff, likely by an order of magnitude. Csongor showed me that stuckness is an insufficiently interesting property for the type errors I'd like to be able to produce, and pointed me towards a richer vocabulary. Together we significantly improved the scope of the proposal's error algebra, and are going to change the face of type errors FOREVER.
Also we infiltrated me into the student bar where I illegally bought a beer, and made sushi promises to his roommate that we couldn't keep. Csongor has made me promise to come back and hang out more, and I absolutely plan to take him up on that.
Asad Saeeduddin (masaeedu)
My roommate for Haskell eXchange got the plague and spent the entire night throwing up and almost dying. As a result, I found myself stranded in London with nowhere to stay for the duration of the conference. Asad had a spare bed and excessive kindness, and invited me to stay with him after hearing the tale.
The result was some of the most fun I've had yet on my trip. During the conference, I found myself continuously impressed by just how much cool shit Asad knew, and bullied him into teaching me some of it. On the first night he walked me through tensors in monoidal categories, and finally convinced me that monads really are just monoids in the monoidal category of endofunctors.
On the second day of the conference, I fell down with the plague, and missed most of it. Asad was cool enough to walk me home (I didn't know the way,) and keep me company during the hours I was convinced that I was going to die. We had a great time sharing dirty rap songs and just bro-ing out. An absolutely delightful experience, and I have half a mind to cancel my trip and just go hang out with Asad full time.
Bratislava, Slovakia
Frantiaek Kocun (fokot)
Fero and I unfortunately only had a few hours to meet up, but he showed me around and hooked me up with traditional Slovakian food and excellent company. We dug into Unison, attempted to write hangman, and immediately found another couple of bugs. This time it's that characters always compare equal --- meaning a Set
will always say "yes" if you ask whether it contains a character. Nice.
I really like the idea of Unison, but dang there are a lot of bugs so far.
Fero is a Scala guy, and walked me through the encoding of typeclasses in Scala. And jesus christ that thing is a nightmare. I have so much more respect for Scala guys after that. The sheer amount of hoops they need to go through to get anything done is astounding.
We did all of this while hanging out on our laptops in a fancy restaurant, much to the disdain of all of the waiting staff. Sorry yall, but we had important programming stuff to go over!
Matej Niznik (TheMatten)
Matej and I have been collaborating on Polysemy for several months at this point, and so it was an absolute delight to get to meet in person. We settled in to the hostel we were staying at, and after an unsuccessful attempt at getting creamy garlic soup, we got down to business.
Beforehand, we had made a list of highest-priority things to work on in Polysemy --- namely reducing the complexity around Tactics
and Strategy
, and solving some issues around locally-introduced effects. We pair programmed on doing the insane type unification necessary to make the first one happen, and then Matej graciously answered all my questions about "how the heck is this supposed to work" for the latter.
All in all, it was a fantastic time. Matej really resonated with me --- I saw a lot of myself in him, and perhaps unfairly have much higher expectations in him than I do in myself. Thanks friend!
Munich, Germany
Elli K (github890)
Meeting Elli was rather unexpected --- she's a friend of my last host, and since we both had a day to kill, suggested we hang out. We ended up seeing some of Munich's best tourist traps, destroying our forearms rock-climbing, eating bad Thai food, and discussing some wild philosophy.
It turns out Elli is teaching herself programming, so I offered to teach her some Haskell. In my experience, most people leg it and scream in terror after such a proposition, so I was genuinely surprised when she said yes! Not only that, but she made remarkable progress after only a few days --- more than I have seen from a lot of people who get paid to write Haskell professionally. If anyone's looking for a very capable hire, I know someone you should get in touch with.
Elli was a fantastic host, and her hospitality made it truly difficult to leave Munich. Thanks Elli, hope to see you again sometime soon!
Justin Kaeser (jastice)
Justin is a Scala guy, and we spent a lot of time sharing folklore knowledge from our respective languages. In particular, I wanted to learn about how Scala's variance system works, and about what their effect system libraries look like. I was convinced we could write unsafeCoerce
by abusing Scala's variance system, but I guess Odersky thought about that because we couldn't make it work.
A while back, Justin bought an Arduino-powered necklace that came with a shitty C++ coding environment. We couldn't figure out how to build the damn thing, so decided to just reverse engineer the hardware and Do It Ourselves. After a few hours of futzing with LED matrices and lots of disgusting bit-twiddling, we could drive images on it. Success! Take that, shitty C++ environments.
We were also both quite interested in Unison, decided to download it and give it a go. Justin found a bug in the fundamental AST-handling machinery within a few minutes, and I found an unsoundness in their effects system. Surprisingly productive afternoon, really! All of that being said, Unison is an amazingly cool language, and I'm excited to give it more love in the near future.
Hanging out with Justin was a true joy. Not only is he excellent company, but he's a great story teller, and an exceptional host. He took me to Oktoberfest, introduced me to lots of his friends, and showed me motorcycles that drive on the fucking walls. Furthermore, Justin went out of town for a few days during my visit, and was kind enough to let me stay in his absence. I considered replacing all of his art with portraits of my face, but it seemed like too much work. Thanks again for a great time, Justin!
Leipzig, Germany
Soares Chen (maybevoid)
Soares and I worked our way through Conal's Compiling to Categories paper, and came to the conclusion that he was doing far too much work. Conal's implementation is written as a core plugin, which means he needs to do all of the hard work of synthesizing dictionaries and fighting against the optimizer.
Thankfully, today we have source plugins --- meaning we can implement syntactic transformations (such as compiling to categories) as actual syntactic transformations!
Our implementation is pretty tiny, but falls apart in all of the same ways as Conal's --- namely, you need to be able to inline all the definitions for any functions you call. We figured we could get around this by looking up unfoldings and then implementing a quick CoreExpr
to HsExpr
pass + aggressively turning on -fexpose-all-unfoldings
. We lost steam on the project after realizing how poorly the paper describes the actual implementation. Fun project, but it didn't really go anywhere.
After that, I suggested we implement a pragma for telling GHC "this is the type I want to see in my error messages." GHC will "helpfully" decompose types into constituent pieces --- which admittedly is usually the right behavior --- but this prevents you from hiding implementation details when it comes to Constraint
s.
The idea: mark abstraction types with a special {-# CANONICAL #-}
pragma, that tells error messages to never expand this type. If there's an issue with a subconstraint, report just the canonical type instead!
We actually got most of this working, though there are still a few bugs in propagating the pragma information from the parse tree all the way into the constraint solver. But once the flag is in place, the error messages do the right thing. Pretty cool, and hopefully coming soon to a GHC release near you.
In addition to all of this, Soares is the implementer of the implicit-effects package, and so we spent a lot of time nerding out about effects systems. We're both convinced that such things are the solutions to most programming problems, and just need to figure out how to convince others of that fact.
Furthermore, Soares comes from the Javascript world, and has a refreshing take on some of the problems we run into in Haskell that aren't in Javascript. In particular, we got chatting about Haskell's concurrency model, and how we could change it in order to make effect systems work better.
Munich, Germany
Jan van Bruegge (jvanbruegge)
Jan and I spent a lot of time chatting about row types; he showed me his new implementation in GHC and I asked lots of stupid questions about it. Together, we worked on some patches to GHC's custom TypeError
machinery. The first of which only emits custom type errors when they're derived constraints, rather than the givens that cause excessively loud errors today.
The second was to add a priority to type errors. Today, whenever a custom type error shows up, it completely erases legitimate errors from GHC. That means an insoluble type equality (eg. asking for String ~ Bool
) will get swallowed up by a custom type error that happens at the same time. It's never helpful, and means type errors are often actively unhelpful.
But GHC already produces two error reports --- the first is for really bad errors that happen (insoluble type equalities), and the second is for other things it would like to comment on. Notably, the second report doesn't show up if the first one happened. Jan and my work was to expose this to the type errors API:
data ErrorPriorty = HighPriority | LowPriority
type family TypeErrorPriorty (priority :: ErrorPriority) (msg :: ErrorMessage)
type TypeError a = TypeErrorPriority 'HighPriority a
This change is completely backwards compatible with TypeError
s as they're used today, but means we can now selectively control when a type error should be emitted. Nice!
Besides all of the great Haskell-ing, Jan and his roommates turned out to be some of the smartest, kindest and most fun people I've had the pleasure to ever meet. They invited me to their band practice, we saw some break dancing competitions, and ate an aggressive amount of traditional Bavarian food. Thanks everyone, I love you all!
Vancouver, Canada
Andrew McKnight (amcknight)
Andrew has some loft goals about getting AIs to optimize bad algorithms into good ones; in other words, you write a brute force algorithm and it some how "massages" it into something that runs fast. That seemed hard, so we instead decided to focus on GHC's simplifier, which performs similar transformations on Haskell code. We figured getting familiar with it might be helpful for Andrew's longer term goals.
We took up Reed and my idea to Scott encode the simplifier --- which should theoretically improve compiler performance by 20%+. After a few hours of prototyping Scott-encoded things to ensure we understood how they worked and why, we jumped into GHC and got going. In our first afternoon we got half of the work done, and spent the rest of the evening talking about huge world-scale projects we could tackle, and what modern super-powers would look like.
The next day we wandered around town for a bit, and then got back to business. After getting stuck in a quagmire of biting off too much for one commit, we undid some work and were more careful moving forwards. A lot of GHC's simplifier is written with explicit recursion, but contains lots of ugly fall-through logic in its pattern matching of such. It's a mess, and desugaring that into something that can take advantage of the Scott encoding is finicky and easy to get wrong. Would that GHC took advantage of good Haskell design principles, but alas it does not.
All in all, 10/10 visit. Would recommend, and would definitely return!
Reed Mullanix (TOTBWF)
(dates are approximate, I actually spent this week staying with Travis Willis, but Travis and I didn't do any Haskell)
As the only known user of Reed's library refinery
, I sat him down and had him explain most of the machinery to me. We spent several hours debugging his new Scott-encoded v2, eventually figuring it out, and teaching me lots about Scott-encoding in the process.
On our second encounter, Reed and I attempted to determine whether or not the polynomial interpretation of monads via Curry-Howard have any interesting number-theory properties. Neither of our category theory was sufficient to come up with any satisfactory answers, but it seems like a pretty interesting line of inquiry.
We then looked at my Dyna editor, working through the semantics of what structural editing should look like. We then spent some time diving into GHC's simplifier, trying to figure out why it's so dang slow (one function is singlehandedly responsible for 20% of compile times.) We're pretty sure that a Scott-encoding of the SimplCont
type would be sufficient to kick off wicked savings, but it seems like a nightmare to actually make happen.
Saskatoon, Canada
Chris Penner (ChrisPenner)
Literally the first thing we did, Chris Penner sat me down and ran me through optics. "They're just traverse
in different pants," he said. A few hours later, I felt like I had a pretty good grasp on the whole idea.
We found it a little hard to find things to collaborate on; Chris' big project these days is his Lens book, which is obviously not something I can contribute much to. But we had an excellent time hanging out, chatting about the ecosystem, and how to fix the problems in the community.
Also, Chris is an amazing musician. We broke into the music store and had a few jam sessions. I came away feeling inspired by the things he taught me on piano, and I can't wait to get my hands on one again to give the new ideas a go.
Toronto, Canada
Jonathan Lorimer (JonathanLorimer)
Back at Jonathan's, in a second push attempting to get weft
finished. We had a long list of things to do, and we powered through almost all of them. We pulled a few 15 hour days, aggressively programming as hard as we could. Things were looking promising to releasing the library --- just hours before Jon was going to present it at the local Haskell meetup.
But that morning, I'd decided to do a big refactor, using higgledy
to magically hide all of our HKD machinery. The approach is actually quite involved: instead of forcing your users to use a type family TypeFam a
, you instead wrap it with a newtype newtype ToTypeFam a = ToTypeFam (TypeFam a)
, and then HKD
over that. The result is gross, but it works.
God am I ever excited for unsaturated type families.
Anyway, such a refactor was an exceptionally breaking change. Literally every module we had assumed your code was written in the direct-HKD style. A few extra typeclass instances helped:
Assuming you have class GSomething (rep :: * -> *)
, with instances for GHC.Generics
, we found that if you separate the structural bits (M1
, :*:
, :+:
, eg.) from the interesting pieces (K1
), everything becomes much easier. We introduced a second typeclass for the K1
contents, and then implemented the structural bit in terms of it:
class GSomethingTerm (t :: *)
instance GSomethingTerm t => GSomething (K1 _1 t) where
= K1 gSomethingTerm gSomething
This separation allows you to easily inject the higgledy
-style HKD logic into a more traditional approach. You need to add two additional cases of GSomethingTerm
. The first is:
instance GSomethingTerm (Magic a) => GSomethingTerm (ToTypeFam a) where
= ToTypeFam gSomethingTerm gSomethingTerm
which expands your type family's instance. The second is:
instance GSomething (M1 _1 _2 _3) => GSomethingTerm (M1 _1 _2 _3 _4) where
= gSomething gSomethingTerm
which ties the recursive knot, connecting the GHC.Generics
-based representation of higgledy
back into the original generics instances you wrote for the traditional HKD style.
It's crazy, but amazingly, it works. I don't even want to think about how much work we're making the compiler do in Weft.
Enough shop talk. Jonathan also took me to the Toronto Haskell meetup which he organizes. I gave a beginner-level talk about the value of types, stressing Matt Parsons' old adage that if your business logic bugs aren't type errors, you should make them be.
Hamilton, Canada
James King (agentultra)
James and I bonded over a shared uneasiness with data versioning. It's tedious, and hard to do correctly. So we decided to build a data migration library, where you explicitly tag your types via a data family indexed by the version. OK, obvious idea, right? But not quite!
We realized that if you enable -XDuplicateRecordFields
, you can use the same field names between different versions. Which means we can now programmatically compute most of the migration details from one type to the next; if the name and the type stay the same, you just want to copy the data between versions. If the type changes, you want to provide a function to map it. If a field gets added, you can hopefully compute it via some projection of the full data structure.
Unfortunately we didn't have enough time to finish everything up, but when I left we were half way through writing a DSL for providing the missing transformation pieces. The idea was to compute a superrecord
whose names correspond to the fields you need to fill in, and then put their transformations inside there.
Richmond Hill, Canada
Boris Rozinov (oofp)
Boris has been working on a library for tracking dependent state management of resources over application lifetimes, complete with refinement of the possibilities based on specific filters. It's wicked cool, though performs compiles aggressively slowly. We looked at the performance, and realized the primary problem is that everything is encoded as type-level lists. We thought that maybe having a better type-level data structure would be effective.
So I implemented a plugin that solves a type-level CmpType
for ordering types. Such a thing means we can effectively write binary search trees for arbitrary types of kind *
, and now get all sorts of great performance improvements. We hunkered down on that, and then on writing BSTs in terms of it. But then I realized most of the work was actually in getting the plugin to solve the type family, and not in comparing types, so we spun out another library for generating plugins.
The result: three libraries. type-sets
, cmptype
and magic-tyfams
; not bad for a weekend of work.
On Boris' project, we found a bug in GHC's TypeError
machinery --- it explodes in the wrong place in the presence of partial type signatures. Having tracked that down, we did some work on existentializing his types so the partial ty sigs weren't required. We then thought about how to reduce the boilerplate in his library, and came up with a combination of Servant and HKD for expressing the state transition graph.
Toronto, Canada
Asad Saeeduddin (masaeedu)
Asad and I met on the University of Toronto campus. We were planning on infiltrating a lecture hall, but they were all locked up. He showed me his encoding of all user interfaces via (u -> m ()) -> s -> v
, and walked me through how it actually works --- pretty dang cool. We grabbed coffee, and Asad saved me a few hundred bucks per year in AWS costs. He walked me through some of the intuitions behind how lenses work, and it was an excellent time.
Ben Hart (Benjmhart)
Ben and I met up for dinner, and spent it discussing why Haskell hasn't taken over the world, and what it would need to be in order to do so. We then meandered down to his office, hung out on the roof on a Friday night, and coded up the most type-astronaut version of Tetris we could think of. The board is a Store
comonad, with gravity and movement being implemented as extend
s. A lot of the core implementation got finished, but the game aspect sadly not.
Jonathan Lorimer (JonathanLorimer)
Weft is a GraphQL implementation for Haskell, based around the idea that Haskell types should be powerful enough to encode everything you need to generate a GQL server. It uses HKDs extensively, to reuse the same data structure from everything from data, IO resolvers, parsed queries, and responses.
Also, Jonathan and Claire took me out to the art museum where we saw totem poles built out of sports bags. We had great philosophical chats (he is a philosopher by training!)
David Rusu (davidrusu)
Nimic is a tiny macro language, with no built-in syntax or operational semantics. I wrote a little blog post on it.
Together, David and I designed the language, wrote a parser and the macro substitution, and a "compiler." He added the bash
primitive, and I worked on the interactive stepper.
Also, David took me out for a pottery class, and to the computer scientists' dinner. We almost managed to burn down his house with an explosive barbecue incident.