Idris - 无法在类型中评估函数应用程序

Question

我遇到了一个问题，我有一个类型为 fun a 的值，fun 是一个函数，a 是一个在类型检查时没有计算出来的值，当我抛出一个统一错误时强制它成为该函数应用程序的结果。

具体错误是这样的：

When checking right hand side of testRec2 with expected type
         Record [("A", String), ("C", Nat)]

 Type mismatch between
         Record (projectLeft ["A", "C"]
                             [("A", String),
                              ("B", String),
                              ("C", Nat)]) (Type of hProjectByLabels_comp ["A",
                                                                           "C"]
                                                                          testRec1
                                                                          (getYes (isSet ["A",
                                                                                          "C"])))
 and
         Record [("A", String), ("C", Nat)] (Expected type)

 Specifically:
         Type mismatch between
                 projectLeft ["A", "C"]
                             [("A", String), ("B", String), ("C", Nat)]
         and
                 [("A", String), ("C", Nat)]

这是来自 Idris 中类似 HList 的记录的实现，具有以下示例：

testRec1 : Record [("A", String), ("B", String), ("C", Nat)]
-- testRec1's value is already defined    

testRec2 : Record [("A", String), ("C", Nat)]
testRec2 = hProjectByLabels_comp ["A", "C"] testRec1 (getYes $ isSet ["A", "C"])

...以下类型：

IsSet : List t -> Type

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs)

LabelList : Type -> Type

IsLabelSet : LabelList lty -> Type

HList : LabelList lty -> Type

Record : LabelList lty -> Type

recToHList : Record ts -> HList ts

recLblIsSet : Record ts -> IsLabelSet ts

hListToRec : DecEq lty => {ts : LabelList lty} -> {prf : IsLabelSet ts} -> HList ts -> Record ts

IsProjectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type

IsProjectRight : DecEq lty => List lty -> LabelList lty -> LabelList lty -> Type

hProjectByLabelsHList : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> HList ts -> ((ls1 : LabelList lty ** (HList ls1, IsProjectLeft ls ts ls1)), (ls2 : LabelList lty ** (HList ls2, IsProjectRight ls ts ls2)))

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty

hProjectByLabelsLeftIsSet_Lemma2 : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsLabelSet ts1 -> IsLabelSet ts2

fromIsProjectLeftToComp : DecEq lty => {ls : List lty} -> {ts1, ts2 : LabelList lty} -> IsProjectLeft ls ts1 ts2 -> IsSet ls -> ts2 = projectLeft ls ts1

hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)

...以及以下（必要的）定义：

LabelList : Type -> Type
LabelList lty = List (lty, Type)

IsLabelSet : LabelList lty -> Type
IsLabelSet ts = IsSet (map fst ts) 

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft [] ts = []
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
  projectLeft ls ((l,ty) :: ts) | Yes lIsInLs = 
    let delLFromLs = deleteElem ls lIsInLs
        rest = projectLeft delLFromLs ts
    in (l,ty) :: rest
  projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts

deleteElem : (xs : List t) -> Elem x xs -> List t
deleteElem (x :: xs) Here = xs
deleteElem (x :: xs) (There inThere) =
  let rest = deleteElem xs inThere
  in x :: rest 

getYes : (d : Dec p) -> case d of { No _ => (); Yes _ => p}
getYes (No _ ) = ()
getYes (Yes prf) = prf

hProjectByLabels_comp : DecEq lty => {ts : LabelList lty} -> (ls : List lty) -> Record ts -> IsSet ls -> Record (projectLeft ls ts)
hProjectByLabels_comp {ts} ls rec lsIsSet =
  let 
    isLabelSet = recLblIsSet rec
    hs = recToHList rec
    (lsRes ** (hsRes, prjLeftRes)) = fst $ hProjectByLabelsHList ls hs
    isLabelSetRes = hProjectByLabelsLeftIsSet_Lemma2 prjLeftRes isLabelSet
    resIsProjComp = fromIsProjectLeftToComp prjLeftRes lsIsSet
    recRes = hListToRec {prf=isLabelSetRes} hsRes
  in rewrite (sym resIsProjComp) in recRes

基本上，有一个函数projectLeft 应用于2 个列表并返回一个新列表。 hProjectByLabels_comp 的类型在类型级别应用此函数。 为了实际构建结果列表，我有一个风格为Pred l1 l2 l3 的谓词和一个风格为Pred l1 l2 l3 -> l3 = projectLeft l1 l2 的引理。在hProjectByLabels_comp 中，我将引理应用于谓词并使用rewrite 来获得正确的类型签名（将l3 重写为projectLeft l1 l2 或projectLeft ls ts，这隐含在实现中出现的谓词中在这种特定情况下）。

我希望将hProjectByLabels_comp 应用于记录将正确计算projectLeft ls ts。但是，在上面的示例中，它无法评估/计算projectLeft ["A", "C"] [("A", String), ("B", String), ("C", Nat)]。这看起来很奇怪，因为在 REPL 中评估该函数应用程序给出的正是 [("A", String), ("C", Nat)]，这正是类型所期望的，但 Idris 在类型检查时似乎无法计算此函数。

我不确定某些引理/函数的实现是否与此有关，或者是否仅与类型有关。

我尝试使用更简单的示例（在 Nats 上使用谓词和函数）复制此错误，但该更简单示例的类型检查正确，因此我找不到其他方法来复制此错误。

我正在使用 Idris 0.9.20.2

编辑：我尝试用以下方式重写projectLeft，看看是否有任何变化，但仍然显示相同的错误

projectLeft : DecEq lty => List lty -> LabelList lty -> LabelList lty
projectLeft ls [] = []
projectLeft ls ((l,ty) :: ts) with (isElem l ls)
  projectLeft ls ((l,ty) :: ts) | Yes lIsInLs = 
    let delLFromLs = deleteElem ls lIsInLs
        rest = projectLeft delLFromLs ts
    in (l,ty) :: rest
  projectLeft ls ((l,ty) :: ts) | No _ = projectLeft ls ts

Answer 1

projectLeft 是一个总函数吗？部分函数不会在类型签名中归约，也就是说，您只会看到它们应用于其参数，而不是该应用程序的结果归约。

举例说明：

type : Int -> Type
type 0 = String

a : type 0
a = "Hello"

将无法编译并出现类型错误，抱怨无法将type 0 与String 匹配。尽管为所讨论的值定义了函数type，但 Idris 拒绝在类型签名中应用部分函数。不过，您仍然可以在 repl 中应用它。 type 0 给出String : Type，type 1 给出type 1 : Type（未缩减）。

Answer 2

显然，在更新到 Idris 0.12 后，此问题现已解决。没有改变任何东西，但现在可以进行类型检查。