如何在Lean中实现类似Rust的关联类型Iterable类型类？

Rust中的实现示例 #

在Rust里，我们可以定义如下trait：

trait Iterator {
    type Item;
    fn next(&mut self) -> Option<Self::Item>;
}

trait Iterable {
    type Item;
    type Iterator: Iterator<Item=Self::Item>;
    fn iterator(self) -> Self::Iterator;
}

接着自定义CountToTen类型实现Iterable trait：

struct CountToTenIterator(u32);

impl Iterator for CountToTenIterator {
    type Item = u32;
    fn next(&mut self) -> Option<u32> {
        if self.0 < 10 {
            self.0 += 1;
            Some(self.0)
        } else {
            None
        }
    }
}

struct CountToTen;

impl Iterable for CountToTen {
    type Item = u32;
    type Iterator = CountToTenIterator;
    fn iterator(self) -> CountToTenIterator {
        CountToTenIterator(0)
    }
}

使用方式如下：

fn print_items<I: Iterable<Item=u32>>(iterable: I) {
    let mut iterator = iterable.iterator();
    while let Some(x) = iterator.next() {
        println!("{}", x);
    }
}

fn main() {
    print_items(CountToTen);
}

Lean中的现有代码 #

现在想在Lean里复刻这套逻辑，已经定义了Iterator类型类：

class Iterator (Self : Type) where
    Item : Type
    next : Self -> Prod Self (Option Item)

以及CountToTenIterator的实例：

structure CountToTenIterator where
    i : UInt32

instance : Iterator CountToTenIterator where
    Item := UInt32
    next self :=
        if self.i < 10 then
            let i := self.i + 1
            ({ i }, some i)
        else
            (self, none)

问题与解决方案 #

当前的Iterable框架如下，但需要约束其关联类型Iterator必须是Iterator类型类的实例，且Item要与Iterable的Item匹配：

class Iterable (Self : Type) where
    Item : Type
    Iterator : Type -- 如何约束这个类型必须是Iterator的实例？
    iterator : Self -> Iterator

正确的Iterable类型类定义 #

在Lean中，可通过依赖类型和实例约束实现需求。我们需要为Iterable的Iterator关联类型添加Iterator实例约束，同时指定该迭代器的Item与Iterable的Item一致：

class Iterable (Self : Type) where
    Item : Type
    Iterator : Type
    iterator : Self -> Iterator
    -- 添加约束：Iterator类型必须实现Iterator类型类，且其Item等于Iterable的Item
    iter_inst : Iterator Iterator
    h_item : iter_inst.Item = Item

更简洁的写法：直接在关联类型上通过[]指定实例约束，利用rfl对齐Item类型：

class Iterable (Self : Type) where
    Item : Type
    Iterator : Type
    [iter_inst : Iterator Iterator]
    h_item : iter_inst.Item = Item
    iterator : Self -> Iterator

实现CountToTen的Iterable实例 #

基于正确的Iterable定义，为CountToTen实现该类型类：

structure CountToTen where

instance : Iterable CountToTen where
    Item := UInt32
    Iterator := CountToTenIterator
    iter_inst := inferInstance -- 自动推导CountToTenIterator的Iterator实例
    h_item := rfl -- CountToTenIterator的Item就是UInt32，直接用rfl证明相等
    iterator _ := CountToTenIterator.mk 0

使用示例 #

类似Rust的print_items函数可这样编写：

def print_items {Self : Type} [Iterable Self] (iterable : Self) : IO Unit := do
    let mut iterator := Iterable.iterator iterable
    loop do
        let (new_iter, opt_val) := Iterator.next iterator
        iterator := new_iter
        match opt_val with
        | some x =>
            IO.println x
            continue
        | none =>
            break

def main : IO Unit := do
    print_items CountToTen.mk

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