Haskell或特定编译器是否有类似于类型级lambda的东西（如果这是一个术语）？
具体而言，假设我有一个参数化类型Foo a b，并且希望Foo _ b成为Functor的一个实例。是否有任何机制可以让我执行类似于下面的操作
instance Functor (\a -> Foo a b) where
...
?
7个回答
27
虽然sclv已经回答了你的直接问题，但我想补充一下，“类型级λ”有不止一种可能的含义。 Haskell有各种类型运算符，但没有一个真正像lambda函数一样的运算符：
- 类型构造函数：引入新类型的抽象类型运算符。给定类型
A和类型构造函数F，函数应用F A也是一种类型，但没有比“这是F应用于A”更多的（类型级）信息。 - 多态类型： 类型如
a -> b -> a隐含地意味着forall a b. a -> b -> a。forall在其范围内绑定类型变量，因此行为类似于lambda。如果我记得没有错，这大致上是System F中的“大写Lambda”。 - 类型同义词：类型运算符的有限形式，必须完全应用，并且只能产生基本类型和类型构造函数。
- 类型类： 本质上是从类型/类型构造函数到值的函数，具有检查类型参数的能力（即通过模式匹配类型构造函数的方式，与常规函数模式匹配数据构造函数的方式相似），并用于定义类型的成员关系谓词。在某些方面它们更像常规函数，但非常有限：类型类不是可以操纵的头等实体，并且它们仅作为输入（不是输出）的类型和值进行操作，只作为输出值（绝对）不是输入。
- 功能依赖： 与其他一些扩展一起，它们允许类型类隐式产生类型作为结果，这些类型然后可以用作其他类型类的参数。仍然受到非常有限的限制，例如无法将其他类型类作为参数。
- 类型族： 类似于功能依赖所做的替代方法；它们允许以看起来更接近常规值级函数的方式定义类型上的函数。然而，通常的限制仍然适用。
其他扩展程序放宽了上述限制，或提供了部分解决方法（参见：Oleg的类型技巧）。然而，在任何地方以任何方式几乎唯一不能做到的一件事情就是您所询问的，即使用匿名函数抽象引入新的绑定范围。
- C. A. McCann
1
对于多态类型，数据声明不就是定义类型 lambda 的一种方式吗？特别是在使用 GADT 语法时，在头部的类型变量具有作用域，所以
data Foo a b where ... 实际上是使用 Scala 3 语法定义了类型 lambda [a, b] => F[A,B]。但是在 Haskell 中，Kind 为 * -> * -> * 的东西毕竟是一种类型 lambda，只是在 kind 级别上没有命名的类型变量而已。 - MaatDeamon20
来自 TypeCompose：
newtype Flip (~>) b a = Flip { unFlip :: a ~> b }
http://hackage.haskell.org/packages/archive/TypeCompose/0.6.3/doc/html/Control-Compose.html#t:Flip
如果一个东西接受两个参数并且是“Functor”，你可以将其成为双函子：
http://hackage.haskell.org/packages/archive/category-extras/0.44.4/doc/html/Control-Bifunctor.html
(或者，在之后的 category-extras 中，还有一种更通用的版本：http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html#t:Bifunctor)
- sclv
7
我不太喜欢自问自答这个想法，但是根据Freenode上#haskell频道的几位用户所说，Haskell没有类型级别的lambda表达式。
- gspr
3
7它们存在于System F(c)中，这也是Haskell编译的对象，但用户无法直接看到它们，除非间接地。 - Don Stewart
4“System F(c) that Haskell compiles to” 可以翻译为“Haskell编译成的System F(c)”；“That GHC compiles to” 可以翻译为“GHC编译成的”。因此，完整的句子翻译为“Haskell编译成的System F(c)，GHC也可以编译成”。 - wnoise
2Don是对的，System F_c支持类型级函数。但是，它们始终是非参数化的，这意味着这些函数总是通过对其参数进行情况分析来定义。System F_c无法表达上面问题中的代码，因为实例中的函数是参数化的。 - svenningsson
6
EHC（以及其可能的后继者UHC）具有类型级别的lambda表达式，但它们没有记录文档，也不如依赖类型语言中强大。我建议您使用依赖类型语言，例如Agda（类似于Haskell）或Coq（不同，但仍然在核心上是纯函数式的，并且可以惰性或严格地进行解释和编译！）但我对这些语言有偏见，对于您在这里所提出的要求来说，这可能是100倍以上的过度杀伤力！
- Robin Green
2
我知道的最接近获得类型lambda的方法是通过定义类型同义词。在您的示例中，
data Foo a b = Foo a b
type FooR a b = Foo b a
instance Functor (FooR Int) where
...
即使使用了-XTypeSynonymInstances和-XFlexibleInstances，这也不起作用；GHC希望在实例头中完全应用类型同义词。可能有一些方法可以使用类型族来解决。
- Chris Smith
1
根据情况，您可以用“翻转”的方式替换原始类型定义，然后为“正确”的版本创建一个类型同义词。
来自
data X a b = Y a b
instance Functor (\a -> X a b) where ...
到
data XFlip b a = Y a b -- Use me for instance decalarations
type X a b = XFlip b a -- Use me for everything else
instance Functor XFlip where ...
- Quelklef
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接