为什么这个eta扩展是必要的？

Question

有人可以帮我理解这个/给我一些阅读材料吗？以下工作正常:

type F a b = Functor f => f a -> f b
fComp :: F b c -> F a b -> F a c
fComp f f' = f . f'

但是,如果我写fComp = (.),而类型检查器抱怨:

Couldn't match type ‘b0 -> f c’
              with ‘forall (f1 :: * -> *). Functor f1 => f1 b -> f1 c’

(这个具体的例子并不是特别有用;我只是想缩小研究镜头时出现的例子.)

Answer 1

fComp对于更高级别的类型具有更高级别类型和类型推断是非常有限的.如果我们扩展类型同义词,它可能会更容易理解(但更长!)

fComp :: forall f a b c. Functor f => 
                (forall f1. Functor f1 => f1 b -> f1 c) ->
                (forall f2. Functor f2 => f2 a -> f2 b) ->
                (f a -> f c)

的较高等级的类型f和f'在这种类型的签名明确指定.这让类型推断已经开始认识的类型f和f'等能够与类型来统一他们..

但是,如果你摆脱f和f',该类型.必须采取不得而知.不幸的是,系统无法推断出更高级别的类型,因此您会遇到类型错误.

本质上,编译器不能创建更高级别的类型来填充类型推断期间的未知数,并且必须依赖于程序员注释,我们需要名称(f和f')和类型签名来获取这些注释.

一个更容易理解的例子是更高级别的id功能:

myId :: (forall a. a) -> (forall b. b)

定义myId x = id x编译,但myId = id给出以下错误:

/home/tikhon/Documents/so/eta-expansion-needed.hs:11:8:
    Couldn't match type ‘b’ with ‘forall a. a’
      ‘b’ is a rigid type variable bound by
          the type signature for myId :: (forall a. a) -> b
          at /home/tikhon/Documents/so/eta-expansion-needed.hs:11:1
    Expected type: (forall a. a) -> b
      Actual type: b -> b
    In the expression: id
    In an equation for ‘myId’: myId = id
Failed, modules loaded: none.

(请记住,forall b. (forall a. a) -> b这与(forall a. a) -> (forall b. b).相同.)

Answer 2

让我使用类似System-F的表示法重写示例,其中我们也传递类型.下面,\\代表类型抽象(大lambda),以及字典抽象.此外,@代表类型/字典应用程序.

在此之前,请回忆一下以下类型(.):

(.) :: forall a b c . (b -> a) -> (c -> b) -> (c -> a)

这是带注释的代码(小心,不是为了胆小的人):

fComp :: F b c -> F a b -> F a c
fComp (f :: forall f1. Functor f1 => f1 b -> f1 c)
      (f':: forall f2. Functor f2 => f2 a -> f2 b) 
   = \\ ff :: (* -> *) ->
     \\ ffD :: Functor ff ->
     ((.) @ (ff c) @ (ff b) @ (ff a))   -- instantiated composition
     (f  @ ff @ ffD)                    -- first argument of (.)
     (f' @ ff @ ffD)                    -- second argument of (.)

(以上我假装a,b,c是类型常量以避免进一步的类型级lambda表达式.)

重要的部分:

• f并且f'正在使用特定类型.也就是说,它们在被馈送之前被应用于类型级参数(.).
• (.)在类型级别被施加到类型(ff c等),其都没有的多型体f和f'

正如您所看到的,原始代码远非微不足道.类型推断能够添加所需的类型级lambda和应用程序.在添加之后,我们不能再简单地签订合同fComp了.

在pointfree变体中,类型推断需要做的不仅仅是在有意义的情况下.虽然第一个参数fComp是类型F a b,但第一个参数(.)必须是形式x -> y,而不是统一的形式F a b = forall g . ....实际上,没有办法成功解决下面的打字尝试:

fComp :: F b c -> F a b -> F a c
fComp 
   = \\ ff :: (* -> *) ->
     \\ ffD :: Functor ff ->
     ((.) @ ???a @ ???b @ ???c)

上面没有???a,...可以导致想要的类型.

唯一的可能性是实例化forall隐藏在F x y类型中的-quantified变量,但要做到这一点,我们需要一个点.编译器可能会为您扩展该代码,以便出现点,从理论上讲可以实例化,但实际上不会.

(此外,在Haskell中,eta扩展并不总是有效的:例如返回时的seq (undefined::()->()) 3循环).seq (\x->(undefined::()->()) x) 33