Haskell 中仅用于传递类型信息的参数，有何术语和理论依据？

这类用法可以称为“用虚设参数传递类型信息”（dummy argument for type information），承担这一作用的参数也可以称为类型见证（type witness）。如果侧重编译器确认参数完全不需要求值，GHC 使用的术语是 absent argument；如果要求类型系统保证参数不参与运行时计算，对应的概念是 run-time irrelevance 或 erasure。

pseudo-phantom type 不适合作为这些情况的统一名称：API 用途、求值行为和类型系统约束是不同的问题，需要分别说明。

仅传递类型信息的参数，应该怎样称呼？

对题中的例子，可以这样描述：

Proxy 本身有正常的值：

Proxy :: Proxy Int

它不携带 Int 值，但仍然可以构造一个 Proxy Int。官方文档也将 Proxy 描述为传统 undefined :: a 用法的更安全替代方式。Data.Proxy 文档

为什么 phantom role 不能标记这些值参数？

GHC 的 role 用来判断，改变类型构造器的某个类型实参后，得到的类型是否仍具有相同的底层表示。它用于判断表示相等以及强制转换是否安全，不能说明函数是否读取某个值参数。

例如：

data Proxy a = Proxy

这里 a 的 role 是 phantom，表示 Proxy Int 与 Proxy Bool 的表示关系不要求 Int 与 Bool 有任何表示关系。

(->) 的两个参数具有 representational role，说的是函数类型构造器的表示关系，不能说明某个具体函数会不会使用参数。nominal 也是一种 role，因此不宜把 representational 简化为“所有非 phantom 情况”。GHC roles 文档

asTypeOf 的第二个参数被忽略，是其实现的性质：

asTypeOf :: a -> a -> a
asTypeOf = const

仅凭类型签名无法得出这个结论。下面的函数具有相同的类型，却会先将第二个参数求值到弱头范式：

sameTypeStrict :: a -> a -> a
sameTypeStrict x y = y `seq` x

普通函数类型没有表达“第二个参数不可用于运行时计算”这项约束。

“不求值”和“不生成 thunk”有什么区别？

普通惰性求值允许参数暂时不被求值，但参数仍可能在之后被使用。参数被确定为 absent，意味着对它的求值需求为零。

对于标准定义的 asTypeOf：

example :: Int
example = asTypeOf 42 (undefined :: Int)

第二个参数只影响类型检查，求取 example 的结果不需要求值这个 undefined。

GHC 的 demand analysis 包含 usage analysis，可以识别 absent arguments，再通过 worker/wrapper 等优化，用占位值替换参数或省略参数。“不必为完全不用的实参保留计算”已有对应的优化机制，术语是 absence analysis 或 absent argument。GHC 优化文档

这是编译器分析得到的优化结果。普通的 a -> b 签名没有承诺参数一定被擦除；具体是否消除调用开销，还取决于实现可见性、优化配置等条件。

unProxy 为什么能够通过类型检查？

unProxy :: Proxy a -> a
unProxy _ = undefined

在通常的安全、纯 Haskell 范围内，Proxy a 没有存储 a 值，也没有提供构造任意 a 所需的信息。因此，这个完全多态的签名不能实现一个对所有 a 都返回正常结果的函数。

它能通过类型检查，是因为 undefined :: a 在 Haskell 中合法。Haskell 允许 bottom，记作 ⊥，表示出错或不终止的计算。类型检查不会证明所有计算都终止，也不会排除显式的 undefined。Haskell 2010 Report：Errors

所以，不能把“well-typed programs can’t go wrong”理解成“Haskell 中任何通过类型检查的表达式都不会抛出异常或不终止”。具体的类型安全结论取决于语言及其形式化模型。

unProxy 的结果也并非一经传递就会导致程序退出。按非严格语义，如果接收方忽略该值，就不需要对它求值：

ignored :: Int
ignored = const 42 (unProxy (Proxy :: Proxy Bool))

只有在结果被要求求值时才会出问题。把结果称为 phantom，既不能提供一个正常的 a 值，也不能自动阻止后续求值。

如何让 API 更清楚地表达这种用途？

设计接口时，可以用 Proxy a 显式传递类型信息。例如，为现有 sizeOf 提供适配层：

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy (Proxy(..))
import Foreign.Storable (Storable, sizeOf)

sizeOfProxy :: forall a. Storable a => Proxy a -> Int
sizeOfProxy _ = sizeOf (undefined :: a)

boolBytes :: Int
boolBytes = sizeOfProxy (Proxy :: Proxy Bool)

调用方可以传入正常的 Proxy 值。适配层内部仍依赖 sizeOf 不使用参数值的约定；这个例子没有让类型系统强制检查所有实例都遵守该约定。Foreign.Storable 文档明确说明，sizeOf 不使用参数值。Foreign.Storable 文档

原问题中的 HTYPE_INT 属于所引用实现的上下文，不应直接当成应用代码中可用的类型，也不能据此写死 Bool 的存储字节数。

如果可以重新设计接口，TypeApplications 或 RequiredTypeArguments 可以让调用者直接提供类型。GHC 文档用一个假想的接口说明这一点：

sizeOf :: forall a -> Storable a => Int

这样可以写成 sizeOf Bool，不再需要虚设值参数。这里的类型实参会在编译期间被擦除。这个接口只是设计示意，并非现有 Foreign.Storable.sizeOf 的实际签名；Storable 约束所需的字典也属于另一回事。GHC RequiredTypeArguments 文档

对普通参数和结果进行静态限制，有什么理论依据？

如果要求“某个参数或结果只能流向允许擦除的位置，运行时计算不得依赖它”，应查找 computational irrelevance、run-time irrelevance、erasure 这些概念。

例如，Agda 提供 @0 或 @erased 标记，并通过类型检查限制运行时计算对被擦除值的依赖。这与问题中希望检查 unProxy 结果使用位置的设想更接近。Agda Run-time Irrelevance 文档

这类机制需要明确哪些位置允许使用被擦除的值，以及这些限制如何在函数调用和返回值之间传播。GHC 的 RoleAnnotations 不提供这种通用的值级使用限制；RequiredTypeArguments 解决的是显式传入类型的问题，不能直接把已有的任意值参数或返回值变成受检查的 erased value。

备注：内容仅供参考。