Haskell：从类型系统中将 DataKinds 类型的值获取到函数中

Question

我在 Haskell 中使用 DataKinds，现在我想知道是否可以获得该值 从类型系统返回继续工作。

这是一个例子：

data MyType = Contructor1 | Constructor2 | ...
    deriving (Show)

f :: IO (Proxy (a :: MyType))
f = do
    -- I want 'x' to be of type 'MyType' being the same value as 'a'.
    let x = #### something ####
    print x
    return Proxy

main = do
    -- Print 'Constructor2' into the console.
    f :: IO (Proxy Constructor2)

    -- Print 'Constructor1' into the console.
    f :: IO (Proxy Constructor1)
    return ()

Answer 1

一般来说，将类型级值转换为普通值是不可能的。这是因为 Haskell 允许类型擦除：所有类型信息都会在编译期间被擦除，并且不会在运行时保留下来，至少默认情况下是这样。

为了在运行时保留一些类型级信息，通常会更改手头的类型以包含适当设计的类型类约束。下面，我相应地更改了

f

的类型。

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

import Data.Proxy

data MyType = Constructor1 | Constructor2
    deriving (Show)

class ReifyMyType (a :: MyType) where
   reify :: MyType
instance ReifyMyType 'Constructor1 where
   reify = Constructor1
instance ReifyMyType 'Constructor2 where
   reify = Constructor2

f :: forall a . ReifyMyType a => IO (Proxy (a :: MyType))
f = do
    -- Here we reify @a, turning it into a value x.
    let x = reify @a
    print x
    return Proxy

main = do
    -- Print 'Constructor2' into the console.
    f :: IO (Proxy Constructor2)

    -- Print 'Constructor1' into the console.
    f :: IO (Proxy Constructor1)
    return ()