现代 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 with 编译-ddump-stg显示，至少在 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"