joey

joey, 16 days ago to random

Anyone have recommendations for a good ergonomic keyboard? My old Microsoft 4000 is wearing out

counting_is_hard, 19 days ago to random

In his famous paper, "on proof and progress in mathematics", Thurston lists 8 (and implies 29 other) ways to think of the derivative.

I was bored waiting for a bus, so I tried listing the different ways I could think of what a category is (see below). Please feel free to help me add more!

A Category is...

1. The usual definition (omitted for space)
2. an abstract theory of functions / arrows (or as Awodey would say "archery")
3. a monoidoid
4. a poset with evidence (wording stolen from Alex Kavvos)
5. a set-enriched category
6. an object in CAT
7. a syntax for a programming language
8. a maze of twisted arrows all alike
9. a "path-complete" digraph (if there is a path x -> y there is an edge x -> y)
10. a multicategory where every arrow has arity 1
11. a polynomial comonad (spivak et al)

#categorytheory

joey, 24 days ago to random

Does anyone have thoughts on how to make a presheaf model of type theory with a universe hierarchy in Lean?

Basically I'm running into size issues since I don't have induction-recursion or Type-ω.

I can just parametrize the syntax over n for how many levels you're allowed to use and use (Type n+1) in the model, but this is unsatisfying.

Is there something I can postulate to get the equivalent of ω inaccessible cardinals? Or can I hack Impredicative Prop somehow?

joey, 1 month ago to random

I will say about using Lean, it has the best blending of direct and tactic-style dependent types that I've tseen, it's just really smooth to switch between them.

And you don't need that many complicated tactics, it's mostly just induction, simp, constructor, apply.

I think the experience could be recreated in Agda if rewrite rules worked better with typeclasses/records and there was a little more polish on the existing tactic libraries like Ataca.

I'll also say, it's just so damn easy not having to worry about equalities of equalities. Definitional Prop and treating iff as equality are just really nice. I'm sure there's some stuff that doesn't formalize well that way but I haven't found it yet.

joey, 1 month ago to random

Alright. What's so fundamental about the fundamental theorem of topos theory?

I guess it gives us the pullback functor, whose adjoints are the dependent product and sum.

But is there more? Why is it so important to get that name?

joey, 1 month ago to random

So, you can encode the category Fam as the arrow category of Set. The family of sets ( { B_a}_{a\in A} ) becomes the arrow π₁:(Σ(𝑥:𝐴).𝐵𝑥)→𝐴 , i.e. the family $B_a$ is the set of index-element pairs whose index is a.

If you introduce universe levels, and want A : Set u and B : A → Set v, this trick doesn't work, because the Sigma type has size (max u v), not v.

Is there a way to get around this that works nicely with universe levels?

joey, 2 months ago to random

In the CwF instance for a presheaf category, contexts are in Psh(C), and types over Γ are in Psh(el(Γ)). You define context extension as (Γ.A)(k) := Σ(g :Γ(k)).A(k,g) in Psh(C)

Question: is there a way to define this more abstractly? Like with the dependent sum or something?

Basically, I'm trying to convince Lean that (Γ.A) is actually a presheaf, and the dependent equalities are kicking my butt, despite the proof being trivial on paper.

But if there's a way to express this using known operations that are guaranteed to produce presheaves as output, then this might be easier

joey, 4 months ago to random

Preparing CPP slides like

joey, 4 months ago to random

Alright everyone, what are your favorite books for an undergrad PL class? Class I'm teaching in the summer is currently using Sebesta, but I'd like to shake it up.

Currently on my radar are:

• PLAI version 3 by @shriramk, which is what I'm currently leaning to
• Essentials of Programming Languages

Are there any in the style of PLAI/EOPL (implementation instead of paradigms) that are Haskell/ML based? e.g. books about writing interpreters in Haskell?

joey, 4 months ago to random

PL Grad student recruiting, boosts welcome

I am a newly-hired Assistant Professor, recruiting Masters and Doctoral students to research programming languages theory with me at the University of Regina in Canada. Specific areas of interest include:

• Programming with dependently typed languages, like Lean, Agda, Idris, and Coq
• Improving usability of dependently typed programming languages
• Gradual types and gradual dependent types
• Live programming environments for dependent types
• Static analysis of dependently typed programs
• Ordinal notations and termination proofs
• Error messages and repair suggestions for static and dynamic type errors
• Dependent pattern matching - semantics and implementation

Graduate students at the U of R have the opportunity to be part of a small, focused research group where you can work closely with your advisor. Regina is one of Canada’s most affordable cities to live in, and students have access to Canada’s universal health care. Students are funded by stipend, and have the opportunity to gain experience as a Teaching Assistant or Sessional Lecturer.

Application deadlines are listed below, but out-of-cycle applications are possible for strong students.

• Feb 15 2024 (to begin September 2024)
• June 15 2024 (to begin January 2025)
• October 15 2024 (to begin May 2025)

For more information on applying, visit https://www.uregina.ca/science/cs/graduate/future-grad/index.html. Any questions for me specifically can be directed to jeremondi@uregina.ca.

joey, 5 months ago to random

I think Pearson must be pretty closet to the highest "quality of person vs quality of airport named after person" ratio

BartoszMilewski, 6 months ago to random

I'm struggling with one particular aspect of Idris. I can define a vector of size 1 like this:
v : Vect 1 Nat
v = [42]
It would seem natural that I should be able to abstract the count 1 into a variable, like this:
n : Nat
n = 1
v : Vect n Nat
v = [42]
This is, however, not correct, and the explanation I was given (it's all a word of mouth in Idris) is very confusing.
Oddly, the way to do it is to use upper case N:
N : Nat
N = 1
v : Vect N Nat
v = [42]
I have a feeling that some deep law of language design was violated.

joey, 6 months ago to random

Is there a for-dummies intro to how the left and right adjoints of the base change functor model dependent products and sums?

I've seen may things say that they are but nothing yet has said how they are.

joey, 7 months ago to random

Is there an adjunction-version of a Galois insertion? Where the counit is a natural isomorphism, but the unit isn't necessarily?

ZachWeinersmith, 7 months ago to random

What food do you think has the most intermediate production stages where it is recognizably some other food (not just an ingredient). For example, processed cheese:

1. Milk
2. Fresh cheese
3. Aged cheese
4. Emulsified cheese

ZachWeinersmith, 7 months ago to random

Where do you draw the line between AI you like and dislike? My sense is there's a serious disdain for e.g. generative art or text, but not for other machine-learning stuff, like plant ID apps or speech to text software.

ZachWeinersmith, 7 months ago to random

Hey mathstodon, help me understand something. What does Hilbert mean when he argues that to prove the existence of a mathematical concept, you only have to prove that if it existed you arrive at no contradiction.

joey, 7 months ago to random

joey, 8 months ago to random

Anyone have a good unicode alternative to \bigvee? Agda uses ⋁ which, in a monospace font, is almost indistinguishable from ∨.

grimalkina, 8 months ago to random

Something I'm curious about rn is how departments that work WITH eng but aren't classified in engineering are being barred from tools like Copilot. We saw this lag with data science and I bet there are swaths of people whose careers will be impacted by this now. Much of the time when I talk to software engineers at large companies they are shocked to learn scientists often have to fight company policy to use the same tools that we might often need. Not something "devex" seems to care about lol

johncarlosbaez, 1 year ago (edited 1 year ago) to random

In computer science it's against the rules to publish your work in many prestigious venues unless you physically travel to present that work at a conference!

They seem to be forgetting that there's a thing called the "internet" that makes this unnecessary. Pretty weird for computer scientists.

Here's the famous computer scientist Moshe Vardi on how this needs to change:

"As I argued in January 2020, in view of the worsening climate crisis, our discipline's practice that every publication requires travel, often trans-oceanic, is inconsistent with the public good. A report released in March 2023 by the Intergovernmental Panel on Climate Change paints an even bleaker picture of the worsening climate crisis. The world is on brink of catastrophic warming, the report warned. A dangerous climate threshold is near, but 'it does not mean we are doomed' if swift action is taken, the scientists said."

"Going back to the pre-pandemic conference-travel culture is simply not morally acceptable, I believe. Yet many conferences have gone back to a full in-person model, and authors are required to present in person. This requirement is drawing criticism. A recent article by Theoretical Computer Scientists for Future (TCS4F) concluded, 'Coupling formal publications with an in-person gathering no longer makes sense for everyone.'"

https://cacm.acm.org/magazines/2023/5/272297-acm-for-the-public-good/fulltext