idris - 使用依赖对时类型检查失败

Question

我写下这个:

data IsTag : String -> Type where
    NumIsTag : IsTag "num"
    StrIsTag : IsTag "str"

arr1 : List (tag : String ** (IsTag tag, (case tag of "num" => Int; "str" => String)))
arr1 = [("num" ** (NumIsTag, 1)), ("str" ** (StrIsTag, "hello"))]

并收到以下使用错误消息:

When checking right hand side of arr1 with expected type
        List (tag : String **
              (IsTag tag, case tag of   "num" => Int "str" => String))

When checking argument b to constructor Builtins.MkPair:
        case "num" of
          "num" => Int
          "str" => String is not a numeric type

但我不明白，为什么 case "num"of "num"=> Int; "str"=> String 不是数字类型？它不等于Int吗？

Answer 1

事实并非如此，因为 Idris 在类型检查期间不会减少部分(非全部)函数。

如果您的字符串不等于 "num"/"str" 时有一个很好的默认类型，那么您可以使用如下所示的内容:

total
tagToType : String -> Type
tagToType "num" = Int
tagToType "str" = String
tagToType _ = ?defaultType

arr1 : List (tag : String ** (IsTag tag, tagToType tag))
arr1 = [("num" ** (NumIsTag, 1)), ("str" ** (StrIsTag, "hello"))]

---

另一种选择是像这样定义它:

total
tagToType : IsTag s -> Type
tagToType NumIsTag = Int
tagToType StrIsTag = String

arr1 : List (tag : String ** istag : IsTag tag ** tagToType istag)
arr1 = [("num" ** NumIsTag ** 1), ("str" ** StrIsTag ** "hello")]