Haskell：如何将DataKinds类型对应的值从类型系统带入函数？

要将DataKinds提升到类型系统的MyType构造器转回可处理的term级值，你需要借助**单例类型（Singleton Types）**建立类型级与term级的关联。以下是两种实现方式：

方式一：手动实现单例关联 #

适合理解底层逻辑，无需额外依赖：

首先启用必要的GHC扩展，然后定义单例类型、类型类及转换函数：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}

data MyType = Constructor1 | Constructor2 deriving (Show)

-- 定义单例类型：每个类型级MyType构造器对应一个term级构造器
data SingMyType (a :: MyType) where
  SingConstructor1 :: SingMyType 'Constructor1
  SingConstructor2 :: SingMyType 'Constructor2

-- 类型类：用于获取对应类型的单例值
class SingMyTypeI (a :: MyType) where
  singMyType :: SingMyType a

-- 为每个MyType构造器实现实例
instance SingMyTypeI 'Constructor1 where
  singMyType = SingConstructor1

instance SingMyTypeI 'Constructor2 where
  singMyType = SingConstructor2

-- 将单例值转回MyType类型的普通值
fromSingMyType :: SingMyType a -> MyType
fromSingMyType SingConstructor1 = Constructor1
fromSingMyType SingConstructor2 = Constructor2

修改你的f函数，添加SingMyTypeI a约束以获取单例值：

import Data.Proxy

f :: forall a. SingMyTypeI a => IO (Proxy (a :: MyType))
f = do
  let x = fromSingMyType (singMyType @a)
  print x
  return Proxy

调用时通过TypeApplications显式指定类型参数：

main :: IO ()
main = do
  f @'Constructor2  -- 控制台输出 Constructor2
  f @'Constructor1  -- 控制台输出 Constructor1

方式二：使用singletons库自动生成（推荐） #

singletons库可以自动生成单例相关代码，避免手动重复劳动：

1. 首先在cabal文件中添加依赖：build-depends: base >= 4.14 && < 5, singletons >= 3.0
2. 编写代码：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Singletons #-}

import Data.Singletons.TH
import Data.Proxy

-- 用模板自动生成单例类型、SingI实例及转换函数
$(singletons [d|
  data MyType = Constructor1 | Constructor2 deriving (Show)
  |])

f :: forall a. SingI a => IO (Proxy (a :: MyType))
f = do
  let x = fromSing (sing @a)
  print x
  return Proxy

main :: IO ()
main = do
  f @'Constructor2
  f @'Constructor1

关键说明 #

• 必须添加SingMyTypeI（手动）或SingI（singletons库）约束：GHC需要明确的规则才能从类型级值映射到term级值，没有约束的话无法自动推导。
• TypeApplications扩展用于显式指定类型参数，让GHC知道你要处理的是哪个类型级构造器。

内容的提问来源于stack exchange，提问作者user20488048