Show older

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 😌

re: OPLSS thread 

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

Follow

re: OPLSS thread 

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

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.