教堂式核心中缺少类型变量会发生什么？ [英] What happens to missing type variables in Church-style core?

问题描述

这有点深奥，但令人发狂。在回答另一个问题时，我注意到在这个完全有效的程序中

  poo :: String  - > a  - > a 
 poo _ = id 
 
 qoo ::（a  - > a） - >字符串
 qoo _ =
 
 roo :: String  - >字符串
 roo = qoo。 poo 
  

类型变量 a 在检查 roo 过程中也没有概括。我想知道在翻译成GHC的核心语言 - 一种教堂式的系统F变体时会发生什么。让我把这些事情说出来，用显式类型lambda / \ 并输入应用程序 @ 。

  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。字符串 - >字符串
 roo = qoo。 poo 
  

会经过确认，这可能并不意味着该物体没有额外的量化。 / p>

这里发生了什么？ （添加一些 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 用于多态类型。 / p>

从文档（强调我的）：

类型构造函数任何都是您可以不安全地强制任何
提升类型并返回的类型。

• 它被解除，因此由一个指针表示
  
• 它并不声称
  是一个数据类型，这对代码生成器很重要，因为
  code gen可能会输入一个数据值，但从不输入函数值。
  
  
  

  它也是用于一世在类型
  检查后显示非约束类型变量。

  
  

有这样一种类型插入来代替不受约束的类型，否则像 length [] 这样的简单表达式会导致模糊的类型错误。

This is a bit esoteric, but maddening. In an answer to another question, I noted that in this entirely valid program

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

the type variable a is neither solved nor generalized in the process of checking roo. I'm wondering what happens in the translation to GHC's core language, a Church-style variant of System F. Let me spell things out longhand, with explicit type lambdas /\ and type applications @.

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 @ ?)

What on earth goes in the ? places? How does roo become a valid core term? Or do we really get a mysterious vacuous quantifier, despite what the type signature says?

roo :: forall a. [Char] -> [Char]
roo = /\ a -> ...

I've just checked that

roo :: forall . String -> String
roo = qoo . poo

goes through ok, which may or may not mean that the thing typechecks with no extra quantification.

What's happening down there?

解决方案

Here's the core generated by GHC (after adding some NOINLINE pragmas).

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)

It seems GHC.Prim.Any is used for the polymorphic type.

From the docs (emphasis mine):

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.

It makes sense to have such a type to insert in place of un-constrained types, as otherwise trivial expressions like length [] would cause an ambiguous type error.

这篇关于教堂式核心中缺少类型变量会发生什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！