如何在Haskell中表达(Type,Value)对及其列表？Idris已有对应写法

嘿，好问题！首先得明确一点：Haskell不像Idris那样支持依赖类型，所以没法直接写出Idris里那种让值完全依赖于类型参数的(Type, Value)对。但别担心，我们可以用Haskell的扩展特性来模拟这种结构，常用的两种方式是存在类型（Existential Types）和广义代数数据类型（GADTs），下面我给你详细拆解：

1. 用存在类型模拟基础的(Type, Value)对 #

首先需要开启ExistentialQuantification扩展，我们可以定义一个包含类型标记和对应值的数据类型：

{-# LANGUAGE ExistentialQuantification #-}
import Data.Proxy  -- 用来做类型标记

data TypeValuePair = forall a. TypeValuePair (Proxy a) a

这里的Proxy a是一个空类型，它唯一的作用就是携带类型a的信息——因为Haskell里不能直接把类型当作值传递，Proxy就是我们的"类型占位符"。

你可以像这样构造具体的对，然后组成列表：

-- 整数对：类型是Int，值是42
intPair :: TypeValuePair
intPair = TypeValuePair Proxy 42

-- 字符串对：类型是String，值是"Hi Haskell"
stringPair :: TypeValuePair
stringPair = TypeValuePair Proxy "Hi Haskell"

-- 不同类型的(Type, Value)对组成的列表
pairList :: [TypeValuePair]
pairList = [intPair, stringPair]

不过这种方式有个小局限：当你从TypeValuePair里取出值时，Haskell不知道它的具体类型，所以需要用类型类约束来操作它。比如我们给它加个Show实例，方便打印：

instance Show TypeValuePair where
  show (TypeValuePair _ val) = show val

现在你就能直接打印pairList，得到["42", "\"Hi Haskell\""]啦。

2. 用GADTs更灵活地定义 #

如果你觉得存在类型的写法有点啰嗦，可以用GADTs（开启GADTs扩展）来实现，写法更直观，还能直接在构造器上添加类型约束：

{-# LANGUAGE GADTs #-}
import Data.Proxy

data TypeValuePair where
  TypeValuePair :: Show a => Proxy a -> a -> TypeValuePair

这样定义后，所有TypeValuePair的实例都自动满足Show约束，不需要再单独写实例了，直接打印列表就行。

3. 结合Typeable获取运行时类型信息 #

如果需要在运行时检查或转换值的类型，可以结合Typeable扩展（需要开启Typeable和ExistentialQuantification）：

{-# LANGUAGE ExistentialQuantification, Typeable #-}
import Data.Typeable

data TypeValuePair = forall a. Typeable a => TypeValuePair a

-- 尝试把值转换成Int
castToInt :: TypeValuePair -> Maybe Int
castToInt (TypeValuePair val) = cast val

这里我们甚至不需要Proxy了，因为Typeable会给我们提供类型的运行时表示，方便做类型安全的转换。

对比Idris的实现 #

最后提一下你熟悉的Idris写法：

data TypeValuePair : Type where
  MkPair : (t : Type) -> t -> TypeValuePair

pairList : List TypeValuePair
pairList = [MkPair Int 42, MkPair String "Hi Idris"]

Idris的依赖类型让它可以直接把Type作为参数，然后让值的类型完全匹配这个参数。而Haskell因为没有依赖类型，只能通过隐藏具体类型的方式模拟这种"类型-值"绑定，核心思路是把不同类型的值统一到一个存在类型下，同时保留必要的操作约束。

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