检查向量的长度是否相等答案

【问题标题】：Check if Vector's Lengths are Equal检查向量的长度是否相等
【发布时间】：2017-02-27 02:40:32
【问题描述】：

鉴于Type-Driven Development with Idris的以下内容：

import Data.Vect

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num                               

sameS : (eq : EqNat k j) -> EqNat (S k) (S j)
sameS (Same n) = Same (S n)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z     Z     = Just $ Same Z
checkEqNat Z     (S k) = Nothing
checkEqNat (S k) Z     = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                           Just eq => Just $ sameS eq
                           Nothing => Nothing

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case (checkEqNat m len) of 
                              Just (Same m) => Just input
                              Nothing       => Nothing

如果我用Just eq 替换最后一个函数的Just (Same m)，编译器会报错：

*Lecture> :r
Type checking ./Lecture.idr
Lecture.idr:19:75:
When checking right hand side of Main.case block in exactLength at Lecture.idr:18:34 with expected type
        Maybe (Vect len a)

When checking argument x to constructor Prelude.Maybe.Just:
        Type mismatch between
                Vect m a (Type of input)
        and
                Vect len a (Expected type)

        Specifically:
                Type mismatch between
                        m
                and
                        len
Holes: Main.exactLength

Just (Same m)（即工作代码）如何提供“证据”证明exactLength 的len 和m 相等？

【问题讨论】：

标签： idris

【解决方案1】：

我发现与 Idris 合作时有用的是在您不确定某事而不是解决问题时添加漏洞。就像在Just ... 分支中添加一个洞以查看那里发生了什么：

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case (checkEqNat m len) of
                        Just (Same m) => ?hole
                        Nothing => Nothing

然后将(Same m) 更改为eq 并返回，同时查看类型检查的结果。在eq 的情况下是这样的：

- + Main.hole [P]
 `--          a : Type
              m : Nat
            len : Nat
             eq : EqNat m len
          input : Vect m a
     --------------------------------
      Main.hole : Maybe (Vect len a)

在(Same m) 的情况下是这样的：

- + Main.hole_1 [P]
 `--            m : Nat
                a : Type
            input : Vect m a
     --------------------------------
      Main.hole_1 : Maybe (Vect m a)

所以eq 是EqNat m len 的一种类型，没有人知道它是否是inhabitant，而Same m（或Same len）肯定是inhabitant，这证明m 和len 相等。

【讨论】：

【解决方案2】：

当你开始时

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input  with (_)
  exactLength {m} len input  | with_pat = ?_rhs

并逐渐扩展缺失的链接，直到你到达p>

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input  with (checkEqNat m len)
  exactLength {m = m} len input  | Nothing = Nothing
  exactLength {m = len} len input  | (Just (Same len)) = Just input

你可以看到 idris 是如何从 checkEqNat m len 返回一个 Just (Same ...) 的事实推导出来的，然后它可以推断出 {m = len}。 AFAIK 只写 Just eq 并不能证明 eq 确实有人居住。

【讨论】：