Show older

re: OPLSS thread 

time to draw some category theory diagrams. I wonder how I'm supposed to do this when none of the types are written down... you're saying I need to derive them myself? smh

re: OPLSS thread 

feeling bad about not doing the intro type theory exercises despite likely already knowing everything in them

re: OPLSS thread 

It's like 1984, type theory is like newspeak: you can't say anything evil

re: OPLSS thread 

When lowercase f is used for both the functor/type and a function: kill kill kill die die die

re: OPLSS thread 

Using out for both the constructor "on paper" and the destructor "in Haskell": die die die die

re: OPLSS thread 

Doing functors in "category theory" but then doing bifunctors in "Haskell": kill kill kill kill

re: OPLSS thread 

This bifunctor stuff is confusing me so much. Can we go back to functors

re: OPLSS thread 

Why use Bifunctor instead of like.
Okay so we want that Mu f is a functor so f needs to be a Bifunctor bc f is a Functor in its second argument
But you could just say that (\x. Mu (f x)) is a functor instead

re: OPLSS thread 

I'm thinking of (after all the lectures are over) rewriting all of my notes with notation that I prefer (and that is consistent throughout!) bc this material is really interesting but just so confusing when mixed with Haskell's limitations on names

re: OPLSS thread 

It bothers me that all this machinery is set up to use bifunctors but you only ever bimap id over the first type and the only time it's useful is to make the fixed point of the bifunctor a functor

re: OPLSS thread 

I bet later on we'll do something more interesting than merely id... but I don't see it yet

re: OPLSS thread 

Wait a minute. If there exists a unique x such that P(x) and I can show that P(y) for some y, then x = y right
I was so caught up in the category theory I forgot how logic works

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 😌

Follow

re: OPLSS thread 

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

re: OPLSS thread 

wondering if I want to write tests and if so how to set up testing in Haskell lol

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

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

Show newer

re: OPLSS thread 

a congruence is a congruent equivalence relation?? lemme edit my thesis real quick

re: OPLSS thread 

iterator is cata... recursor is para... I am connecting the dots

re: OPLSS thread 

@ionchy Lexicigraphical induction on types then terms will get you out of a lot of scrapes. This sounds a lot like the proofy counterpart.

re: OPLSS thread 

@pigworker that's exactly what he did next!

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.