将任意数据类型指定为(编译时已知)值

Question

我希望能够编写以下内容：

reify (Proxy @True)) == True;
reify (Proxy @(Just 5)) == Just 5;

是否可以通过一揽子实施？我已到达

class Reify (a :: k) where
reify :: Proxy a -> k

除了手工编写每个实例之外，我不知道如何编写：一个实例为True，一个实例为False，等等。我不想全部手工编写，也不想使用模板haskell为我编写。我可以只有一个实例来完成吗？

或者可能还有其他方法？对我来说，用例是能够写：

type DeriveHelper :: Settings -> Type -> Type
newtype DeriveHelper s a = DeriveHelper a
instance (Generic a, GMyClass (Rep a)) => MyClass (DeriveHelper s a) where
myMethod (DeriveHelper x) = genericMyMethod (reify (Proxy @s)) $ from x
-- and then
data FooBar ...
deriving MyClass via DeriveHelper SomeSettings FooBar

至于我在世界上看到的这样做的图书馆，它们似乎都有小的设置，我相信这些设置是手工具体化的。

Answer 1

如果我没有注意到目前最好的解决方案仍然是singletons包，它提供了demote函数来执行您想要的操作，那我就太失职了(请参阅最后的示例(。但是，该实现在内部使用TemplateHaskell来提升现有的Prelude类型，并要求您显式使用TH来提升其他类型。而且，你说你不想那样做。。。

所以，我想这在技术上是可能的泛型。您可以使用Data.Typeable或Type.Reflection来销毁类型为k的类型级t，然后使用GHC.Generics(或Data.Data或其他(构造类型为k的项t。

考虑以下概念证明，其中使用Data.Typeable进行类型销毁，使用Data.Data进行术语构建：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Reify where
import Data.Typeable
import Data.Data
demote :: forall k t. (Typeable t, Data k) => Proxy (t :: k) -> k
demote pxy
= let rep = typeRep pxy
in  fromConstr $ mkConstr (dataTypeOf @k undefined)
(removeTick $ tyConName . typeRepTyCon $ rep)
[]
Prefix
where removeTick (''':xs) = xs

这只是部分实现，但它将降级任意空前缀构造函数：

data MyType = A | B Int deriving (Show, Data)
main = do
print $ (demote (Proxy @'Nothing) :: Maybe Int)
print $ (demote (Proxy @'False) :: Bool)
print $ (demote (Proxy @'A) :: MyType)

我认为将其推广到处理任意arity的构造函数和添加对Int#等的支持没有任何技术障碍。

也许有人在某个地方的包中实现了这一点，但我不知道在哪里。

无论如何，使用TH的singletons解决方案已经准备好运行，看起来像：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Reify where
import Data.Singletons
import Data.Singletons.TH
import Data.Kind
import GHC.Generics
import GHC.Natural
-- define a new type supporting "demote"
$(singletons [d|
data MyType = A | B Bool deriving (Show)
|])
-- add "demote" support to an existing type (e.g., imported from a library)
data LibraryType = C | D Bool deriving (Show)
$(genSingletons [''LibraryType])
main = do
print $ (demote @('Just 5) :: Maybe Natural)
print $ (demote @'False :: Bool)
print $ (demote @'A :: MyType)
print $ (demote @('D 'False) :: LibraryType)