DataKinds遇到问题 [英] Trouble with DataKinds

问题描述

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

类似问题1

类似的问题2

  { - ＃LANGUAGE GADTs，DataKinds，FlexibleInstances，KindSignatures＃ - } 
 
模块测试其中
 
数据TIdx = TI | TD 
 
 data Test :: TIdx  - > *其中
 T1 :: Int  - >测试TI 
 T2 :: Double  - >测试TD 
 
类型T1 =测试TI 
类型T2 =测试TD 
 
 prob :: T1  - > T2  - > Test TIdx 
 prob xy = undefined 
  

----这是错误--- -
Test.hs：14：26：

 种类不符
 
 `Test'的第一个参数应该有`TIdx'，
 
，但`TIdx'有`*'
 
在`prob'类型签名中：prob :: T1  - > T2  - > Test TIdx 
  

解决方案

参数到 Test 需要
的类型为 TIdx ，但唯一具有该类型的类型是 TI 和 TD 。
类型 TIdx 具有类型 * 。

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

你可以做什么，因为GADT构造函数都映射到特定的ptyom类型 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其中
 UnknownTest :: Test t  - > UnknownTest 
 
 prob :: T1  - > T2  - > UnknownTest 
 prob xy = undefined 
 $ b $ main main :: IO（）
 main = do 
 let a = T1 5 
b = T2 10.0 
p = prob ab 
 
 case p of 
 UnknownTest t @（T1 _） - > fun1 t 
 UnknownTest t @（T2 _） - > fun2 t 
  

值得注意的是，在 case UnknownTest GADT已经擦除了幻像类型， T1 和 T2 构造函数给编译器足够的
类型信息， t 恢复它的确切类型在case-expression的分支中测试TI 或
测试TD ，从而允许我们例如调用期望这些特定类型的
函数。

I have created a very simple example of a problem I'm having using GADTs and DataKinds. My real application is obviously more complicated but this captures the essence of my situation clearly. I'm trying to create a function that can return any of the values (T1, T2) of type Test. Is there a way to accomplish this or am I getting into the realm of dependent types? The questions here seem similar but I could not find (or comprehend) an answer to my question from them. I'm just starting to understand these GHC extensions. Thanks.

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

----Here is the error---- 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

解决方案

The error message you get is because the type parameter to Test needs to have the kind TIdx, but the only types that have that kind are TI and TD. The type TIdx has the kind *.

If I understood correctly what you are trying to express is that the result type of prob is either Test TI or Test TD, but the actual type is determined at runtime. However, this won't work directly. The return type generally has to be known at compile time.

What you can do, since the GADT constructors each map to specific phatom type of kind TIdx, is to return a result that erases the phantom type with an existential or another GADT and then recover the type later using a pattern match.

For example, if we define two functions that require a specific kind of Test:

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

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

This type-checks:

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

The notable thing here is that in the case-expression, even though the UnknownTest GADT has erased the phantom type, the T1 and T2 constructors give enough type information to the compiler that t recovers its exact type Test TI or Test TD within the branch of the case-expression, allowing us to e.g. call functions that expect those specific types.

这篇关于DataKinds遇到问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！