Zulip Chat Archive

Stream: general

Topic: Computational category theory


view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:15):

@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).

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:18):

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?

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:19):

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.

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:20):

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

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:21):

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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:21):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:22):

I thought F# had dependent types?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:23):

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.

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:24):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:24):

@Mario Carneiro that is F* not F#

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:24):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:26):

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'

view this post on Zulip Notification Bot (Feb 02 2021 at 05:28):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:29):

Oops, this got the whole past of the thread too

view this post on Zulip Huỳnh Trần Khanh (Feb 02 2021 at 05:30):

Oh dear. How can we fix this?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:32):

Eh, close enough

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:34):

@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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:37):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:41):

@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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:42):

yeah that sounds doable

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 05:42):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:44):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 05:45):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:29):

@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.

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:43):

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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:46):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:48):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:49):

@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?

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:49):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:50):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:51):

i see--thanks!

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:51):

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)

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:52):

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?

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:53):

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

view this post on Zulip Mario Carneiro (Feb 02 2021 at 07:53):

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

view this post on Zulip Nasos Evangelou-Oost (Feb 02 2021 at 07:54):

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

view this post on Zulip Kyle Miller (Feb 02 2021 at 07:55):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 02 2021 at 16:17):

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


Last updated: May 14 2021 at 22:15 UTC