如何用Haskell DataKinds实现类似Kotlin的函数类型约束？

问题原因解析 #

你原来的代码编译错误，核心是混淆了Haskell中类型、种类以及DataKinds提升后的实体概念：

• 启用DataKinds后，你的Format数据类型会被提升为一个种类（Kind），而构造器Photo、Video会被提升为类型级构造器：'Photo的种类是Int -> Format，'Video的种类是Int -> Int -> Format。
• 你试图让函数返回'Video，但'Video是一个类型级构造器（不是值的类型，值的类型属于Type种类），编译器自然会报错。
• Haskell本身没有子类型系统，Kotlin中Format.Video作为Format子类型的行为，需要用GADTs（广义代数数据类型）结合DataKinds来模拟。

正确实现方案 #

我们可以用GADTs定义带类型标记的Format，同时保留记录语法，实现编译时的类型限定：

步骤1：启用必要扩展 #

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

步骤2：定义类型级标记与GADT #

先定义一个用来标记不同格式的类型（会被DataKinds提升为种类），再用GADT绑定类型标记与具体的格式构造器：

-- 类型级标记，区分照片和视频
data FormatTag = PhotoTag | VideoTag

-- GADT：不同的FormatTag对应不同的具体类型
data Format (tag :: FormatTag) where
  Photo :: { bytes :: Int } -> Format 'PhotoTag
  Video :: { bytes :: Int, durationSec :: Int } -> Format 'VideoTag

步骤3：实现类型限定的构造函数 #

现在createVideo可以明确返回Format 'VideoTag类型，编译时会严格检查类型匹配：

createVideo :: Int -> Int -> Format 'VideoTag
createVideo bytes durationSec = Video{..}

步骤4：模拟Kotlin的“父类型”行为 #

如果需要像Kotlin中把Format.Video赋值给Format类型的变量，可以定义一个存在类型来包装任意标记的Format：

-- 存在类型：包装任意FormatTag的Format
data SomeFormat where
  SomeFormat :: Format tag -> SomeFormat

这样就可以实现和Kotlin示例完全一致的编译时行为：

-- 正确：Video可以被包装为通用的SomeFormat
video :: SomeFormat
video = SomeFormat (createVideo 0 0)

-- 正确：明确指定类型为Video
video2 :: Format 'VideoTag
video2 = createVideo 0 0

-- 编译错误：类型不匹配，无法将Video赋值给Photo类型
-- video3 :: Format 'PhotoTag
-- video3 = createVideo 0 0

关键差异说明 #

• Kotlin靠子类型系统实现类型限定，而Haskell靠GADTs的类型索引实现编译时的类型区分。
• DataKinds的作用是把普通数据类型提升为种类，让我们可以用类型级别的标记来区分不同的Format变体。

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