Show newer

oh my god it's a typo. it's supposed to be a cdot, not a .

Show thread

The name is pretty funny though. because it's represented by a type, haha get it

Show thread

A cwf is democratic provided each context Γ is represented by a type Γ in the sense that there is an isomorphism γ_Γ : Γ ≃ 1.Γ̅

what is. what's this 1. notation. pleas

Show thread

From the definition of ucwf it is immediately clear that an
initial ucwf Tucwf can be generated inductively

no it's not! show me!

Show thread

OH about a restaurant 

And I thought I was extra pretentious about ice cream in listing places that serve single scoops over 6$

Show thread

OH about a restaurant 

I'm like oh East is East is a little pricey but I would go time to time and it's totally worth it to me. But 75$ for dinner????

no

Show thread

OH about a restaurant 

"It was 75$ a head"
"Oh! That's doable"

75$??????

presheaves have a universal property whose statement I can't read so I'm going to ignore it until they bring it up

Show thread

Like at this point if you're saying things like "D-valued presheaf over C" you can just say a contravariant functor from C to D
I'm guessing D is typically Set but in a cwf it's Fam instead so clearly it can be other categories that aren't Set-like

Show thread

Is a presheaf just a contravariant functor or are there additional properties I can assume that they haven't mentioned here beyond the functor

Show thread

a key feature of the notion of cwf is
that it can be presented as a generalized algebraic theory

you're really gonna make me learn One More Thing huh

Show thread

Waking up tired disease. Dependency on coffee disorder

Show thread

I've already been yelled at by two people on the street I've had enough of the day

Show thread

I left my hoodie at home
Do I go back to get it? I'm literally halfway to campus

literal quote from Haskell bytestring package documentation 

Deprecated and unmentionable

accursedUnutterablePerformIO :: IO a -> a

This "function" has a superficial similarity to unsafePerformIO but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the IO monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet.

Witness the trail of destruction:

github.com/haskell/bytestring/
github.com/haskell/bytestring/
ghc.haskell.org/trac/ghc/ticke
ghc.haskell.org/trac/ghc/ticke
ghc.haskell.org/trac/ghc/ticke

Do not talk about "safe"! You do not know what is safe!

Yield not to its blasphemous call! Flee traveller! Flee or you will be corrupted and devoured!

Show thread
Show older
types.pl

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