这有点深奥,但令人抓狂。在对 another question 的回答中,我注意到在这个完全有效的程序中
poo :: String -> a -> a
poo _ = id
qoo :: (a -> a) -> String
qoo _ = ""
roo :: String -> String
roo = qoo . poo
类型变量
a
在检查roo
的过程中既没有解决也没有概括.我想知道在翻译成 GHC 的核心语言(System F 的 Church 风格变体)时会发生什么。让我用明确的类型 lambdas /\
将事情拼写出来。并键入应用程序 @
.poo :: forall a. [Char] -> a -> a
poo = /\ a -> \ s x -> id @ a
qoo :: forall a. (a -> a) -> [Char]
qoo = /\ a -> \ f -> [] @ Char
roo :: [Char] -> [Char]
roo = (.) @ [Char] @ (? -> ?) @ [Char] (qoo @ ?) (poo @ ?)
?
中到底有什么地方? roo
如何成为有效的核心术语?还是我们真的得到了一个神秘的空量词,尽管类型签名说了什么?roo :: forall a. [Char] -> [Char]
roo = /\ a -> ...
我刚刚检查过
roo :: forall . String -> String
roo = qoo . poo
顺利通过,这可能意味着也可能不意味着该事物在没有额外量化的情况下进行类型检查。
下面发生了什么事?
最佳答案
这是 GHC 生成的核心(在添加了一些 NOINLINE
编译指示之后)。
qoo_rbu :: forall a_abz. (a_abz -> a_abz) -> GHC.Base.String
[GblId, Arity=1, Caf=NoCafRefs]
qoo_rbu = \ (@ a_abN) _ -> GHC.Types.[] @ GHC.Types.Char
poo_rbs :: forall a_abA. GHC.Base.String -> a_abA -> a_abA
[GblId, Arity=1]
poo_rbs = \ (@ a_abP) _ -> GHC.Base.id @ a_abP
roo_rbw :: GHC.Base.String -> GHC.Base.String
[GblId]
roo_rbw =
GHC.Base..
@ (GHC.Prim.Any -> GHC.Prim.Any)
@ GHC.Base.String
@ GHC.Base.String
(qoo_rbu @ GHC.Prim.Any)
(poo_rbs @ GHC.Prim.Any)
看来
GHC.Prim.Any
用于多态类型。来自 the docs (强调我的):
The type constructor
Any
is type to which you can unsafely coerce any lifted type, and back.
- It is lifted, and hence represented by a pointer
- It does not claim to be a data type, and that's important for the code generator, because the code gen may enter a data value but never enters a function value.
It's also used to instantiate un-constrained type variables after type checking.
插入这样一个类型来代替不受约束的类型是有意义的,否则就像
length []
这样的琐碎表达式会导致模棱两可的类型错误。
关于haskell - Church 风格的核心中缺少类型变量会怎样?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/7076517/