Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: dependent types

sarahzrf (Apr 04 2020 at 20:17):

@Jules Hedges i'm gonna reply to this here https://twitter.com/_julesh_/status/1246528993903497222

@sarah_zrf A bit... at least I read a bunch of Jacobs' book and I'm generally intimidated and confused by the whole thing, but I know at least some of the basics

- julesh (@_julesh_)

sarahzrf (Apr 04 2020 at 20:23):

basically the idea is like

sarahzrf (Apr 04 2020 at 20:25):

if you're interpreting your type theory in a category $\mathcal{C}$, and you have a typing judgment $\vdash A\ \mathsf{type}$, then you should of course have an object $\llbracket A \rrbracket \in \mathcal{C}$ to act as its semantics

sarahzrf (Apr 04 2020 at 20:27):

but say you have a judgment $x : A \vdash B\ \mathsf{type}$, and your language is dependently typed, so that $x$ may well appear free in $B$—we don't just want an object of $\mathcal{C}$

sarahzrf (Apr 04 2020 at 20:27):

rather, the semantics of $B$ should be a family of objects of $\mathcal{C}$, parameterized by $\llbracket A \rrbracket$

sarahzrf (Apr 04 2020 at 20:27):

that's an object of the slice category $\mathcal{C} / \llbracket A \rrbracket$!

Stelios Tsampas (Apr 04 2020 at 20:30):

sarahzrf said:

Jules Hedges i'm gonna reply to this here https://twitter.com/_julesh_/status/1246528993903497222

What's the context on this? I'm a big Bart Jacobs fan myself!

sarahzrf (Apr 04 2020 at 20:34):

click thru & see

sarahzrf (Apr 04 2020 at 20:36):

anyway tho, in general if we have a context $\Gamma$, that determines an object in some category, and then $\Gamma \vdash A\ \mathsf{type}$ determines an object in the slice category over $\llbracket \Gamma \rrbracket$

sarahzrf (Apr 04 2020 at 20:37):

and then if you write a term $\Gamma \vdash e : A$, that gives a global element of $\llbracket A \rrbracket$

sarahzrf (Apr 04 2020 at 20:37):

so, something that i was tweeting about the other day with like 4am brain and which finally clicked for me was like...

Stelios Tsampas (Apr 04 2020 at 20:37):

sarahzrf said:

click thru & see

I tried but the thread is not visible in either profile :/.

sarahzrf (Apr 04 2020 at 20:38):

you should be able to click the twitter link itself, not our @

sarahzrf (Apr 04 2020 at 20:38):

but i can screenshot it if you want, one sec

sarahzrf (Apr 04 2020 at 20:39):

image.png

Jules Hedges (Apr 04 2020 at 20:39):

I still think we're talking at cross purposes..... the idea behind what I originally said is that the syntax of languages ought to reflect the categorical semantics

Jules Hedges (Apr 04 2020 at 20:40):

Inspired by mixed linear-nonlinear logic, really

sarahzrf (Apr 04 2020 at 20:40):

and im claiming that it does :>

sarahzrf (Apr 04 2020 at 20:40):

in this case

Jules Hedges (Apr 04 2020 at 20:40):

Hm, I don't see that

sarahzrf (Apr 04 2020 at 20:40):

it was a bit tongue in cheek, but i actually kinda like this viewpoint

sarahzrf (Apr 04 2020 at 20:40):

lemme continue

sarahzrf (Apr 04 2020 at 20:41):

if you have $\Gamma \vdash x : A$—i.e., $x$ is a variable of $\Gamma$—then that's still a global element in a slice category

sarahzrf (Apr 04 2020 at 20:42):

a slice category over $\llbracket \Gamma \rrbracket$ is the category where there is a global parameter of $\llbracket \Gamma \rrbracket$

Stelios Tsampas (Apr 04 2020 at 20:42):

Jules Hedges said:

I still think we're talking at cross purposes..... the idea behind what I originally said is that the syntax of languages ought to reflect the categorical semantics

What exactly do you mean by "reflect"?

sarahzrf (Apr 04 2020 at 20:43):

so $x$'s categorical semantics is "one of the components of the global parameter"

sarahzrf (Apr 04 2020 at 20:44):

i contend, at least semiseriously and for the purpose of this conversation, that having free variables at all is a syntax that reflects working in a slice category!

Jules Hedges (Apr 04 2020 at 20:44):

Ok, I can buy that

sarahzrf (Apr 04 2020 at 20:44):

whenever you add a free variable, you move up a slice, or at least base change

sarahzrf (Apr 04 2020 at 20:45):

and whenever you bind a variable, you're applying an adjunction

sarahzrf (Apr 04 2020 at 20:45):

$\sum \dashv \Delta \dashv \prod$

Jules Hedges (Apr 04 2020 at 20:46):

Then I need to refine what I said a bit. We have lexical scoping (??) for slice categories, and then another example is how do-notation drops you into the internal syntax of a kleisli category.... but my crazy idea is that all these things should be programmer-definable instead of having a fixed-for-all-time collection of adjunctions provided by the language

sarahzrf (Apr 04 2020 at 20:47):

yeah that would be sick as hell

sarahzrf (Apr 04 2020 at 20:47):

but i just mean like

sarahzrf (Apr 04 2020 at 20:47):

the story behind that tweet was basically just

Jules Hedges (Apr 04 2020 at 20:47):

Another example that was really the motivating one is the language based on call by push value, where you have a strict language and a lazy language and operators that go between them

Jules Hedges (Apr 04 2020 at 20:48):

One of my zen principles is that if you make your language strict you went wrong, and if you make it lazy you went wrong, the only true path is to put them on exactly equal footing with neither preferred

sarahzrf (Apr 04 2020 at 20:49):

i had a shower thought like "hmm... modalities are [co]monads b/c youre, like, really talking about something in another category thru the lens of this one, so ur moving thru an adjunction... what if u had a type constructor that really was an adjoint instead of a monad... wait a second, didnt jules tweet something like that before... wait a second, $\sum \dashv \Delta \dashv \prod$... lmao im gonna tweet this"

Dan Doel (Apr 04 2020 at 20:49):

All the things I've seen that do that have a lot of extra boilerplate.

Jules Hedges (Apr 04 2020 at 20:50):

Ah, I get it

Jules Hedges (Apr 04 2020 at 20:51):

And yeah. I guess nobody knows how to make it work, otherwise someone would have done it already

Dan Doel (Apr 04 2020 at 20:51):

By the way, have you read Compiling with Classical Connectives?

sarahzrf (Apr 04 2020 at 20:51):

nope, whats it about

Dan Doel (Apr 04 2020 at 20:52):

I don't know CBPV very well, but CwCC seems like it's probably that on steroids.

Dan Doel (Apr 04 2020 at 20:52):

It kind of has a bunch of somewhat different ideas crammed into one paper, but they're all cool.

sarahzrf (Apr 04 2020 at 20:53):

CwCC looks like an emoticon

Jules Hedges (Apr 04 2020 at 20:53):

The thing that really started me on that train of thought was linear-nonlinear logic. So you start with linear logic, where the ! modality looks like a comonad. Then in the categorical semantics it really is a comonad, but after a lot of work in the 90s everyone agreed that the "right" categorical semantics of linear logic is a "linear-nonlinear adjunction" between a *-autonomous category and a cartesian category, where ! gets decomposed. And then Benton invented linear-nonlinear logic, which is a syntactic reformulation of linear logic that directly reflects the categorical semantics

sarahzrf (Apr 04 2020 at 20:53):

waittttt i thought the "right" categorical semantics was a comonad :cold_sweat:

sarahzrf (Apr 04 2020 at 20:54):

"seely comonad" or sth

sarahzrf (Apr 04 2020 at 20:54):

i havent looked into categorical semantics of linear logic much

Jules Hedges (Apr 04 2020 at 20:55):

I kinda cut my teeth in category theory reading "categorical semantics of linear logic" by Melliès, so I always take his word on this

Dan Doel (Apr 04 2020 at 20:55):

Anyhow, one of the things in CwCC is a type theory that's like sequent calculus, with multiple consequents. It has all the linear connectives, but I think the sequents are not linear.

Dan Doel (Apr 04 2020 at 20:56):

Instead the connectives are distinguished by their inherent polarity, which maps to an evaluation strategy that makes the reduction deterministic, and you can shift between them.

Jules Hedges (Apr 04 2020 at 20:57):

I don't think I read that paper, but I love this stuff.... if I wasn't doing game theory I'd like to be a French logician

sarahzrf (Apr 04 2020 at 20:57):

be a french PL theorist instead

Dan Doel (Apr 04 2020 at 20:57):

So $+$ is a positive connective whose values are a choice of two positive values, and $⅋$ is a negative connective whose covalues are pairs of two negative covalues.

sarahzrf (Apr 04 2020 at 20:57):

well, is there a difference

Jules Hedges (Apr 04 2020 at 20:58):

French programming languages = French logic + naming things to make English speakers uncomfortable

sarahzrf (Apr 04 2020 at 20:58):

have you seen abramsky's $\mathrm{PE}_2$?

Dan Doel (Apr 04 2020 at 20:59):

Positive values are built out of constructors, and negative covalues are built out of projections. Negative values are built by copattern matching and positive covalues are built by pattern matching.

sarahzrf (Apr 04 2020 at 20:59):

its what im most familiar with, given that ive been working with it for my degree project

Dan Doel (Apr 04 2020 at 20:59):

But, it also has semantics for call-by-need, and call-by-coneed. The latter avoids duplicate work when capturing continuations.

sarahzrf (Apr 04 2020 at 21:00):

hmmmm that sounds like the dual calculus :thinking:

Dan Doel (Apr 04 2020 at 21:01):

Then in a later section it also shows how to have arbitrary (co)data definitions whose constructors/projections are specified by sequents.

Dan Doel (Apr 04 2020 at 21:01):

And how to compile it back to the linear logic set of connectives.

Jules Hedges (Apr 04 2020 at 21:01):

Ok, I'd like to know what "coneed" is, but I'd like to go to bed even more

sarahzrf (Apr 04 2020 at 21:01):

imagine going to bed at only 10pm

sarahzrf (Apr 04 2020 at 21:02):

when there is PL to be done

Jules Hedges (Apr 04 2020 at 21:03):

I'm normally more of a night person, but I'm living with my dad who is a morning person with far more determination than me. And also I don't have enough enthusiasm to work on weekends

sarahzrf (Apr 04 2020 at 21:04):

the week is a principal homogeneous space for the action of $\mathbb{Z}_7$

sarahzrf (Apr 04 2020 at 21:07):

at least, when i'm at home and lying in bed all day :disappointed:

Nathanael Arkor (Apr 04 2020 at 21:08):

do-notation drops you into the internal syntax of a kleisli category.... but my crazy idea is that all these things should be programmer-definable

isn't this the idea behind embedded domain specific languages?

Nathanael Arkor (Apr 04 2020 at 21:08):

Racket is particularly big on this

Andre Knispel (Apr 04 2020 at 23:19):

I have a couple of cool demos that might be relevant to this discussion, I'll probably show them soon-ish. Just have to do a bit more polish first...

Avi Craimer (Sep 15 2020 at 13:57):

I've been trying to wrap my head around Sigma and Pi types for a while now. I find that the hardest part is understanding how the type level and value level interact in a kind of zigzagging way. I finally think I understand, and I drew this diagram to try to make it clear what is going on. Would be happy to hear if I'm on the right track.

https://drive.google.com/file/d/19qfBnTk0e7AxMBCGGi9QEZ_ZXjAPpQ80/view?usp=drivesdk

Dan Doel (Sep 15 2020 at 14:28):

That looks right.