haskell - 数据种类的问题

Question

我创建了一个非常简单的示例，说明我在使用 GADT 和 DataKinds 时遇到的问题。我的实际应用程序显然更复杂，但这清楚地捕获了我的情况的本质。我正在尝试创建一个可以返回任何类型为 Test 的值(T1，T2)的函数。有没有办法做到这一点，或者我正在进入依赖类型的领域？这里的问题看起来很相似，但我无法从他们那里找到(或理解)我的问题的答案。我刚刚开始了解这些 GHC 扩展。谢谢。

similar question 1

similar question 2

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

module Test where

data TIdx = TI | TD

data Test :: TIdx -> * where
  T1 :: Int -> Test TI
  T2 :: Double -> Test TD

type T1 = Test TI
type T2 = Test TD

prob :: T1 -> T2 -> Test TIdx
prob x y = undefined

----这里是错误----
测试.hs:14:26:

Kind mis-match

The first argument of `Test' should have kind `TIdx',

but `TIdx' has kind `*'

In the type signature for `prob': prob :: T1 -> T2 -> Test TIdx

Answer 1

您收到的错误消息是因为类型参数为 Test需要
有种TIdx ，但唯一具有这种类型的类型是 TI和 TD .
类型TIdx有种* .

如果我理解正确你想要表达的是结果prob 的类型是 Test TI或 Test TD ，但实际类型是
在运行时确定。但是，这不会直接起作用。返回类型
通常必须在编译时知道。

你可以做什么，因为 GADT 构造函数每个都映射到特定的 phatom 类型 TIdx , 是返回一个结果，该结果用
存在或其他 GADT，然后稍后使用模式恢复类型
匹配。

例如，如果我们定义了两个需要特定类型 Test 的函数。 :

fun1 :: T1 -> IO ()
fun1 (T1 i) = putStrLn $ "T1 " ++ show i

fun2 :: T2 -> IO ()
fun2 (T2 d) = putStrLn $ "T2 " ++ show d

这种类型检查:

data UnknownTest where
    UnknownTest :: Test t -> UnknownTest

prob :: T1 -> T2 -> UnknownTest
prob x y = undefined

main :: IO ()
main = do
    let a = T1 5
        b = T2 10.0
        p = prob a b

    case p of
        UnknownTest t@(T1 _) -> fun1 t
        UnknownTest t@(T2 _) -> fun2 t

这里值得注意的是，在 case -表达式，即使 UnknownTest GADT 已删除幻像类型， T1和 T2构造函数提供足够的
向编译器键入 t 的信息恢复其确切类型 Test TI或者 Test TD在 case-expression 的分支中，允许我们例如称呼
期望这些特定类型的函数。