是否可以在简单类型的lambda演算上编写列表函数？

你可以写多态列表的功能,例如cons,nil和reverse对STLC？

要详细说明问题,为了cons在Haskell中编写,您需要多态类型:

cons : ? a . a -> List a -> List a

?在STLC上没有这样的东西,所以我认为很明显多态列表函数是不可能的,即你需要cons为每个专用列表类型编写一个新的定义.但是,如果您将类型注释保留,请改为:

cons = ...
a = cons 1 []
b = cons "" []

推理器可以识别cons : Int -> List Int -> List Int第一种情况,cons : String -> List String -> List String第二种情况 - forall不需要.在这种观点下,看起来像多态列表函数在STLC上不是问题 - 你只是不能注释它们的类型.

不,在STLC上编写多态函数是不可能的.在STLC的定义中,没有普遍量化的类型.为了表示多态列表,您需要一些带有类型抽象的语言,比如System F.

在你的问题中你混合了(请纠正我,如果我理解错了)STLC的推理算法.如果您需要多态类型,则需要一种具有类型抽象和应用程序的语言(以便进行类型实例化).

类型推断算法(如Haskell或ML使用的算法)考虑系统F的限制版本,通常称为Mini(或Core)ML.这种限制的动机是类型推断的不可判断性和系统F的检查(详情请参见此处).有关这方面的更多详细信息,请访问:

类型和编程语言的第23章

一种简单的应用语言:Mini-ML.本文介绍了Mini-ML语言:它的语法,语义,类型系统和类型推理算法.它很旧,但非常易读.

任意秩类型的实际类型推断呈现了系统F的更具表现力的片段,并讨论了它在Haskell中的实现.