The Robot Kata is a well known exercise, but could it be made to be completely typesafe? What if instead of having runtime errors, or even representing illegal moves with a sum type we instead let the compiler enforce all the constraints?
This is an exploration of what it could look like to solve this problem using this style and approach. Particular attention was directed into making all the type-level code as expressive as possible, to a ridiculous extent. There's value in going overboard and seeing what happens when you turn it all to 11. Hope you enjoy this and leave some feedback (open an issue maybe?).
Enjoy!