Haskell依赖类型函数改造：如何将参数从GADTInt替换为Int？

现有一个依赖类型函数dfunc，其返回类型由参数的GADT值决定：GADTZero对应返回Int类型，GADTOne对应返回Integer类型，以此类推，具体映射由类型族Dt定义。当前dfunc的签名为GADTInt a -> Dt a，希望移除GADTInt a这种对整数的编码方式，实现签名为Int -> ?的函数——直接用普通Int作为参数。尝试通过NTI类型类和无类型签名的ff函数让Haskell推导类型时失败，因为ff的实现无法用合法类型签名表达，想知道是否有可行的改造方案。

原代码如下：

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Main where


data Nat :: * where
    Z :: Nat
    S :: Nat -> Nat


data GADTInt a where
    GADTZero :: GADTInt Z
    GADTOne :: GADTInt (S Z)
    GADTTwo :: GADTInt (S (S Z))   
    GADTThree :: GADTInt (S (S (S Z)))   

type family Dt a where
    Dt 'Z = Int
    Dt ('S 'Z) = Integer
    Dt ('S ('S 'Z)) = Float
    Dt ('S ('S ('S 'Z))) = String

class NTI a where
    toi :: a -> Int

instance NTI (GADTInt a) where
    toi GADTZero = 0 
    toi GADTOne = 1 
    toi GADTTwo = 2
    toi GADTThree = 3

dfunc :: GADTInt a -> Dt a
dfunc GADTZero = 1
dfunc GADTOne = 1000000000000000000000000000000
dfunc GADTTwo = 3.14
dfunc GADTThree = "Hi"

ff i 
     | toi GADTZero == i = dfunc GADTZero     
     | toi GADTOne == i = dfunc GADTOne
     | toi GADTTwo == i = dfunc GADTTwo     
     | toi GADTThree == i = dfunc GADTThree
     | otherwise = undefined

核心问题分析 #

Haskell是静态类型语言，函数返回类型必须由输入类型而非输入值决定。普通Int是单一类型，编译器无法从运行时的Int值推导出对应的类型级Nat构造（即a），因此无法直接写出Int -> Dt a这种合法签名——a是多态的，但没有类型约束能将Int值与a关联。

可行解决方案 #

方案1：用存在类型封装异构结果 #

定义存在类型，把不同类型的Dt a值打包在一起，统一返回类型：

{-# LANGUAGE ExistentialQuantification #-}

-- 封装任意Dt a类型的值
data DtResult = forall a. DtResult (Dt a)

ff :: Int -> DtResult
ff 0 = DtResult (dfunc GADTZero)
ff 1 = DtResult (dfunc GADTOne)
ff 2 = DtResult (dfunc GADTTwo)
ff 3 = DtResult (dfunc GADTThree)
ff _ = error "无效的Int值"

后续可以通过定义类型类来处理DtResult中的值，比如：

class ShowDt a where
    showDt :: a -> String

instance ShowDt Int where showDt = show
instance ShowDt Integer where showDt = show
instance ShowDt Float where showDt = show
instance ShowDt String where showDt = id

showResult :: DtResult -> String
showResult (DtResult x) = showDt x

方案2：用GADT明确枚举所有返回类型 #

用GADT列出所有可能的返回类型，比存在类型更直观，后续处理时可直接模式匹配：

data DynDt where
    DynInt :: Int -> DynDt
    DynInteger :: Integer -> DynDt
    DynFloat :: Float -> DynDt
    DynString :: String -> DynDt

ff :: Int -> DynDt
ff 0 = DynInt (dfunc GADTZero)
ff 1 = DynInteger (dfunc GADTOne)
ff 2 = DynFloat (dfunc GADTTwo)
ff 3 = DynString (dfunc GADTThree)
ff _ = error "无效的Int值"

使用时直接匹配构造子：

processDyn :: DynDt -> IO ()
processDyn (DynInt n) = print $ "Int值：" ++ show n
processDyn (DynInteger n) = print $ "Integer值：" ++ show n
processDyn (DynFloat f) = print $ "Float值：" ++ show f
processDyn (DynString s) = print $ "String值：" ++ s

方案3：用类型见证实现安全转换 #

定义一个从Int到GADTInt a的安全转换函数，返回包含类型见证的GADT，仅当Int有效时返回对应Dt a值：

{-# LANGUAGE EmptyCase #-}
import Data.Void

data IntToNat a where
    ValidInt :: GADTInt a -> IntToNat a
    InvalidInt :: IntToNat Void

intToGADT :: Int -> IntToNat a
intToGADT 0 = ValidInt GADTZero
intToGADT 1 = ValidInt GADTOne
intToGADT 2 = ValidInt GADTTwo
intToGADT 3 = ValidInt GADTThree
intToGADT _ = InvalidInt

ff :: Int -> Maybe (Dt a)
ff i = case intToGADT i of
    ValidInt g -> Just (dfunc g)
    InvalidInt -> case invalidInt of {}  -- EmptyCase处理Void类型

这种方式保留了类型关联，但调用时需处理Maybe，且a的类型仍需上下文推导，通常结合存在类型使用。

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