Lambda用于Haskell中的类型表达式？

Question

Haskell或特定编译器是否具有类型级lambda(如果这甚至是一个术语)？

详细说,我说有一个参数化类型,Foo a b并希望Foo _ b成为一个实例,比如Functor.是否有任何机制可以让我做类似的事情

instance Functor (\a -> Foo a b) where
...

？

Answer 1

虽然sclv回答了你的直接问题,但我会补充一点,"类型级lambda"的含义不止一个.Haskell有各种类型的运算符,但没有一个真正表现为正确的lambdas:

类型构造函数:引入新类型的抽象类型运算符.给定一个类型A和类型构造函数F,函数应用程序F A也是一个类型,但不包含" F应用于此"的其他(类型级别)信息A.
多态类型:类似a -> b -> a隐式的类型forall a b. a -> b -> a.在forall其范围内结合的类型变量,从而表现有点像的λ.如果记忆为我服务,这大致是系统F中的"资本lambda".
类型同义词:必须完全应用的有限形式的类型运算符,并且只能生成基类型和类型构造函数.
类型类:本质上是从类型/类型构造函数到值的函数,能够检查类型参数(即,通过类型构造函数上的模式匹配,与常规函数模式在数据构造函数上匹配的方式大致相同)并用于定义成员资格关于类型的谓词.这些行为在某些方面更像是常规函数,但是非常有限:类型类不是可以操作的第一类实体,它们仅作为输入(不是输出)和值仅作为输出操作(绝对不是输入).
功能依赖:与其他一些扩展一起,这些类允许类型类隐式生成类型作为结果,然后可以将其用作其他类型类的参数.仍然非常有限,例如,无法将其他类型类作为参数.
类型系列:功能依赖关系的另一种方法; 它们允许以更接近常规值级函数的方式定义类型上的函数.但是,通常的限制仍然适用.

其他扩展放松了一些提到的限制,或提供部分解决方法(另请参阅:Oleg的类型hackery).然而,几乎你不能以任何方式做任何事情的一件事正是你所要求的,即引入一个带有匿名函数抽象的新绑定范围.

Answer 2

来自TypeCompose:

newtype Flip (~>) b a = Flip { unFlip :: a ~> b }

另外,如果某个东西是两个参数中的Functor,你可以把它变成一个bifunctor:

Answer 3

我不喜欢回答我的问题的想法,但显然,根据几个人就Freenode上#haskell,Haskell没有类型级lambda表达式.

它们存在于Haskell编译的系统F(c)中,但除了间接编辑外,对用户不可见. (6认同)
"Haskell编译为"的系统F(c)".那GHC编译成. (4认同)
Don在System F_c体育类型级别功能中是正确的.但是,它们始终是非参数的,这意味着这些函数总是通过对其参数进行大小写分析来定义.系统F_c无法表达上述问题中的代码,因为实例中的函数是参数化的. (2认同)

Answer 4

EHC(也许还有其继承者,UHC)具有类型级别的lambda,但它们没有文档记录,也没有依赖类型语言那么强大.我建议您使用依赖类型的语言,例如Agda(类似于Haskell)或Coq(不同,但仍然是纯函数的核心,可以懒惰或严格解释和编译!)但我偏向于这些语言,这可能是你要求的100倍矫枉过正!