­jonoodle­ @ionchy@types.pl

Trying to sleep but I just remembered I forgot to handle the regrade requests
And set up zoom recording

I will convince you why this is a bad idea. In fact I have an entire section and a half devoted to why it's a bad idea

Someone reopened my draft pull request for sized types

Why

Okay I've relearnt how to use macros. I can think about how to teach them on the bus or smth

I also always want to add type signatures to macro definitions but I'll inevitably run into one eventually where I don't know how to do it

@wilbowma oh I guess there's that too, but looks like define-syntax-rule is for when you only have one rule and the pattern's right at the top like (define-syntax-rule (name . args) ...) like define for functions
I was wondering why we don't use that in tutorial but later on we have multiple rules, so

@wilbowma also define-syntax-rule in the other direction

I always forget what the () in syntax-rules is for

(define-syntax f (syntax-rules () ...)) has big (define f (lambda () ...)) energy

My half-screen is working again for some mysterious reason. I can't live like this but I could get half the work I normally do done I guess

@operand yeah, guarded types is kind of the only "actual" application I'm familiar (ish) with lol

Was the internalization of parametricity a modality? I don't remember if anyone did that

I'm not actually sure what modal type theories are for
I mean I did try to express size erasure as a modality but that's not programming. That's math

@hazel ocean vibes hazel

idk if there's dots to connect here

If ◻ is an internalization of validity and represents closed code
and closures are pieces of closed code

Might save these for a more condensed tweet for a rainy day

type theorist voice three things is just two things where one of the things has two things