haskell - 现代 GHC 版本是否有任何类型的证明删除？

Question

假设我有一个仅为类型系统的利益而存在的参数，例如在这个小程序中:

{-# LANGUAGE GADTs #-}
module Main where
import Data.Proxy
import Data.List

data MyPoly where
  MyConstr :: Proxy a -> a -> (Proxy a -> a -> Int -> Int) -> MyPoly

listOfPolys :: [MyPoly]
listOfPolys = [MyConstr Proxy 5 (const (+))
              , MyConstr Proxy 10 (const (+))
              , MyConstr Proxy 15 (const (+))]

main = print $ foldl' (\v (MyConstr p n a) -> a p n v) 0 listOfPolys

结构中的 Proxy 参数和成员只需要在编译时存在，以帮助进行类型检查，同时维护多态 MyPoly(在这种情况下，程序将在没有它的情况下编译，但这个人为的示例是一个更普遍的问题，其中存在仅在编译时需要的证明或代理)- Proxy 只有一个构造函数，并且类型参数是幻像类型。

使用 ghc 编译 -ddump-stg表明至少在 STG 阶段，没有删除构造函数的 Proxy 参数或构造函数的第三个参数。

有没有办法将这些标记为仅编译时，或者以其他方式帮助 ghc 进行证明删除并排除它们？

Answer 1

实际上，您的代码确实会导致 Proxy s 存储在构造函数中:

ProxyOpt.listOfPolys8 :: ProxyOpt.MyPoly
[GblId, Caf=NoCafRefs, Unf=OtherCon []] =
    CCS_DONT_CARE ProxyOpt.MyConstr! [Data.Proxy.Proxy
                                      ProxyOpt.listOfPolys9
                                      ProxyOpt.listOfPolys4];

然而，通过一个小的改变，我们得到了想要的优化。没有了 Proxy !

ProxyOpt.listOfPolys8 :: ProxyOpt.MyPoly
[GblId, Caf=NoCafRefs, Unf=OtherCon []] =
    CCS_DONT_CARE ProxyOpt.MyConstr! [ProxyOpt.listOfPolys9
                                      ProxyOpt.listOfPolys4];

我做了什么？我做了 Proxy字段严格:

data MyPoly where
  MyConstr :: !(Proxy a) -> a -> (Proxy a -> a -> Int -> Int) -> MyPoly
           -- ^ --

一般来说，我们不能因为底部而删除非严格代理。 Proxy和 undefined都是 Proxy a 类型但它们在观察上并不等价，因此我们必须在运行时区分它们。

相反，一个严格的 Proxy只有一个值，所以 GHC 可以优化它。

但是，没有类似的功能可以优化(非构造函数)函数参数。您的领域 (Proxy a -> a -> Int -> Int)将需要 Proxy在运行时。