Prepare a better and faster representation for unification.
Context
Currently Teika uses alpha renaming for type checking, while this works nicely and is conceptually closer to the source behavior, it relies on alpha-renaming which is in general slow and it additionally makes unification considerably harder.
This representation split variables in 3, rigid, local and global vars, the first two are equivalent to locally nameless free and bound vars, while global vars are a relocatable version of local vars, the goal is that all the terms in the substitution list are packed and as such they don't require any shifting, packing has a cost, but it is paid only once when creating the substitution.
Warning
This is likely not the final representation, just an intermediary state to show case a couple techniques, used here, namely packing which may be a worth optimization in the future.
Goals
Prepare a better and faster representation for unification.
Context
Currently Teika uses alpha renaming for type checking, while this works nicely and is conceptually closer to the source behavior, it relies on alpha-renaming which is in general slow and it additionally makes unification considerably harder.
This representation split variables in 3, rigid, local and global vars, the first two are equivalent to locally nameless free and bound vars, while global vars are a relocatable version of local vars, the goal is that all the terms in the substitution list are packed and as such they don't require any shifting, packing has a cost, but it is paid only once when creating the substitution.
Warning
This is likely not the final representation, just an intermediary state to show case a couple techniques, used here, namely
packingwhich may be a worth optimization in the future.Related
199