细化参数的`case` [英] `case` that refines arguments

问题描述

在有关总体检查器的问题中的答案，此变通办法涉及使用case而不是with被推荐.

In this answer on a question about the totality checker, a workaround involving using case instead of with was recommended.

但是，在匹配结果细化其他参数类型的情况下，这种转换并不容易进行.

However, in situations where the result of the match refines the type of other arguments, this transformation is not straightforward to make.

例如，给定以下定义:

data IsEven : Nat -> Nat -> Type where
    Times2 : (n : Nat) -> IsEven (n + n) n

data IsOdd : Nat -> Nat -> Type where
    Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n

total parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))

以下定义类型进行检查，但不接受总计:

the following definition typechecks, but is not accepted as total:

foo1 : Nat -> Nat
foo1 n with (parity n)
  foo1 n@(k + k) | Left (Evidence _ (Times2 k)) = (n * n)
  foo1 n@(S (k + k)) | Right (Evidence _ (Times2Plus1 k)) = (2 * (k * n + k))

以下内容不会进行类型检查:

whereas the following one doesn't typecheck:

foo2 : Nat -> Nat
foo2 n = case parity n of
  Left (Evidence k (Times2 k)) => n * n
  Right (Evidence k (Times2Plus1 k)) => (2 * (k * n + k))

由于

Type mismatch between
      IsEven (k + k) k (Type of Times2 k)
and
      IsEven n k (Expected type)

我还尝试了，但是在这里，foo1'也不被接受为总计:

but here, foo1' is also not accepted as total:

 foo1' is not total as there are missing cases

推荐答案

为此，我发现一个有效的解决方法是在每个分支中重新绑定n，即将foo2编写为

One effective workaround I've found for this is to re-bind n in each branch, i.e. to write foo2 as

foo2 : Nat -> Nat
foo2 n = case parity n of
  Left (Evidence k (Times2 k)) => let n = k + k in n * n
  Right (Evidence k (Times2Plus1 k)) => let n = S (k + k) in (2 * (k * n + k))

不幸的是，虽然这对于我最初提出的问题来说是一个简化的问题，但是当各个分支的类型不同时，它就不起作用.例如在

Unfortunately, while this works for this simplified problem from my original question, it doesn't work when the types of the various branches differ; for example in

total Foo : Nat -> Type
Foo n = case parity n of
    Left (Evidence k (Times2 k)) => ()
    Right (Evidence k (Times2Plus1 k)) => Bool

foo : (n : Nat) -> Foo n
foo n = case parity n of
    Left (Evidence k (Times2 k)) => ()
    Right (Evidence k (Times2Plus1 k)) => True

失败

 Type mismatch between
         () (Type of ())
 and
         case parity (plus k k) of
           Left (Evidence k (Times2 k)) => ()
           Right (Evidence k (Times2Plus1 k)) => Bool (Expected type)

这篇关于细化参数的`case`的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！