如何在Haskell中实现Kotlin风格的不变类型？

在Kotlin中可以编写如下代码：

sealed class Substance {
    object Uranus : Substance()
    object Mercury: Substance()
    object Ammonia : Substance()
}

data class DangerousBox<T : Substance>(val item: T)

fun main() {
    val uranus = DangerousBox<Substance.Uranus>(Substance.Uranus)
    val mercury: DangerousBox<Substance.Mercury> = uranus
}

由于DangerousBox<Substance.Uranus>、DangerousBox<Substance.Mercury>是不变类型，上述代码无法编译，这正是预期效果。

我希望在Haskell中实现完全相同的效果：定义类似下面的代码时，编译器能拒绝编译：

uranus :: DangerousBox Uranus
uranus = DangerousBox Mercury

我尝试了两种实现方式，但都存在问题：

1. 模块化约束实现 #

我编写了如下模块：

module Sample.Types.Boxes
  ( Substance(..)
  , dangerousBox
  , VDangerousBox {- no Con-}
  ) where

data Substance
  = Uranus
  | Mercury
  | Ammonia
  deriving (Show)

data VDangerousBox a =
  VDangerousBox Substance
  deriving (Show)

dangerousBox :: Substance -> VDangerousBox Substance
dangerousBox a = VDangerousBox a

模块使用者只能通过dangerousBox构造实例，但得到的类型是VDangerousBox Substance，无法区分具体的物质类型，达不到类型不变的约束效果。

2. Data Kinds实现 #

data DangerousBox :: Substance -> * where
  DangerousBox :: Substance -> DangerousBox a

uranus :: DangerousBox Uranus
uranus = DangerousBox Uranus

mercury :: DangerousBox Mercury
mercury = uranus {- 这段代码无法编译，符合预期 -}

但下面这段不符合预期的代码却能通过编译：

mercury :: DangerousBox Mercury
mercury = DangerousBox Ammonia

这相当于Kotlin中data Box<T : Substance>(val value: Substance)的泛型实现，没有把类型参数T和实际存储的Substance值绑定起来。

这是学术研究需求，请问如何在Haskell中正确实现目标效果？

要实现Kotlin中那种“DangerousBox<T>的类型参数T必须和内部存储的具体物质实例严格对应”的不变类型效果，你需要用**GADTs（广义代数数据类型）**结合Data Kinds，把类型参数和构造器的参数值做强绑定。

正确实现代码 #

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

-- 定义物质类型，启用DataKinds后会自动提升为类型级别的符号
data Substance = Uranus | Mercury | Ammonia deriving (Show)

-- 定义DangerousBox的GADT，构造器的参数值必须和类型参数匹配
data DangerousBox :: Substance -> * where
  UranusBox :: DangerousBox 'Uranus
  MercuryBox :: DangerousBox 'Mercury
  AmmoniaBox :: DangerousBox 'Ammonia

-- 如果需要保留类似Kotlin中"包装具体实例"的语义，可以调整为：
-- data DangerousBox :: Substance -> * where
--   DangerousBox :: (s ~ 'Uranus) => Substance -> DangerousBox s
--   DangerousBox :: (s ~ 'Mercury) => Substance -> DangerousBox s
--   DangerousBox :: (s ~ 'Ammonia) => Substance -> DangerousBox s
-- 但更简洁的方式是直接用对应类型的构造器，避免传入错误值

效果验证 #

• 符合预期的正确代码可以编译：

uranus :: DangerousBox 'Uranus
uranus = UranusBox

• 尝试把UranusBox赋值给DangerousBox 'Mercury类型的变量，编译器会报错：

mercury :: DangerousBox 'Mercury
mercury = uranus -- 编译错误：无法将DangerousBox 'Uranus转换为DangerousBox 'Mercury

• 尝试用错误的物质值构造对应类型的DangerousBox（如果用带参数的构造器版本），编译器也会报错：

mercury :: DangerousBox 'Mercury
mercury = DangerousBox Uranus -- 编译错误：无法满足s ~ 'Mercury的约束

原理说明 #

通过GADTs，我们让DangerousBox的每个构造器只能对应唯一的类型参数：

• UranusBox只能构造DangerousBox 'Uranus类型的值
• MercuryBox只能构造DangerousBox 'Mercury类型的值
  这样就完全模拟了Kotlin中DangerousBox<T>的不变性：不同T对应的DangerousBox类型完全不兼容，且内部存储的实例和类型参数严格绑定。

如果需要保留“包装Substance实例”的语义，可以用带类型相等约束（~）的GADT构造器，强制传入的Substance值必须和类型参数一致，这样编译器会拒绝传入不匹配的值。

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