one of the things I want to be pretty easy to work with in tmTTmt is rank-2 type systems:
rank-2 type systems consist of:
- monotypes (types with no polymorphism, i.e. no
forall: just things likeInt,Int -> Int, and so on) - rank-1 types, which can have
forall, but never as an input to a function - rank-2 types, which can have
forallas an input to a function but not further nested
the way you hop up a level is the same each time, so in theory you could define this data type as a nesting of functors RankUp (RankUp Monotype))
except it's really annoying to actually pattern match on that datatype
so I just hope to make it easier to do the pattern matching part, so it looks like compiler magic that it magically tracks what rank your types are at, even though it would hopefully just be a little bit of sugar and not require dependent types
(there's a pesky detail though, about how to differentiate what level function types are at, so I'll have to see if it actually pans out for me)
(I haven't actually implemented a type system for tmTTmt yet)
why rank 2 types? I think they're the best you can do for unification
apparently for rank 3 types, unification ends up being undecidable ... but I've never really understood that proof
just a big gaping hole in my knowledge lol
but for rank 2 types, the conceptual idea seems pretty straightforward, but it ends up being pretty fiddly, and I haven't figured out all the details of scoping and such
ugh my tag has the wrong capitalization and it's going to bug me and I don't think I can fix it??
