Type-Level Programming Syntax

Read the files in order. It may take a few read-throughs for it to make sense as to why some things are needed but it will make sense eventually.

Note: there is an annoyance that can occur if you play around with the code: due to using the same names for some things, the IDE may try to import these names from other modules. If it does so, it may result it some definition being declared twice in the same file and produce a compiler error. If you experience such a problem, check the top of the file and delete any imports there.

Other Learning Sources

Consider purchasing Thinking with Types, a book that claims to be "the comprehensive manual for type-level programming". Abhinav Sarkar also made his notes public