Rust was a gateway drug to getting into functional programming and I don’t know how to feel about this
Conversation
Just wait till you get to dependently typed programming! 😍
1
6
I was reading up on it the other day 🙃
1
2
Oh cool! What were you learning about? How did you find it?
1
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
Replying to
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
Quote Tweet
Still trying to figure out how to be able to work on programming languages and graphics at the same time… it keeps wanting to work on programming language stuff right now… it's just so easy to keep chipping away at the PL work…
Show this thread
1
2
I feel you. I’m trying to stick to graphics as I made the switch from embedded to “full-stack” game programming fully in October & want to be much more experienced before making a deep dive into another sub-field. I’d recommend whole separate days for separate “fields” to focus
1
Replying to
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
Show replies