Okay need help for a quick slide
What's a good example of using types to specify high-level structure of a domain problem? Like where the types alone form a specification (not necessarily complete) of a system/problem. It doesn't have to be beginner-accessible.
Conversation
Replying to
Servant perhaps? Or Idris's type-level state machine specifications?
Np! Lots of stuff in the paper, ‘The Power of Pi’, too. I’m also working on a external DSL for parsing binary formats based on dependent types (still a private repo), but this has been done before with PADS/DDC, so you might find interesting stuff there.
2