Oh cool! What were you learning about? How did you find it?
Conversation
Honestly I don’t remember how I got there, I think I was generally reading about category theory and type theory, maybe I was reading something on Agda (not sure) and then it was an usual case of a tangential rabbit hole. Just found out what it means & how it could be implemented
2
Oh neat! Yeah it's surprisingly not too hard to implement them. But yeah, dealing with the implications of implementing them is kind of where the 'fun' comes in. Like, how to generated efficient code when types are first class.
1
3
I found these helpful when learning how to implement them for Pikelet:
- math.andrej.com/2012/11/08/how
- andres-loeh.de/LambdaPi/
- davidchristiansen.dk/tutorials/nbe/
3
3
15
Ahh these are lovely👌, thank you!
1
No worries! I'm super interested in doing them in a 'graph' based way. And having a nice GUI for editing with them (which may or may not expose that graph). Eg.
Quote Tweet
2
1
Interesting! Do I understand it correctly that Point belongs to the Type set, and what’s possible to do with Type would be also applicable to point; I don’t understand how the “records” work there e.g is it a “property” of type that maps the vals, or..?
1
`Point` is an element of the type `Type`. So it can be used in places where types are expected, like as type annotations on function parameters, or record fields.
1
1
In the example I'm building up another record which is kind of like a 'module', which gives the type, and a constructor function. It's a bit pointless though - was more just experimenting with notation.
1
1
Got it, thanks! As an aside, the possibilities for (better/novel/more accurate symbolically) math notation are so interesting
1
1
Replying to
Yeah, there's so many cool possibilities! I think it's kind of interesting to see them as something that can be 'designed' and played around with creatively.
Replying to
Definitely. I often think about it when I work on algorithms for the plant game. Just thinking about a problem in a different way symbolically will show you a unique way to solve the problem
1