haskell - 当构造函数静态已知时消除 GADT 上的模式匹配

Question

假设我升级了数据类型:

data GADTConstructor = IntConstructor | StringConstructor

然后我创建 GADT:

data MyGADT (a :: GADTConstructor) where
    MyInt    :: Int -> MyGADT IntConstructor
    MyString :: String -> MyGADT StringConstructor

以及模式匹配功能:

printMyMyGADT :: MyGADT a -> IO ()
printMyMyGADT (MyInt i) = printInteger i
printMyMyGADT (MyString s) = printString s

这里实际的 GADT 构造函数是由编译时已知的 GADT 类型索引唯一确定的。是否可以强制 GHC 在运行时忽略任何模式匹配并假设实际分支是静态已知的来生成代码？

Answer 1

当 GHC 编译 printMyGADT 时，类型索引 a 当然是未知的(它是一个变量)，并且有关 a 的信息不可用在运行时，所以 printMyMyGADT 必须在它传递的构造函数上执行一个分支。

如果你有的话

printMyMyGADT' :: MyGADT IntConstructor -> IO ()
printMyMyGADT' (MyInt i) = printInteger i

然后 GHC 能够将只有 MyInt 构造函数可能的信息传播到生成的代码，并避免构造函数上的分支。

如果您在已知类型变量 a 为 IntConstructor 的上下文中调用原始 printMyGADT，并且如果它是inlined 那么 GHC 会将内联表达式简化为 printMyMyGADT' ，并且分支将再次被避免。我不确定这也可能适用于特化。

所有这些在实践中都有些无关紧要，因为在所有情况下 printMyGADT 都需要处理传递未计算表达式的情况。我们看到两个构造函数中哪一个的分支成本不超过首先检查我们是否已传递构造函数的成本。