2

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

类似问题 1

类似问题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

----这里是错误---- Test.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
4

2 回答 2

6

您收到的错误消息是因为类型参数 toTest需要具有种类TIdx，但具有这种种类的唯一类型是TIand TD。有种类 。_TIdx*

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

由于 GADT 构造函数每个都映射到 kind 的特定 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

这里值得注意的是，在-expression 中case，即使 UnknownTestGADT 已经删除了幻像类型，T1andT2构造函数也向编译器提供了足够的类型信息，以t恢复其确切类型Test TI或 Test TD在 case 表达式的分支内，允许我们例如调用期望这些特定类型的函数。

于 2013-02-17T08:20:14.380 回答
1

您在这里有两个选择。您可以从参数类型中推断出返回值的类型，或者您不能。

在前一种情况下，您可以优化类型：

data Which :: TIdx -> * where
  Fst :: Which TI
  Snd :: Which TD

prob :: Which i -> T1 -> T2 -> Test i
prob Fst x y = x
prob Snd x y = y

在后一种情况下，您必须删除类型信息：

prob :: Bool -> T1 -> T2 -> Either Int Double
prob True (T1 x) y = Left x
prob False x (T2 y) = Right y

您还可以使用存在类型擦除类型信息：

data SomeTest = forall i . SomeTest (Test i)

prob :: Bool -> T1 -> T2 -> SomeTest
prob True x y = SomeTest x
prob False x y = SomeTest y

在这种情况下，您无法使用 的值做任何有趣的事情SomeTest，但在您的真实示例中可能可以。

于 2013-02-17T07:48:49.210 回答