Предположим, у меня есть параметр, который существует только для системы типов, например, как в этой маленькой программе:
{-# 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 выполнить стирание доказательства и исключить их?
источник