David Thrane Christiansen @d_christiansen@types.pl

I'm overjoyed to announce that I will be starting as an Associate Professor in Logical Foundations and Formal Methods at University of Cambridge this fall!

Daniel J. Velleman has translated parts of his classic text "How to prove it" into Lean 4!

https://djvelleman.github.io/HTPIwL/

"How to prove it in Lean" goes through examples in the original book, and discusses how they can be proved in Lean. He also talks about how Lean's use of type theory rather than set theory affects this kind of basic mathematics, and furthermore gives clear installation instructions for anyone who wants to play along at home!

We're delighted to announce that the first ACM SIGPLAN Workshop on "Functional Software Architecture - FP in the Large" will be held in Seattle, USA in September 2023, co-located with the ICFP conference.

Please share, and submit your best papers, experience reports, and architectural pearls on large-scale functional programming!

The Call for Papers is open - deadline is June 1! https://www.functional-architecture.org/events/funarch-2023/cfp/

Higher-order unification is pretty hard when you also have eta-equality for record types and definitional proof irrelevance. There's just too many ways for variables to disguise themselves as other things.

For example, consider a constraint _f u =?= v : B where u : A:

• If u is a variable x, then we can just solve it with _f := \(x : A) -> v.

• If u is eta-equivalent to a specific variable x, say u = (fst x , snd x), then we can eta-contract it and still solve the equation.

• If the type of u is a unit type, then it is eta-equivalent to any variable of the same type, so if there are two variables x : A and y : A then we don't know which one to eta-expand u to. Luckily, in this case it does not really matter since we can just prune the dependency of the metavariable and solve it as _f = \(_ : A) -> v.

• The fun really starts when you add definitional proof irrelevance into the mix. If the type A is in Prop (or sProp for the roosters here) then u is definitionally equal to any variable of type A, but also pruning the dependency of the metavariable could now lose solutions since A might be an empty type! So what do you do then, do you just try all the variables in the context to see if they have the right type? What if there's a variable in the context of a record type that has a (possibly nested) field of type A? Do we then need to first eta-expand the context variable? If there are multiple choices, do we then need to pick one that makes the variables in the arguments to the metavariable linear? This all feels way too complex and ad-hoc.

I've been talking with an academic researcher who is interested in speaking with people who have shut down their fediverse servers, for any reason.

I know it's a touchy subject so I didn't want to just refer her directly to people, but if you are seeing this message and you're interested, please DM me and I will give you her email. I did a 1-hour interview with her on more general topics and really enjoyed the experience.

(Boosts appreciated!)

This is your yearly PSA: Most of the US have switched to Daylight Savings Time now, but Europe will not switch for another two weeks. Keep in mind that any cross-Atlantic appointments you may have could be shifted by an hour. (Or tell your European buddies that theirs are)

#dst #timeZones #international #travel #summerTime

@robysinatra @vedransekara These PhDs will proceed in #Copenhagen. In Denmark, a PhDs is considered a full-time paid working position (37h) with excellent work-life balance: https://denmark.dk/society-and-business/work-life-balance. Here also an interesting infographic about salary from a few years ago:

Robby Findler's excellent PADL keynote on modern macro systems, which explains Racket macros for the uninitiated:

https://www.youtube.com/watch?v=YMUCpx6vhZM

The 21st annual Oregon Programming
Languages Summer School (OPLSS) will be held from June 26th to July 8th, 2023 at the University of Oregon. The theme will be "types, semantics, and logic" and is being organized by Zena Ariola, Stephanie Balzer, and myself. More details, soon!

Quite a few people have registered to MGS'23, as usual. This is a reminder that the early registration fee ends in 6 days. After that, the registration fee increases considerably:
https://www.cs.bham.ac.uk/~mhe/events/MGS23/
Looking forward to seeing you there.

Really pleased to have pushed watch.ocaml.org out of beta. 130+ videos about #ocaml dating back to 2010 (and would like to get more historical ones) all available via PeerTube/ActivityPub. https://discuss.ocaml.org/t/watch-ocaml-org-out-of-beta-and-a-call-for-new-videos/11561

The Haskell Error Index now supports dark mode, thanks to a volunteer contribution from Jake Wood!

As an antidote to the other (declining) platform, I am actively trying to build bridges here. My expertise is in election technology, administration, security, disinformation, and defense of democracy. Most recently, I led the civic integrity product team at Twitter.

I hope you might enjoy my feed, if you’re not already following me.

And if you are already familiar with my work, would you please consider recommending me to your friends?

Thanks for helping to extend our community! 🙏

The 36th #Agda Implementors' Meeting will happen in Delft on 10-16 May! Find all the details and register at https://wiki.portal.chalmers.se/agda/Main/AIMXXXVI. Proposals for talks, discussions, and code sprints are welcome too!

A presheaf P on a category C behaves a lot like a "predicate" on C. In my category and types class I introduced presheaves under the name "predicators" (since we'll never get to sheaves anyway). P is a functor C^op -> Set.

Why is a functor P : C^op -> Set like a predicate? Well we think of an element of P(a) as a "witness" that P(a) is true. But the objects of a category are connected by the morphisms, so we additionally have that for any f : a -> b and proof p : P(b) we can "compose" the proof p o f : P(a). These have to satisfy some natural looking rules as well.

The reason presheaves are so central in category theory is that we use them to define *universal properties* by asking for the presheaf to be *representable* by an object. A representation of a presheaf P is an object a in C and an isomorphism Y a =~ P between the Yoneda embedding of a and P.

Does this notion of representability generalize something about predicates? Yes! First, the Yoneda embedding: the baby Yoneda embedding of an element a in a set A is a predicate Y a on A that is defined as Y a b := (a = b). So it defines a very small subset: just the element a itself.

Then we would say that a predicate P on a set A is representable by an element a in A when Y a = P, i.e., they define the same predicate, i.e., P(b) is true if and only if a = b. So at first glance this seems like a strange notion: representability of a predicate says that it is true of exactly one element?

But if we think of this in terms of logic, this is a familiar notion: saying a predicate P on A is representable says that there exists a *unique* element that satisfies it. So representability of presheaves is in fact a generalization of the idea of the unique-existential quantifier of logic. In fact if you look at the wikipedia page for unique existential quantifier [1] the 2nd and 4th formulation are direct analogues of two equivalent formulations of representable presheaves.

[1]: https://en.wikipedia.org/wiki/Uniqueness_quantification#Reduction_to_ordinary_existential_and_universal_quantification

Nominations to the HF Board are due by the end of the month: https://discourse.haskell.org/t/2023-call-for-nominations-for-the-haskell-foundation/5803

If you don't think of yourself as the kind of person who would be on the HF board, but you have a sincere desire to help the Haskell community, please consider self-nominating. We need many different viewpoints!