haskell - 为什么您不能(完全)应用具有使用其他类型同义词的参数的类型同义词？

Question

我们可以用参数定义类型同义词，这在与实际类型一起使用时效果很好:

type MyType t = t String String

data Test a b = Test a b

f :: MyType Test
f = undefined

main = undefined

编译这不会导致任何错误:

$ghc --make test.hs                                           
[1 of 1] Compiling Main             ( test.hs, test.o )                                          
Linking test ...   

但是，当 Test 是类型同义词时，这不起作用:

type MyType t = t String String

data Test a b = Test a b

type Test' a b = Test a b

f :: MyType Test'
f = undefined

main = undefined

这给出了以下错误:

$ghc --make test.hs
[1 of 1] Compiling Main             ( test.hs, test.o )

test.hs:7:6:
    Type synonym Test' should have 2 arguments, but has been given none
    In the type signature for `f': f :: MyType (Test')

让我感到困惑的是 Test' 是 被应用于两个参数，那么为什么 GHC 提示我没有通过参数？

类型同义词不应该完全透明并且无法与其他类型的类型区分开来吗？

有没有办法实现预期的行为？

Answer 1

根据 Haskell report 类型同义词不能部分应用:

Type constructor symbols T introduced by type synonym declarations cannot be partially applied; it is a static error to use T without the full number of arguments.

特别是在扩展类型同义词之前检查了这一点，这意味着在表达式中:

MyType Test'

检查是在扩展 MyType 之前执行的，因此部分应用了 Test' 结果。

但是， 是 可能使用 GHC LiberalTypeSynonyms 扩展来实现该行为。此扩展将类型同义词视为宏，无需任何检查即可扩展它们，然后类型检查器将查看是否部分应用了类型同义词。

类型推断仍然在类型同义词扩展之前完成。

请注意，即使在这种情况下，类型同义词也不能部分应用，例如:

Test' Int

仍然是一个错误。但是，您现在可以使用类型同义词来完全应用其他类型的同义词而不会收到错误。

允许部分应用类型同义词会使类型推断不可判定，因此不可能在该方向上轻松扩展类型系统。