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 like Int, 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 forall as 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??


You must log in to comment.