在这些基本功能之上，提供了一些设施，例如用于整数的 Peano 类项、依赖范围限制的整数、数据依赖的元组和 Result、依赖 Vec、创建和组合等价证明的工具，以及整数和布尔值的公理和定理。

请注意，与依赖类型语言不同，此包使用多个断言公理，因为虽然可以通过归纳证明事物，但这样做非常麻烦，并且还需要断言 Rust 函数的完备性和纯度，或者构建一种在类型级别编码完备纯函数的方法。

目前提供的设施集相当基本。

功能

std 功能启用标准库，nightly 功能启用需要夜间的包部分，目前包括需要 never 类型的 never 功能。

示例

这是一个确保非恐慌索引多个长度依赖向量的示例，以及使用依赖对封装依赖类型。

use deptypes::{term::{Term, ValueEq, Def}, fin::Fin, int::{Succ, a_lt_s_a}, vec::DVec, pair::DPair, kinds::Term2S, transmutable::{coerce, coerce_vec}, type_eq::refl, make_guard};
use core::marker::PhantomData;
use std::vec::Vec;

#[repr(C)] // to support trasmutation by Term2S::equiv
struct DWorld<NumEntities: Term<Type = usize>, NumMonsters: Term<Type = usize>> {
    // vectors of num_entities positions and velocities
    position: DVec<f64, NumEntities>,
    velocity: DVec<f64, NumEntities>,

    // vector of numbers less than num_entities representing entities that are a monster
    monsters: DVec<Fin<NumEntities>, NumMonsters>,
    smart_monsters: Vec<Fin<NumMonsters>>
}

struct DWorldFamily<NumEntities>(PhantomData<NumEntities>);

unsafe impl<NumEntities: Term<Type = usize>> Term2S<usize> for DWorldFamily<NumEntities>
{
    type Type<NumMonsters: Term<Type = usize>> = DWorld<NumEntities, NumMonsters>;
}

// this could be derived if deriving used proper bounds
impl Default for DWorld<Def<usize>, Def<usize>> {
    fn default() -> Self {
        DWorld {
            position: Default::default(),
            velocity: Default::default(),
            monsters: Default::default(),
            smart_monsters: Default::default()
        }
    }
}

impl<NumEntities: Term<Type = usize>, NumMonsters: Term<Type = usize>> DWorld<NumEntities, NumMonsters> {
    fn add_entity(self, position: f64, velocity: f64) -> DWorld<Succ<NumEntities>, NumMonsters> {
        // coerce all data from depending on Succ<old num_entities> to new num_entities
        let position = self.position.push(position);
        let velocity = self.velocity.push(velocity);
        // use fact that a < Succ(a) => a <= Succ(a) => Fin<a> transm to Fin<Succ(a)> to coerce monsters
        let monsters = coerce(self.monsters, DVec::transm(Fin::transm(a_lt_s_a().le()), refl()));
        let smart_monsters = self.smart_monsters;

        DWorld {position, velocity, monsters, smart_monsters}
    }

    fn add_monster(self, entity: Fin<NumEntities>) -> DWorld<NumEntities, Succ<NumMonsters>> {
        let position = self.position;
        let velocity = self.velocity;
        // use fact that a < Succ(a) => a <= Succ(a) => Fin<a> transm to Fin<Succ(a)> to coerce monsters
        let monsters = self.monsters.push(entity);
        let smart_monsters = coerce_vec(self.smart_monsters, Fin::transm(a_lt_s_a().le()));

        DWorld {position, velocity, monsters, smart_monsters}
    }

    fn add_smart_monster(&mut self, monster: Fin<NumMonsters>) {
        self.smart_monsters.push(monster);
    }
}

struct DPairDWorldFamily;

unsafe impl Term2S<usize> for DPairDWorldFamily
{
    type Type<NumEntities: Term<Type = usize>> = DPair<usize, DWorldFamily<NumEntities>>;
}

#[derive(Default)]
pub struct World(DPair<usize, DPairDWorldFamily>);

pub struct EntityId(usize);
pub struct EntityIdInvalidError;

pub struct MonsterId(usize);
pub struct MonsterIdInvalidError;

impl World {
    pub fn move_smart_monsters(&mut self, time: f64) {
        make_guard!(g);
        let (_num_entities, world1) = self.0.get_mut(g);
        make_guard!(g);
        let (_num_monsters, world) = world1.get_mut(g);

        for m in world.smart_monsters.iter().copied() {
            // these indexing operations are guaranteed to never fail, thanks to the dependent types!
            let e = world.monsters[m];
            world.position[e] += world.velocity[e] * time;
        }
    }

    pub fn add_entity(&mut self, position: f64, velocity: f64) -> EntityId {
        make_guard!(g);
        let (num_entities, world1) = core::mem::replace(&mut self.0, DPair::default()).into_inner(g);
        make_guard!(g);
        let (num_monsters, world) = world1.into_inner(g);

        let world = world.add_entity(position, velocity);

        self.0 = DPair::new(Succ(num_entities), DPair::new(num_monsters, world));
        EntityId(num_entities.into_inner())
    }

    pub fn add_monster(&mut self, entity: EntityId) -> Result<MonsterId, EntityIdInvalidError> {
        make_guard!(g);
        let (num_entities, world1) = core::mem::replace(&mut self.0, DPair::default()).into_inner(g);
        make_guard!(g);
        let (num_monsters, world) = world1.into_inner(g);

        let world = world.add_monster(Fin::from(num_entities, entity.0).ok_or(EntityIdInvalidError)?);

        self.0 = DPair::new(num_entities, DPair::new(Succ(num_monsters), world));
        Ok(MonsterId(num_monsters.into_inner()))
    }

    pub fn add_smart_monster(&mut self, monster: MonsterId) -> Result<(), MonsterIdInvalidError> {
        make_guard!(g);
        let (_num_entities, world1) = self.0.get_mut(g);
        make_guard!(g);
        let (num_monsters, world) = world1.get_mut(g);

        world.add_smart_monster(Fin::from(*num_monsters, monster.0).ok_or(MonsterIdInvalidError)?);

        Ok(())
    }
}

变更日志

版本 0.2

整个代码库的全面审查。

• 现在需要 GATs，因此 Rust >= 1.66
• 提供循环遍历依赖类型语句的辅助工具，因此不再需要递归，也不应再使用递归（因为它将溢出堆栈）。
• 非必需功能已移动到 deptypes_extra
• type_eq 重构：现在有 TypeNe，不再使用 Uninhabited
• 项现在使用 checked_*，避免溢出，使其成为正确的
• Ops 项现在需要 ConstOps，因为非 const 操作会使它们不正确
• term! 只支持 fn-like 语法
• DPair 现在是一个结构体，不再是宏
• 算术定理现在仅使用少量公理进行证明
• 更多算术定理

版本 0.1

初始版本