Computational category theory

Stream: general

[Nasos Evangelou-Oost]

@Huỳnh Trần Khanh i see. actually what i'm more interested is in computational category theory and general purpose programming. i recently was surprised to learn that lean4 is actually quite capable of this. i'm currently working on a project in F# but the lack of dependent types is limiting. i also considered idris2 as a general-purpose dependently typed language but it is in prerelease and its development seems slow (idris 1 seems too slow to be able to do anything useful).

[Nasos Evangelou-Oost]

on the official Lean about page (https://leanprover.github.io/about/) it says "Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover." it sounds like Lean is being marketed here as a programming language first and a theorem prover second. Is this a change of direction in lean4? or is lean3 also capable of general purpose programming?

[Huỳnh Trần Khanh]

I wouldn't say that this is a change of direction in Lean 4. Lean has been exploiting the Curry–Howard correspondence since its inception and I think this is just a natural evolution of the idea perhaps.

[Huỳnh Trần Khanh]

And no, Lean 3 is not capable of general purpose programming. But you can still write programs in Lean 3.

[Huỳnh Trần Khanh]

Nasos Evangelou-Oost said:

Huỳnh Trần Khanh i see. actually what i'm more interested is in computational category theory and general purpose programming. i recently was surprised to learn that lean4 is actually quite capable of this. i'm currently working on a project in F# but the lack of dependent types is limiting. i also considered idris2 as a general-purpose dependently typed language but it is in prerelease and its development seems slow (idris 1 seems too slow to be able to do anything useful).

Have you tried Dafny? Does it fit your use case?

[Mario Carneiro]

Lean 3 can be used as a general purpose programming language, it's just not very good

[Mario Carneiro]

I thought F# had dependent types?

[Mario Carneiro]

https://www.fstar-lang.org/#introduction

F*'s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.

[Nasos Evangelou-Oost]

funny you ask... i am about to TA for a class that uses Dafny. but I have never actually used it before, so I'm not sure. to give you an idea of what i'm interested in, here is the project i am working on in F#: https://github.com/nasosev/topos-tool . my goal is to use it as a calulator for small presheaf toposes

[Nasos Evangelou-Oost]

@Mario Carneiro that is F* not F#

[Mario Carneiro]

oh right, F# is just C# with different syntax

[Nasos Evangelou-Oost]

eh, i guess. i use it because it is an ML with good cross-platform support and it works in jupyter notebooks, so works well as a 'calculator'

[Notification Bot]

This topic was moved here from #lean4 > mathlib by Mario Carneiro

[Mario Carneiro]

Oops, this got the whole past of the thread too

[Huỳnh Trần Khanh]

Oh dear. How can we fix this?

[Mario Carneiro]

Eh, close enough

[Mario Carneiro]

@Nasos Evangelou-Oost From a cursory look at the project, it seems like you are looking at finite categories represented by finite sets of objects and morphisms?

[Mario Carneiro]

How large are the categories and presheaves you are building? It might be possible to do this in lean 3 if the numbers are small enough

[Nasos Evangelou-Oost]

@Mario Carneiro yes, everything is finite and the base categories are very small, and i am looking at 'presheaves' on them that take objects to homogeneous sets Set<'A> and morphisms to set functions, represented as maps Map<'A,'A> (so that they can be collected into sets themselves and compared for equality). as a simple example (see https://github.com/nasosev/topos-tool/blob/master/nb/graphs.ipynb) is the category G with two objects and two morphisms between them, and presheaves on G are directed graphs

[Mario Carneiro]

yeah that sounds doable

[Nasos Evangelou-Oost]

i think essentially i am limited to very small things as the constructions involved tend to be exponential in complexity

[Mario Carneiro]

it's a bit different from the definitions in category_theory, where the objects are a whole type rather than a finite subset of that type

[Mario Carneiro]

you can build a type out of a finite set though, so you can still relate your definitions to those in the category theory library

[Mario Carneiro]

@Nasos Evangelou-Oost Here's a prototype of the first example in your notebook, using the Category.make function:

import data.list.alist

namespace alist

def modify_or_insert {α} [decidable_eq α] {β : α → Type*} (a : α) (z : β a)
  (f : β a → β a) (l : alist β) : alist β :=
l.insert a $ f $ (l.lookup a).get_or_else z

end alist

namespace list

def to_alist' {α} [decidable_eq α] {β : α → Type*} (l : list α) (f : ∀ x, β x) : alist β :=
let s := l.erase_dup in
⟨s.map $ λ x, (⟨x, f x⟩ : sigma β),
  by simp [list.nodupkeys, list.keys]; convert l.nodup_erase_dup; rw [map_id']; simp⟩

instance {α} {β : α → Type*} [has_to_string α] [∀ a, has_to_string (β a)] :
  has_to_string (alist β) := ⟨to_string ∘ alist.entries⟩

end list

namespace fincat

@[derive decidable_eq]
structure arrow (α : Type*) := (dom : α) (cod : α) (name : string)

instance {α} : has_to_string (arrow α) := ⟨arrow.name⟩

def arrow.id {α} [has_to_string α] (a : α) : arrow α := ⟨a, a, "1_" ++ to_string a⟩

structure fincat (α : Type*) :=
(name : string)
(ob : list α)
(nonid_arrows : list (arrow α))
(arrows : list (arrow α))
(id : alist (λ _:α, arrow α))
(hom : alist (λ _:α, alist (λ _:α, list (arrow α))))
(compose : alist (λ _:arrow α, alist (λ _:arrow α, arrow α)))

def fincat.make {α} [has_to_string α] [decidable_eq α]
  (name : string) (ob : list α)
  (nonid_arrows : list (arrow α))
  (nontriv_compose : alist (λ _:arrow α, alist (λ _:arrow α, arrow α))) :
  option (fincat α) :=
let compose : list (arrow α × arrow α × arrow α) :=
  (ob.map $ λ A, let I := arrow.id A in (I, I, I)) ++
  (nonid_arrows.map $ λ a, (a, arrow.id a.dom, a)) ++
  (nonid_arrows.map $ λ a, (arrow.id a.cod, a, a)) ++
  (do
    a ← nonid_arrows,
    b ← nonid_arrows,
    guard (b.cod = a.dom ∧ a.cod = b.dom ∧
      ((nontriv_compose.lookup a).bind (λ v, v.lookup b)).is_none),
    pure (a, b, arrow.id b.dom)) in
let hom : alist (λ _:α, alist (λ _:α, list (arrow α))) :=
  ob.to_alist' $ λ A, ob.to_alist' $ λ B,
    (do
      (a, b, c) ← compose,
      guard (b = arrow.id A),
      pure c) ∩
    (do
      (a, b, c) ← compose,
      guard (a = arrow.id B),
      pure c) in
let compose : alist (λ _:arrow α, alist (λ _:arrow α, arrow α)) :=
  compose.foldl (λ l ⟨a, b, c⟩, l.modify_or_insert a ∅ $ alist.insert b c) ∅ in
let arrows := do ⟨_, l⟩ ← hom.1, ⟨_, l⟩ ← l.1, l in
guard (
  ∀ a ∈ arrows,
  ∀ b ∈ arrows,
  arrow.cod b = arrow.dom a →
  ((compose.lookup a).bind (λ v, v.lookup b)).is_some
) >>
some {
  name := name,
  ob := ob,
  id :=  ob.to_alist' arrow.id,
  arrows := arrows,
  nonid_arrows := nonid_arrows,
  hom := hom,
  compose := compose }

end fincat

open fincat

@[derive decidable_eq]
inductive Graph | V | E

instance : has_to_string Graph := ⟨λ x, Graph.rec "V" "E" x⟩

open Graph
#eval show tactic unit, from do
  let objects := [V, E],
  let arrows := [arrow.mk V E "s", arrow.mk V E "t"],
  cat ← fincat.make "Graphs" objects arrows ∅,
  tactic.trace $ "name: " ++ cat.name,
  tactic.trace $ "objects: " ++ to_string cat.ob,
  tactic.trace $ "nonid_arrows: " ++ to_string cat.nonid_arrows,
  tactic.trace $ "hom: " ++ to_string cat.hom,
  tactic.trace $ "compose: " ++ to_string cat.compose,
  pure ()

-- name: Graphs
-- objects: [V, E]
-- nonid_arrows: [s, t]
-- hom: [⟨V, [⟨V, [1_V]⟩, ⟨E, [s, t]⟩]⟩, ⟨E, [⟨V, []⟩, ⟨E, [1_E]⟩]⟩]
-- compose: [⟨1_E, [⟨t, t⟩, ⟨s, s⟩, ⟨1_E, 1_E⟩]⟩, ⟨t, [⟨1_V, t⟩]⟩, ⟨s, [⟨1_V, s⟩]⟩, ⟨1_V, [⟨1_V, 1_V⟩]⟩]

This sort of thing will get a lot easier in lean 4 though.

[Nasos Evangelou-Oost]

thank you very much @Mario Carneiro ! this will give me a great head start.

are you using mathlib here by the way? and what in particular should be easier in lean 4?

[Mario Carneiro]

Yes, it's using data.list.alist from mathlib. This is more or less straight programming, which has better support (and much more efficient too, meaning you can go to bigger examples) in lean 4, as well as nicer syntax for this use case. The code above has been written such that you could in principle prove the equivalence to category_theory categories, but that's a fairly nontrivial theorem because of all the programming stuff

[Mario Carneiro]

I originally started writing this with finset and finmap, but those types are explicitly order-erased, which means there are proof obligations in the operations to prove that the order you collect things doesn't matter. It can be done but it would take some more hours to figure out

[Nasos Evangelou-Oost]

@Mario Carneiro I see. If i don't need to show equivalence mathlib definitions or do any proofs ofr the time being, maybe I could just start right away with lean 4, using its List type?

[Nasos Evangelou-Oost]

ah yes, i was worried about that when looking up finset earlier in the mathlib docs

[Mario Carneiro]

Yes, I think that would work. There might also be more efficient set/map data structures in lean 4; I'm using lists here for simplicity but that performs pretty poorly

[Nasos Evangelou-Oost]

i see--thanks!

[Mario Carneiro]

alist B is really just list (sigma B) with a proof that the list has nodup keys; if you maintain that property yourself without doing proofs then you can just use list (sigma B) (or list (A x B) in your case since the dependent types aren't necessary)

[Nasos Evangelou-Oost]

oh, and once the library is built, how would you suggest is the best way to use/interact with i?t-- i imagine Lean does not yet support a notebook interface like Jupyter. But does it have a REPL?

[Mario Carneiro]

@Bryan Gin-ge Chen has a set up for running lean 3 in an Observable notebook somewhere

[Mario Carneiro]

No REPL but it does have a web version, for example https://leanprover-community.github.io/lean-web-editor/

[Nasos Evangelou-Oost]

oh, nice! it looks like one can load external files in there, so that should be enough

[Kyle Miller]

Nasos Evangelou-Oost said:

But does it have a REPL?

In a certain sense the source files themselves are a REPL using commands like #eval

[Bryan Gin-ge Chen]

Mario Carneiro said:

Bryan Gin-ge Chen has a set up for running lean 3 in an Observable notebook somewhere

Here's a link to a collection containing my Lean notebooks: https://observablehq.com/collection/@bryangingechen/lean