如何为处理不同索引TimedWord类型的Haskell函数标注类型？

针对你遇到的TimedWord无法同时接受两种索引类型的问题，这里提供几种实用的修正方案：

方案1：使用类型类（Typeclass） #

通过为不同的TWEnd索引定义类型类实例，让函数自动适配不同的索引类型：

{-# LANGUAGE DataKinds, GADTs, PatternSynonyms, FlexibleInstances #-}

data TWEnd = TWESample | TWETime

data TimedWord end where
  TWSample :: Bool -> TimedWord 'TWETime -> TimedWord 'TWESample
  TWTime :: Double -> TimedWord 'TWESample -> TimedWord 'TWETime
  TWEmpty :: TimedWord 'TWESample

-- 定义类型类，声明打印方法
class PrintableTimedWord end where
  printTimedWord :: TimedWord end -> String

-- 为结束于Sample的TimedWord实现实例
instance PrintableTimedWord 'TWESample where
  printTimedWord TWEmpty = "[]"
  printTimedWord (TWSample b rest) = "Sample " ++ show b ++ ", " ++ printTimedWord rest

-- 为结束于Time的TimedWord实现实例
instance PrintableTimedWord 'TWETime where
  printTimedWord (TWTime d rest) = "Time " ++ show d ++ ", " ++ printTimedWord rest

调用时，Haskell会根据TimedWord的具体索引自动选择对应的实例，完美适配两种类型。

方案2：使用存在类型（Existential Type） #

如果需要将不同索引的TimedWord放在同一容器（比如列表）中，或者不想编写类型类，可以用存在类型抹去索引信息：

{-# LANGUAGE DataKinds, GADTs, PatternSynonyms, ExistentialQuantification #-}

data TWEnd = TWESample | TWETime

data TimedWord end where
  TWSample :: Bool -> TimedWord 'TWETime -> TimedWord 'TWESample
  TWTime :: Double -> TimedWord 'TWESample -> TimedWord 'TWETime
  TWEmpty :: TimedWord 'TWESample

-- 定义存在类型，打包任意索引的TimedWord
data AnyTimedWord = forall end. AnyTimedWord (TimedWord end)

-- 针对打包后的类型编写打印函数
printAnyTimedWord :: AnyTimedWord -> String
printAnyTimedWord (AnyTimedWord TWEmpty) = "[]"
printAnyTimedWord (AnyTimedWord (TWSample b rest)) = "Sample " ++ show b ++ ", " ++ printAnyTimedWord (AnyTimedWord rest)
printAnyTimedWord (AnyTimedWord (TWTime d rest)) = "Time " ++ show d ++ ", " ++ printAnyTimedWord (AnyTimedWord rest)

使用时只需将TimedWord包装成AnyTimedWord即可统一处理。

方案3：使用约束统一索引类型 #

通过定义约束限定索引只能是TWESample或TWETime，让函数接受符合约束的任意索引：

{-# LANGUAGE DataKinds, GADTs, PatternSynonyms, ConstraintKinds, TypeFamilies, FlexibleContexts #-}

import Data.Type.Bool

data TWEnd = TWESample | TWETime

-- 定义约束：end必须是两种索引之一
type IsValidTWEnd end = (end == 'TWESample) || (end == 'TWETime)

data TimedWord end where
  TWSample :: Bool -> TimedWord 'TWETime -> TimedWord 'TWESample
  TWTime :: Double -> TimedWord 'TWESample -> TimedWord 'TWETime
  TWEmpty :: TimedWord 'TWESample

-- 用约束限定函数参数的索引类型
printTimedWord :: IsValidTWEnd end => TimedWord end -> String
printTimedWord TWEmpty = "[]"
printTimedWord (TWSample b rest) = "Sample " ++ show b ++ ", " ++ printTimedWord rest
printTimedWord (TWTime d rest) = "Time " ++ show d ++ ", " ++ printTimedWord rest

为什么原写法会报错？ #

GADT的索引与构造器强绑定，每个构造器返回的TimedWord索引是固定的。当你尝试写TimedWord end -> String时，Haskell期望end是单一固定类型，但递归调用时，rest的索引是另一种（比如TWSample的rest是TWETime，而当前函数的end是TWESample），导致类型不匹配。上述方案通过类型类、存在类型或约束，解决了这种索引不统一的问题。

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