Not a big fan of podcasts. I started reading The Little Typer to get into Dependent Type Theory. The author gave a talk at Strange Loop 2018 which is available: youtube.com/watch?v=VxINoKFm-S4 cc: Kartik Agaram

Those credits 😂

I feel like thats almost every talk in the last few years he’s given. One example - youtu.be/D43PlUr1x_E?t=1777

that talk got 220k views btw, which is awesome

Srini! hi im back!

it's wild i was going through all of yoshiki ohshima’s uploads and finding none of them—good to know there are a lot more talks/sources nowadays

wait… this video doesn't include the “collapse” part—I know he references sketchpad in basically every talk

ah got it

A couple people mentioned zippers, which are closely tied to continuations. To be a hair more precise, you can think of a zipper as saving a place in the traversal of a data structure. I think they're important from a PLT perspective.

Wow Andrew F, I've never thought of the connection, but it is obvious and beautiful.

I surely didn't discover it myself. Enter the rabbit hole if you dare. ;) okmij.org/ftp/continuations/zipper.html

Thank you. Ah ha! This bit, "We show [delimited continuations] offer a uniform view of many scenarios that arise in systems programming, such as a request for a system service, an event handler for input/output, a snapshot of a process, a file system being read and updated, and a Web page." Far on my back burner, I have this idea of a "kinetic programming" environment where something like delimited continuations are one of the primary constructs.

Imagine yourself in a VR void. In the beginning, you just have your own motion of head and hands. So record a segment of your motion, reify it. Pick it up, put it over there: a translation in space. Flatten the time and orientation dimensions: now you have three paths, head, left, and right hand. Pick out the right hand path. Map it over the left hand path. Now you have a surface. If the right path was an arc and the left path was a loop, the resulting figure could be a ball. Turn the head path back into motion over time, attach the ball to the head, and now it's bobbing around. Copy the whole thing and now you have a field of floating orbs.

Once I implemented a simple bloom filter. A while back. It was an interesting experience

Lessons Shubhadeep Roychowdhury?

I forgot how exactly it was, but I remember one thing I felt that to be effective most of the time the number of hash functions and size of the bit array has to REALLY big. I may have gotten something wrong. But smaller they are bigger the chances of False Positive.