Recent searches
Search options
I wrote a thing!
Bidirectional Typechecking is Bidirectional
https://cybercat.institute/2025/01/28/bidirectional-typechecking/
Cybercat InstituteBidirectional Typechecking is BidirectionalFor a while I've had an intuition that typechecking should be optical, with subterms going forwards and types (and type errors) for subterms going backwards. In this post I'll make sense of this idea, by implementing a bidirectional typechecker for simply typed lambda calculus as an optic, using Haskell's Control.Lens.
@julesh I am spending a hell of a lot of my time writing a typechecker for a lambda-calculus-like (closer to system F) language lately so I'm excited to give this a read!
@julesh I wish I had quote toots so I could tell people this is one of the most exciting developments in optics and PL :D
@zanzi Just grab the url and stick it at the bottom of the twoot, like people used to do it on twitter back in the day
@julesh ok, i'll do it like a *pleb* :P