现代 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 进行证明擦除并排除它们？

Answer 1

确实，您的代码确实导致Proxys 被存储在构造函数中：

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。

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

现在，我们有一些工具可以在没有 Proxy 的情况下更轻松地工作：例如，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"