我发现这个
webapp可以让你为给定的类型生成一个自由定理.

生成的定理量化了这些类型的类型和关系.这些定理(公式)是哪个理论/逻辑系统的定理？这个系统如何与语言的等式理论相关？

最佳答案 请参阅介绍所有内容的论文.

http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf