如何编写接受长度小于 3 的 Vector 的 Idris 函数

Question

伊德里斯 1.2.0。我试图自动找到向量长度小于3的证明。

f : {n : Nat} -> {auto prf: n < 3 = True} -> Vect n a -> ()
f v = ()

f' : {n : Nat} -> {auto prf: isJust (natToFin n 3) = True} -> Vect n a -> ()
f' v = ()

这两个类型检查，并与 f {n=2} [1, 2} 甚至 f (the (Vect 2 Nat) [1, 2]) 一起工作，但是当我像 f [1, 2] 这样称呼它时，我得到

When checking argument x to constructor Data.Vect.:::
    No such variable len

我也试过另一种方法：

g : {x : Fin 3} -> Vect (finToNat x) a -> ()
g v = ()

这也适用于 g {x=2} [1, 2]，但再次失败 g [1, 2]

When checking an application of function Main.g:
    Type mismatch between
            Vect 2 Integer (Type of [1, 2])
    and
            Vect (finToNat x) Integer (Expected type)

    Specifically:
            Type mismatch between
                    2
            and
                    finToNat x

好吧，我想当 x 未知时，这两个表达式不会简化为相同的规范形式。

我不明白第一个错误。我怀疑它与 [] 语法重载有关。我做错了什么？

Answer 1

Idris 在尝试解决合一问题 finToNat x = 2 时不会尝试反转（单射）函数 finToNat 来猜测 x 的值。所以它只是卡住了。

在更一般的层面上，而不是在类型中推动计算或在隐式参数中进行证明搜索，我将通过以下任一方式表示有界向量：

record BoundedVec (n : Nat) (a : Type) where
  size : Nat
  less : LTE size n
  vect : Vect size a

或者，关注Agda's standard library

data BoundedVec : (n : Nat) -> (a : Type) -> Type where
  Nil  : BoundedVec n a
  Cons : a -> BoundedVec n a -> BoundedVec (S n) a

Answer 2

感谢 gallais 提供的见解。这是一个完整的例子：

-- idris -p contrib

import Data.BoundedList
import Data.Vect

-- a function that takes a list of at most 3 elements
f : BoundedList 3 a -> ()
f xs = ()

-- a shorter vector
v : Vect 2 Int
v = [1, 2]

-- convert the vector to a bounded list and weaken the bound
bounded : BoundedList 3 Int
bounded = weaken $ fromList $ toList v

-- call the function
answer : ()
answer = f bounded

如何编写接受长度小于 3 的 Vector 的 Idris 函数

How to write an Idris function that accepts a Vect of length less than 3

dependent-type

idris