如何让Agda识别if语句then分支中恒成立的属性？

问题背景 #

假设我需要定义一个Digit类型，作为Char类型的精化类型，仅用于表示数字字符：

open import Data.Bool using (Bool; true; if_then_else_)
open import Data.Char using (Char; isDigit)
open import Data.Maybe using (Maybe; just; nothing)

data IsTrue : Bool → Set where
  is-true : IsTrue true

data IsDigit (c : Char) : Set where
  is-digit : {p : IsTrue (isDigit c)} → IsDigit c

data Digit : Set where
  digit : (c : Char) → {p : IsDigit c} → Digit

我可以按如下方式构造对应字符'0'的Digit实例，不过需要显式传入隐式参数的写法较为繁琐：

0-digit : Digit
0-digit = digit '0' {is-digit {_} {is-true}}

但编写接收任意Char、返回Maybe Digit的函数时，Agda无法自动识别if表达式then分支中isDigit c必然为真的事实，传入is-true作为证明会报类型错误：

maybeFromChar : Char → Maybe Digit
maybeFromChar c =
  if isDigit c
    then just (digit c {is-digit {c} {is-true}})
    else nothing

错误信息如下：

.../Foo.agda:20,39-46
true != isDigit c of type Bool
when checking that the expression is-true has type
IsTrue (isDigit c)

部分编程语言将这类分支中的类型推导称为流类型（flow typing），但Agda仅在对构造器做模式匹配时才会自动推导这类等式信息。如果对'0'到'9'的所有字符做穷尽匹配确实可以通过编译，但写法过于繁琐。同时也希望获得Digit类型建模的优化建议。

解决方案 #

核心原因 #

普通的if_then_else_函数类型为{A : Set} → Bool → A → A → A，仅做普通布尔值分支，不会将分支条件的真值证据带入上下文，因此Agda无法在then分支中得知isDigit c ≡ true，自然无法接受is-true作为IsTrue (isDigit c)的实例。

最简便的修复方式 #

使用Agda的with抽象对isDigit c的返回值直接做模式匹配，匹配到true构造器时，Agda会自动将isDigit c = true的等式写入上下文，证明即可通过类型检查：

maybeFromChar : Char → Maybe Digit
maybeFromChar c with isDigit c
... | true = just (digit c {is-digit {c} {is-true}})
... | false = nothing

不需要手动写额外的相等性证明，也不需要枚举所有数字字符。

类型建模优化建议 #

你当前的定义存在冗余包装，可以做如下简化：

• 去掉多余的IsDigit层，直接将IsTrue (isDigit c)作为digit构造器的隐式参数即可，不需要额外定义单构造器的IsDigit类型：

  data Digit : Set where
    digit : (c : Char) → {p : IsTrue (isDigit c)} → Digit
  

  你现在定义的IsTrue属于轻量的“真值见证”类型，比使用命题相等isDigit c ≡ true性能更好，是比较好的实践，可以保留。
• 平时构造Digit统一通过maybeFromChar这个智能构造器，不需要每次手动填写隐式证明参数，减少样板代码。
• 如果需要更通用的精化类型能力，可以直接使用标准库的Data.Refinement模块定义子集类型，不需要手动编写包装类型，配套的消去、构造工具也可以减少证明相关的样板代码：

  open import Data.Refinement using (Refinement; _,_)
  Digit : Set
  Digit = Refinement Char (λ c → IsTrue (isDigit c))
  

如果确实需要保留if写法而非使用with，可以搭配inspect机制手动携带isDigit c和匹配值的相等性证据，但常规场景下with写法是Agda中最简洁、符合习惯的实现方式。

内容的提问来源于stack exchange，提问作者Camelid