У современных версий GH C есть какое-либо доказательство удаления?

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 в структуре действительно должны существовать только в время компиляции, чтобы помочь с проверкой типов при поддержке polymorphi c MyPoly (в этом случае программа будет компилироваться без него, но этот надуманный пример является более общей проблемой, когда существуют доказательства или прокси, которые необходимы только во время компиляции) - есть только один конструктор для Прокси, и аргумент типа является фантомным типом.

Компиляция с gh c с -ddump-stg показывает, что, по крайней мере, на этапе STG, стирание Прокси не происходит аргумент для конструктора или третий аргумент для конструктора.

Есть ли способ пометить их как только время компиляции, или иным образом помочь gh c выполнить стирание доказательства и исключить их?

Answer 1

Действительно, ваш код приводит к сохранению Proxy s в конструкторе:

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, но они не являются обсервационно эквивалентными, поэтому мы должны различать guish их во время выполнения.

Вместо этого строгий Proxy имеет только одно значение, поэтому GH C может его оптимизировать.

Нет аналогичной функции для оптимизации (неконструктивного) параметра функции, хоть. Ваше поле (Proxy a -> a -> Int -> Int) потребует Proxy во время выполнения.

Answer 2

Есть два способа выполнить sh то, что вы хотите.

Несколько более старый способ - использовать Proxy # из GH C .Prim, который гарантированно будет стерто во время компиляции.

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

Хотя это немного громоздко.

Другой способ заключается в go 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"