Haskell:类型变量是否与父项在同一名称空间中的"where"子句中？

Question

在下面的片段中(我已经抽象了所有其他琐碎的部分)

data T s = T (s -> s)

foo :: T s -> s -> s
foo (T f) x = bar x where
    bar :: s -> s
    bar a = f a

我收到了以下错误

Couldn't match expected type `s1' with actual type `s'
  `s1' is a rigid type variable bound by
       the type signature for bar :: s1 -> s1 at /tmp/test.hs:5:12
  `s' is a rigid type variable bound by
      the type signature for foo :: T s -> s -> s at /tmp/test.hs:3:8
In the return type of a call of `f'
In the expression: f a
In an equation for `bar': bar a = f a

我的猜测是bar's签名中的类型变量不与命名空间共享foo,因此编译器无法推断这两者s实际上意味着相同的类型.

然后我发现这个页面的Scoped类型变量,这表明我可以使用{-# LANGUAGE ScopedTypeVariables #-},这没有帮助.我得到了同样的错误.

Answer 1

类型变量是否在与其父项相同的命名空间中的"where"子句中？

没有*.如果你想到这一点,这会变得容易foo :: s -> s一些foo :: forall s. s -> s.毕竟,类型变量表明该函数适用于任何类型s.让我们为您的代码添加明确的量化:

{-# LANGUAGE ExplicitForAll #-}

data T s = T (s -> s)

foo :: forall s. T s -> s -> s
foo (T f) x = bar x where
    bar :: forall s. s -> s
    bar a = f a

如你所见,那里有两个forall s..但是那个bar是错的.毕竟,你不能选择任何 s,但已经使用过的s.这可以通过启用ScopedTypeVariables:

{-# LANGUAGE ScopedTypeVariables #-}

data T s = T (s -> s)

--     vvvvvvvv  explicit here
foo :: forall s. T s -> s -> s
foo (T f) x = bar x where
    --     vvvvvv  same as above here
    bar :: s -> s
    bar a = f a

但是,有一些技巧要摆脱ScopedTypeVariables.例如,在这种情况下的以下内容:

data T s = T (s -> s)

foo :: T s -> s -> s
foo (T f) x = (bar `asTypeOf` idType x) x where

    bar a = f a

    idType :: a -> a -> a
    idType a _ = a

-- For completion, definition and type of 'asTypeOf'
-- asTypeOf :: a -> a -> a
-- asTypeOf x _ = x

对于任何x :: s术语idType x都具有类型s -> s,并asTypeOf强制两者具有相同的类型.

根据您的实际代码,这样的事情可能或多或少可行.

^{*嗯,在这种情况下,由于可以使用ScopedTypeVariables,请参阅后面的部分答案.}

Answer 2

ScopedTypeVariables确实是解决方案,但是还有一个额外的要求:使用它们:必须forall在类型签名中加上明确的s来声明要扩展的变量,如下所示:

foo :: forall s. T s -> s -> s

这样,代码中签名的含义不依赖于是否启用了扩展.