I think there could be practical applications. The type systems of most commonly used languages are not very sophisticated. The problem is the focus on lamda c

I think there could be practical applications. The type systems of most commonly used languages are not very sophisticated. The problem is the focus on lamda calculus imo. I get it that it's nice for mathematics and proofs, but for (almost all) practical applications it's useless.