types - Little Typer：如何禁止具有更具体类型的参数？

Question

我想了解并正确利用更具体类型的技术来排除不需要的参数。6.37 左右给出的示例是first包装函数，head不能在空向量上调用。他们的解决方案是使用 +1 来偏置类型声明：

(claim first
    (Pi ((E U) (l Nat))
        (-> (Vec E (add1 l))
            E)))

这很不舒服，因为如果前两个参数是向量的包含类型和长度，则在调用它时必须“撒谎”：

(first Atom 2 (vec:: 'A (vec:: 'B (vec:: 'C vecnil))))

问题 #1：我的概念是否错误？不得不“撒谎”来解决某事感觉就像某事并没有真正被理解。

我告诉first我要发送一个长度为 2 的 Atom 向量，而实际上它的长度为 3。调用假设second将需要 2 的不诚实。对于third，不诚实为 3，依此类推。

我想知道是否最好不将 l 视为向量的长度，而是将其视为函数的一个版本。没有任何版本first需要一个空向量。它的第 0 个版本采用向量长度 1。它的第二个版本采用向量长度 2：

第一版	第一类
0	(-> (Vec E 1) E)
1	(-> (Vec E 2) E)
...	...

问题#2：这是正确的思考方式吗？这本书使用l，所以似乎他们希望读者思考“长度”。

考虑到这一点，我着手进行纠正first，以获取输入向量的包含类型和真实长度。旧的实现现在包含在新的实现中first-worker并被新的first：

(claim first-worker
    (Pi ((T U) (version Nat))
        (-> (Vec T (add1 version)) ; the i'th version takes vectors length i+1
            T)))

(define first-worker
    (lambda (E l)
        (lambda (es)
            (head es))))

(claim first
    (Pi ((E U) (length Nat))
        (-> (Vec E length) E)))

(define first
    (lambda (E length input)
        (first-worker E (sub1 length) input))) ; length vectors call version length-1

(first-worker Atom 3 (vec:: 'A (vec:: 'B (vec:: 'C vecnil))))

但是现在没有空向量的保护！(first Atom 0 vecnil)如果要进行类型检查（不允许），仍然允许调用 like 。

问题#3：我怎样才能写出first输入向量的真实长度？

任何其他建议和更正表示赞赏。

标签： typesracketpie-lang