为什么 Lean 允许无效的 UInt8 文字？

Question

def x := (0xFFFF : UInt8)

编译时没有错误，考虑到 Lean 专注于证明正确性，我觉得这很令人惊讶。这样做有充分的理由还是仅仅是一个疏忽？另外它在运行时做了什么？

额外问题：是否有更优雅的方式来编写 UInt8 文字？例如。在 Rust 中你可以做到

0xFFu8

。

Answer 1

正如评论中提到的，允许这样做与“专注于证明正确性”并不矛盾；对于有界整数，超出类型边界的数字文字只是定义为环绕，因此您可以执行

#eval (0xFFFF : UInt8)

并会发现其计算结果为

255

。

这种行为的原因主要是由于 Lean 4 中数字文字的实现方式。这使用名为

OfNat

的类型类进行工作：当 Lean 遇到具有预期类型

n

的数字文字

α

时，它将尝试合成

OfNat α n

的实例。因此，为了获得拒绝越界文字的所需行为，仅当

OfNat α n

足够小时，您才需要以某种方式给出

n

的实例。这不是 Lean 的类型类系统以直接方式支持的东西，因此通常为所有

OfNat

定义

n

的实例，并且仅实现某种包装行为。

但是，实际上可以使用“有点晦涩的技巧”来获得所需的行为，如以下代码所示：

class When (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @When p (.isTrue h) := @When.mk p (_) h

-- Just a wrapper around `UInt8` to avoid clashing with the existing `OfNat` instance.
inductive MyUInt8 : Type where
  | mk : UInt8 -> MyUInt8

instance [When (n < 256)] : OfNat MyUInt8 n where
  ofNat := ⟨n.toUInt8⟩

#check (0xFF : MyUInt8) -- works
#check (0xFFFF : MyUInt8) -- failed to synthesize `OfNat MyUInt8 65535`

正如上面链接的线程中所讨论的，这种方法有一些局限性，因此不应被视为问题的良好解决方案，这大概就是精益核心开发人员不在精益核心中定义的

OfNat

实例中使用它的原因。

精益开发人员将来可能会重新设计数字文字，并引入比上述

When

hack 更简单、更通用的解决方案。做到这一点将很棘手，因为这可能是一个非常具有破坏性的变化，所以我不希望很快看到这方面的任何进展。

关于您的额外问题：如果预期类型已知，则无需注释数字文字的类型。例如，你可以写

def x : UInt8 := 0xFF