现代的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

这个结构中的代理参数和成员只需要在编译时存在，以帮助类型检查并维护多态的 MyPoly（在这种情况下，该程序将在没有它的情况下编译，但这个假想的示例是一个更一般的问题，其中有些证明或代理仅在编译时需要）- Proxy 只有一个构造函数，类型参数是一个虚拟类型。

使用 -ddump-stg 编译 ghc 显示，在 STG 阶段至少不会对构造函数的 Proxy 参数或第三个参数进行消除。

是否有任何方法可以将它们标记为仅在编译时使用，或者以其他方式帮助 ghc 进行证明擦除并将它们排除？

- a1kmm

Answer 1

事实上，你的代码确实会导致在构造函数中存储Proxy：

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
           -- ^ --

通常情况下，由于底部(bottoms)的存在，我们无法擦除非严格(Non-strict)的代理(proxy)。 Proxy 和 undefined 都属于类型 Proxy a，但它们在运行时不是观察上等价的，因此我们必须在运行时加以区分。

相反，严格(strict)的 Proxy 只有一个值，因此 GHC 可以优化掉它。

然而，并没有类似的功能来优化掉（非构造函数）的函数参数。你的字段 (Proxy a -> a -> Int -> Int) 在运行时将需要一个 Proxy。

- chi

Answer 2

有两种方法可以实现你想要的。

稍微旧一点的方法是使用GHC.Prim中的Proxy#，该方法保证在编译时被擦除。

{-# LANGUAGE GADTs, MagicHash #-}
module Main where

import Data.List
import GHC.Prim

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

listOfPolys :: [MyPoly]
listOfPolys = [MyConstr proxy# 5 (\_ -> (+))
              , MyConstr proxy# 10 (\_ -> (+))
              , MyConstr proxy# 15 (\_ -> (+))]

尽管这有点繁琐。

另一种方法是完全放弃Proxy：

{-# LANGUAGE GADTs #-}

module Main where

import Data.List

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

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

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

现在，我们有一些工具可以使无需代理更容易工作：例如，像 AllowAmbiguousTypes 和 TypeApplications这样的扩展意味着你可以直接应用你想要的类型。我不知道你的使用情况是什么，但是以这个（刻意构造的）例子为例：

import Data.Proxy

asTypeP :: a -> Proxy a -> a
asTypeP x _ = x

readShow :: (Read a, Show a) => Proxy a -> String -> String
readShow p x = show (read x `asTypeP` p)

>>> readShow (Proxy :: Proxy Int) "01"
"1"

我们希望读取并显示一些类型的值，因此需要一种指示实际类型的方式。下面是使用扩展的示例：

{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables #-}

readShow :: forall a. (Read a, Show a) => String -> String
readShow x = show (read x :: a)

>>> readShow @Int "01"
"1"

- oisdk

---

在我看来，最后一个选择（无代理）是最好的。 - chi

这是我博客文章的无耻宣传，其中详细记录了上述技巧：https://www.haskellforall.com/2021/04/how-to-replace-proxy-with.html - Gabriella Gonzalez