Bob Atkey boosted

I handed in my thesis!

people.compute.dtu.dk/ahfrom/ahfrom-thesis.pdf

Bob Atkey boosted

In tribute to Lawvere, here is one of his ideas that is simple enough to explain in one post.
The original paper is "Diagonal arguments and cartesian closed categories" (tac.mta.ca/tac/reprints/articl)

Lawvere's fixed point theorem is the positive constructive content of many diagonalization arguments.
Here I'll show how it unifies Cantor's theorem that there's no surjection from a set to its powerset and the construction of the Y combinator.

Lawvere's fixed point theorem in type theory:
If r : X -> (X -> D) is surjective (forall f: X -> D. exists x. r x = f), then for every function h : D -> D there exists d : D. a fixed point of h , i.e., h d = d.

Proof:
Given h : D -> D, by surjectivity there exists l:X such that r l = λ x. h(r x x).
Then r l l is a fixed point of h:
r l l = (λ x. h(r x x)) l = h (r l l)

Corollary: Cantor's theorem. There is no surjection X -> (X -> Prop).
Proof:
If there were, then every h : Prop -> Prop would have a fixed point, but not : Prop -> Prop does not have a fixed point (exercise).

If we strengthen the hypothesis we can get something which makes sense purely in the equational theory of the lambda calculus (i.e., no existential quantifiers) and therefore interpretable in all Cartesian Closed Categories.

Variant of Lawvere's fixed point theorem in STLC:
if r : X -> (X -> D) is a retract of s : (X -> D) -> X (i.e., (λ x. r(s(x))) = (λ x. x)), then we can construct a fixed point combinator Y : (D -> D) -> D, i.e., Y = λ h. h(Y h).

Note that in the presence of the axiom of choice, this variant is equivalent to the previous, but the most interesting applications are in settings without choice.

Proof:
Y = λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
Here s (λ x. h(r x x)) is the l in the previous proof, where our strengthened hypothesis gives us a choice of element rather than its mere existence.
Then
Y
= λ h. Y h
= λ h. r (s (λ x. h(r x x))) (s (λ x. h(r x x)))
= λ h. (λ x. h(r x x)) (s (λ x. h(r x x)))
= λ h. h(r (s (λ x. h(r x x))) (s (λ x. h(r x x)))))
= λ h. h(Y h)

Which is the Y combinator in STLC, which more typically is constructed using a recursive type X =~ (X -> D) with r, s the isomorphism, or in untyped lambda calculus which is equivalent to having a single type D where if only β is assumed then D is a retract of (D -> D) and with η then D is isomorphic to (D -> D).

Related expository material:
- arxiv.org/abs/math/0305282
- math.andrej.com/2007/04/08/on-
- cs.bham.ac.uk/~mhe/agda-new/La

Tested negative! Just in time for POPL to be over!

Every time the session chair at POPL says "Remember to say your name and your affiliation" I just think of Bruce Forsyth on the Generation Game asking "What's your name and where're you from?"

Bob Atkey boosted

The notion of model of intuitionistic propositional logic (IPL) I'm
most familiar with (being a category theory/PL nerd) is a Heyting
algebra (HA): a poset with finite meets, finite joins and a Heyting
implication. If you add propositional variables, the model includes a
choice of how to interpret them as elements of the HA and if you
include axioms, their interpretation must be true in the HA.

Then you can interpret every proposition of IPL as an element of the
HA where you interpret conjunctions as meets, disjunctions as joins
and implication as the Heyting implication. If G |- A is provable then
/\ [G] |- [A] is true.

If you look up what a model of IPL is though, you'll likely find
Kripke models, and they look at first a bit different: It's a pair of
a poset W, and a "forcing relation" ||- between elements of W and
propositions of IPL satisfying a bunch of properties:

1. for variables x, if w ||- x and v <= w then v ||- x
2. w ||- p /\ q iff w ||- p and w ||- q
3. w ||- true is true
4. w ||- p \/ q iff w ||- p or w ||- q
5. w ||- false is false
6. w ||- p => q iff for any v <= w if v ||- p then v ||- q

Despite the cosmetic difference, Kripke models are instances of the HA
model construction. Given a poset W, the HA in question is
Prop^(W^op), the poset of antitone functions from W to Prop
(classically, Prop is just the boolean order 0 <= 1). This has the
pointwise ordering: f <= g if for every w. f w implies g w.

This is a Heyting Algebra:

top w iff true
(f /\ g) w iff f w and g w
bot w iff false
(f \/ g) w iff f w or g w
(f => g) w iff for any v <= w. if f w then g w

Then an interpretation of the propositional variables in this HA would
be an assignment for each variable X and w a proposition [x] w that is
antitone in w: if [x] w and v <= w then [x] v. Then the model HA
interpretation defines exactly our Kripke forcing semantics. It
defines for each proposition of IPL p a function from W to Prop that
is antitone, i.e., [p] : W^op -> Prop. Then the definition of Kripke
model is just an infix notation for this semantics:

w ||- p := [p] w

And if you unravel the definitions of the HA semantics and the HA
structure of the poset, you reproduce exactly the definition of a
Kripke model.

Bonus: this is all a "de-categorification" of a similar situation for
lambda calculus. The Kripke models are presheaf categories and the HA
are bi-cartesian closed categories.

Every Virtual Learning Environment expands until it has a bug ridden unusable half implemented spreadsheet for incorrectly computing final marks.

I should've gone to Boston, Lincolnshire. Would've been substantially cheaper and I wouldn't be jetlagged.

“Compiling higher-order specifications to SMT solvers” slides and link paper: bentnib.org/posts/2023-01-17-h

A last-minute-COVID-forced remote talk about type based analyses for checking and translating higher-order specifications to SMT solvers.

My CPP talk is coming up next. Really wish I was giving it in person.

Urrgh. At POPL with a positive COVID test. Stuck in my room!

And this is the view out of my window:

Catala is a programming language for the law. It has a feature for making definitions with defaults and overrides. I think the description in the Catala ICFP paper hides how elegant and simple this is.

A simple semantics for defaults in Catala: bentnib.org/posts/2023-01-16-c

Data types with Negation -- some slides from a talk about how to understand data type definitions that include negation.

The talks were a while ago, but I never put the slides online anywhere.

bentnib.org/posts/2023-01-15-d

Bob Atkey boosted

By the way, js_of_ocaml 5.0 has been released with (opt-in) support for effect handlers 🙂 discuss.ocaml.org/t/ann-js-of-

js_of_ocaml is a compiler from OCaml to Javascript. It allows to do a number of cool things such as the OCaml Playground ocaml.org/play or Learn OCaml ocaml-sf.org/learn-ocaml-publi

All credit where credit is due, the effect support in js_of_ocaml uses a CPS transform adapted from the one proposed by Daniel Hillerström, @reifyreflect, @bentnib and @kayceesrk
in “Continuation Passing Style for Effect Handlers” and “Effect handlers via generalised continuations”!

Bob Atkey boosted

Can't wait to be back in Paris this late April thanks to my upcoming ESOP paper: 'Builtin Types viewed as Inductive Families' gallais.github.io/pdf/esop23-t

Bob Atkey boosted

Category Theory, Presheaves, Long Explanation 

The usual definition of a presheaf P on a category C is a functor C^op -> Set. But here is a more conceptual way to think about it. (For the experts, basically it’s the same idea as a monoid/group action).

First, a category is a notion of object and morphism between objects. These morphisms can be composed if the source of one matches the target of the other. I.e., they can be composed “tip to tail”. You need identity morphisms for this composition and the composition is associative. This all justifies notation like drawing morphisms by concatenating arrows without using parentheses (picture 1). Or writing a composition as `f;g;h` or even `hgf` with just concatenation.

One way to think about a presheaf P on a category C is that it extends the notion of morphism. We had morphisms with a source and target, and the presheaf defines a new notion: a morphism that has a source but no target. What kind of composition should such a thing have? Well if I have a morphism f with domain A and codomain B and I have a morphism phi with domain B but no codomain, then I should still be able to compose them together to get a morphism with domain A and no codomain. That is, we can compose these “morphisms to nowhere” with ordinary morphisms on one side but not the other (since there is no codomain object to tell us what kind of morphisms we can compose with). This kind of composition should intuitively extend the existing notion: composing an arrow with no codomain with the identity (id; phi = phi) shouldn’t change it and there should be an Associativity when combining with ordinary composition (f;g);phi = f;(g;phi). These rules make it so that we can cleanly extend our original notation for composition to these new morphisms (picture 2). It is a very useful exercise to figure out why this data is precisely the same as a functor from C^op to Set.

A few observations:
1. This all would work perfectly fine with arrows that only have a codomain and no domain. These are “copresheaves” and are equivalent to functors C to Set.
2. For any object A of C, we could define a presheaf by defining an arrow with no codomain to be an arrow into A! Then this satisfies the right identity and Associativity rules because it is just ordinary composition. This construction turning an object of a category into a presheaf on it is the Yoneda embedding!
3. Once we have seen (2) we should ask for any presheaf: Is this notion of morphisms with no codomain really just the same as morphisms into some fixed object? If it is, then we call it a *representable* presheaf.

The concept of a representable presheaf is, in my opinion, the most important idea of category theory. It deserves more in another post but here’s just one example that I learned from Emily Riehl’s textbook (Category Theory in Context) to tie everything together. Take the category of (undirected) graphs and graph homomorphisms. A K-coloring of a graph is an assignment of a number [1,…K] for each vertex of a graph such that if two vertices are connected by an edge, they have to be assigned different colors. The concept of a K-coloring turns out to be a presheaf. We can think of a K-coloring of a graph G as a morphism chi with domain G but no codomain. If I have a graph homomorphism f from H to G, then I can compose the coloring chi with f to get a coloring f;chi on H (since homomorphisms preserve adjacency) and this satisfies the correct identity and associativity rules. Once we realize this we should ask: is this notion representable? I.e., is there a special graph Q(K) such that a K-coloring on G is the same thing as a homomorphism from G to Q(K)? I’ll post the answer in a reply.

Bob Atkey boosted

First they came for the journalists, who were very surprised to find themselves in a giant warehouse filled with minorities, immigrants, disabled, trans, and gay people.

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.