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 个列表和 returns 一个新列表。 hProjectByLabels_comp 的类型在类型级别应用此功能。为了实际构造结果列表，我有一个样式为 Pred l1 l2 l3 的谓词和一个样式为 Pred l1 l2 l3 -> l3 = projectLeft l1 l2 的引理。在 hProjectByLabels_comp 中，我将引理应用于谓词并使用 rewrite 获得正确的类型签名（将 l3 重写为 l3，它隐含在出现在实现内部的谓词中25=]，或在此特定情况下为 projectLeft ls ts）。

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

我不确定某些 lemmas/functions 的实现是否与此有关，或者是否仅与类型有关。

我尝试使用一个更简单的示例（使用 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 后已经解决了。没有改变任何东西，但它现在进行类型检查。

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

Idris - Can't evaluate function application in type

unification

type-level-computation