时间戳

首页 > 解决方案 > 评估值相等时发生类型不匹配

functional-programming - 评估值相等时发生类型不匹配

问题描述

我是 Idris 的初学者并试图使代码有效。

你能告诉我关于伊德里斯的菜鸟问题的更好地方吗？

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = filter {len=l} p xs
   in if p x then
        ((FS a) ** x::tail)
      else
        ((weaken a) ** tail)

我写了另一个filter还不能通过类型检查的。

这种新filter的 's 类型意味着过滤后的向量不能长于原始向量。

然而，伊德里斯说

...
Specifically:
                Type mismatch between
                        finToNat a
                and
                        finToNat (weaken a)

我们知道这两个术语总是具有相同的值。

我该如何描述事实并让伊德里斯说好？

标签： functional-programmingidrisdependent-type

解决方案

你必须证明这一点finToNat a = finToNat (weaken a)。tail有 type Vect (finToNat a) elem，但您需要Vect (finToNat (weaken a)) elem最后一行中的第二个组件，因为您weaken a在第一个对组件中编写。

lemma : {n : _} -> (a : Fin n) -> finToNat (weaken a) = finToNat a
lemma FZ     = Refl
lemma (FS x) = rewrite lemma x in Refl

filter : (elem -> Bool) -> Vect len elem -> (p: (Fin len) ** Vect (finToNat p) elem)
filter {len=S l} p xs = ((FZ {k=l}) ** [])
filter {len=S l} p (x::xs) =
  let (a ** tail) = Main.filter {len=l} p xs
  in if p x then
       ((FS a) ** x::tail)
     else
       (weaken a ** (rewrite lemma a in tail))

推荐阅读