Show older

re: OPLSS thread 

I still can't sleep properly and I feel like I'm racking up a sleep debt that will get me in week 2

re: OPLSS thread 

Every time I see "NilF" — you know, the empty constructor for the functor whose fixpoint generates lists — I read it like "dilf" in my head

re: OPLSS thread 

Nullary list I'd like to functor

re: OPLSS thread 

Debating whether this one is going on Twitter

re: OPLSS thread 

I need a lil screenshot for context... and I think it'll work

re: OPLSS thread 

Hmm usual type theory is a mix of natural deduction and sequent calculus
Does it have a name

re: OPLSS thread 

First positive covid of the summer school... it was a lecturer 😳

re: OPLSS thread 

"Agda checks that I only do reasonable recursion" size-preserving recursion is reasonable 😤

re: OPLSS thread 

ordinals ❤️

re: OPLSS thread 

ngl despite knowing formally how guardedness for coinductive types works it's rather challenging to actually define functions for them lol

re: OPLSS thread 

paramorphisms are ezpz, it's just a cata with extra

re: OPLSS thread 

...in Haskell. I fear what this will look like in the diagrams

re: OPLSS thread 

You lost me at histomorphisms

re: OPLSS thread 

I don't like zygomorphisms
para and mutu are fine

re: OPLSS thread 

I've figured out the universal property for para and mutu but I don't see it for zygo

re: OPLSS thread 

mutu phi psi . in = (fork phi psi) . fmap (mutu phi psi)
Isn't that lovely

re: OPLSS thread 

Idk if that's a universal property. It's an equation alright

re: OPLSS thread 

Two ppl I just met, immediately after shaking hands: "I guess we shouldn't be doing that"

re: OPLSS thread 

What do I do now. I wanted to draw out mutumorphisms but what after...

re: OPLSS thread 

Perhaps I shall get a souvenir

re: OPLSS thread 

Nope itchy itchy. Back to the dorms it is

re: OPLSS thread 

how tf do I draw a histomorphism

re: OPLSS thread 

What is a function Mu F -> Cofree F A ???

re: OPLSS thread 

We've got our fourth positive COVID test today... unless they were already included in the count idk. I only know one of the lecturers caught it

re: OPLSS thread 

I'm so fucking itchy I hate this I wanna be OUTSIDE but the outside HATES ME

re: OPLSS thread 

There's someone in our group whose first exposure to pattern matching might be Agda... oof
Come to think of it though, everything we've been doing could've been done in Haskell, idk when we're going to get to dependent types

re: OPLSS thread 

Baby's First Category Theory Proof 😌

re: OPLSS thread 

Omg new exercises posted... but it's 11:30 pm aaa but I wanna do them

re: OPLSS thread 

Very suspicious of my para from cata

re: OPLSS thread 

Me: *coughs once* is it COVID

re: OPLSS thread 

lmao. technical difficulties

re: OPLSS thread 

also at some point someone told me cut elim was let-bound expressions and I was surprised but hearing Frank Pfenning explain it, it makes total sense and I don't remember why I was surprised

re: OPLSS thread 

If sequent calc without cut is natural deduction in normal form doesn't that mean proving cut elimination is proving normalization

re: OPLSS thread 

Lmao. It was the next thing he said

re: OPLSS thread 

Here we go. By induction on the derivations. The thing I've been doing for the past four months

re: OPLSS thread 

Huh. Lexicographical induction on the cut premises
I wonder how he's going to frame that concept bc I've never seen it in a proofy context

re: OPLSS thread 

Maybe sum of the heights of the derivations. Ew

re: OPLSS thread 

I am always hearing about hereditary substitution

re: OPLSS thread 

Oh negative/positive types is codata/data
That's easier to remember than negative/positive

Follow

re: OPLSS thread 

If an ana then a cata is a hylo then what's a futu then a histo called

re: OPLSS thread 

There's hylo but no meta?? smh

re: OPLSS thread 

Somehow doing a concrete example has gotten me more confused. Maybe I'm just sleepy

re: OPLSS thread 

I forgot Thorsten follows me on Twitter
I quoted smth he said in lecture in my OPLSS shitposting thread 💀

re: OPLSS thread 

hold on. what is an isomorphism in category theory lol

re: OPLSS thread 

that's like. two morphisms and two laws

re: OPLSS thread 

I cannot pay attention to this type theory lecture lol

re: OPLSS thread 

I look up at the screen and suddenly we're doing cubical equality in agda. what happened

re: OPLSS thread 

send help I'm being haunted by hcomp

re: OPLSS thread 

hcomp is defined by recursion on types?? like type casing??

re: OPLSS thread 

The last speaker is a good speaker but the content is so boring I can't pay attention

re: OPLSS thread 

Oh no he picked the same arrow for function types and for reduction

re: OPLSS thread 

Running out of space in my notebook lol
Now OPLSS 2022 is going to be awkwardly divided across two notebooks

re: OPLSS thread 

ugh I wanna sit outside and work bc it's so nice out but I know if I stay too long out I'll start leaking everywhere again... the AC is so strong inside I'm COLD

re: OPLSS thread 

idk how some people have the time to go out for drinks and socialize bc there are literally so many homework exercises I want to do lmao
I'm STILL doing the algebra of programming ones but I want! to write! the abstract machine compiler!! and I probably will be up a little late to do that lol
I played some card games after dinner with ppl and that was fun so I don't regret that at all but each day is so long while there's still not enough time for everything

re: OPLSS thread 

but I also want to clean up my slides and I want to edit the POPL paper and I want to look over the JFP feedback HELP

re: OPLSS thread 

wth is a futumorphism supposed to do

re: OPLSS thread 

wait, not futumorphisms. what's the dual of mutumorphisms called

re: OPLSS thread 

oh! you start with either one of the two seeds. at every step you produce a new seed which may be one or the other. the coinductive is constructed from these seeds

re: OPLSS thread 

I'm "in bed" but I wanna come up with a use for wutus...

re: OPLSS thread 

@ionchy probably time travel I assume

re: OPLSS thread 

@ionchy oh boy learning op sem for the 10th time

Sign in to participate in the conversation
types.pl

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