DataKinds的麻烦

Question

我创建了一个使用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

Answer 1

您得到的错误消息是因为type参数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-expression,即使 UnknownTestGADT已删除的幻象类型,T1和T2建设者提供足够的类型信息,编译器t恢复它的确切类型Test TI或 Test TD案件表达的分支内,使我们能够如调用期望这些特定类型的函数.