¿Las versiones modernas de GHC tienen algún tipo de borrado de prueba?

Supongamos que tengo un parámetro que existe solo para el beneficio del sistema de tipos, por ejemplo, como en este pequeño programa:

{-# 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

Los argumentos y miembros de Proxy en la estructura solo necesitan existir en tiempo de compilación para ayudar con la verificación de tipos mientras se mantiene el MyPoly polimórfico (en este caso, el programa se compilará sin él, pero este ejemplo artificial es un problema más general donde hay pruebas o proxies que solo se necesitan en tiempo de compilación): solo hay un constructor para Proxy, y el argumento type es un tipo fantasma.

Compilar con ghc con -ddump-stgmuestra que, al menos en la etapa STG, no hay borrado del argumento Proxy para el constructor o el tercer argumento para el constructor.

¿Hay alguna manera de marcarlos como solo en tiempo de compilación, o de lo contrario ayudar a ghc a borrar la prueba y excluirlos?

De hecho, su código lleva a que Proxys se almacene en el constructor:

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

Sin embargo, con un pequeño cambio, obtenemos la optimización deseada. No mas Proxy!

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

Que hice Hice el Proxycampo estricto :

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

En general, no podemos borrar proxies no estrictos debido a los fondos. Proxyy undefinedson de tipo, Proxy apero no son observacionalmente equivalentes, por lo que debemos distinguirlos en tiempo de ejecución.

En cambio, un estricto Proxysolo tiene un valor, por lo que GHC puede optimizarlo.

Sin embargo, no hay una característica similar para optimizar un parámetro de función (no constructor). Su campo (Proxy a -> a -> Int -> Int)requerirá un Proxytiempo de ejecución.

Hay dos formas de lograr lo que quieres.

La forma un poco más antigua es usar Proxy # de GHC.Prim, que se garantiza que se borrará en tiempo de compilación.

{-# 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 (\_ -> (+))]

Aunque esto es un poco engorroso.

La otra forma es renunciar por Proxycompleto:

{-# 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

Hoy en día, tenemos algunas herramientas que facilitan el trabajo sin Proxy: extensiones como AllowAmbiguousTypesy TypeApplications, por ejemplo, significan que puede aplicar el tipo que quiere decir directamente. No sé cuál es su caso de uso, pero tome este ejemplo (artificial):

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"

Queremos leer y luego mostrar un valor de algún tipo, por lo que necesitamos una forma de indicar cuál es el tipo real. Así es como lo haría con extensiones:

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

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

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