3 unstable releases
0.2.1  Feb 23, 2024 

0.2.0  Feb 23, 2024 
0.1.1  Jan 23, 2022 
0.1.0 

#244 in Rust patterns
32 downloads per month
115KB
2.5K
SLoC
deptypes
An implementation of dependent types for Rust by lifting values to the type level.
It can be used in practice for relatively simple applications like vector types depending on the vector length, but you might need to extend it and add missing functionality as needed for more complex usae cases.
Usage
Add this to your Cargo.toml
:
[dependencies]
deptypes = "0.2"
How does it work?
The crate defines a Term
trait to represent expressions lifted to the type level, and a Value<T: Term>
type that carries the value of a term.
This allows to form zerosized term types like Succ<A>
representing A + 1 and Add<A, B>
representing the sum of two Values.
We can then form, for example, DLVec<i32, Var<'a, usize>>
and DLVec<i32, Succ<Var<'a, usize>>>
, which are two vectors of i32s where the second one is guaranteed to be always one item longer than the first;
Var<'a, T>
represents variables, implemented by leveraging the generativity
crate to define a term such that Value<Var<'a, T>>
can only be instantiated once, thus guaranteeing that the value of a variable is always the same (for each time the region it's used in is run).
A ValueEq<A, B>
value encodes a proof that the Values A
and B
have the same value, and allows to safely transmute Value<A>
into Value<B>
. For instance, the uint_as_succ
function takes an unsigned integer and a Guard<'a>
and either returns a proof that it is zero ValueEq<A, Zero<A::Type>>
or the value of its predecessor expressed as a variable Value<Var<'a, A::Type>>
and a proof that the input number is its successor ValueEq<A, Succ<Var<'a, A::Type>>>
.`
Several facilities are provided on top of these basic features, such as Peanolike terms for integers, dependent rangelimited integers, data dependent pair and Result, dependent Vec, tools to create and combine equality proofs, axioms and theorems for integers and booleans.
Note that unlike dependently typed languages, this crate uses several asserted axioms, since proving things by induction is very unwieldy although possible, and also would require to either assert the totality and purity of Rust functions or build a way to encode total pure functions at the type level.
The set of provided facilities is quite basic at the moment.
Features
The std
feature enables the standard library, the nightly
feature enable parts of the crate that need nightly, currently consisting of the never
features requiring the never type.
Example
This is an example of guaranteed nonpanicing indexing of multiple lengthdependent vectors, as well as encapsulation of dependent types using dependent pairs.
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(())
}
}
Changelog
Version 0.2
General overhaul of the whole codebase.
 Now requires GATs and thus Rust >= 1.66
 Helpers to loop over a dependentlytyped stated, so recursion is no longer needed and should no longer be used (since it will overflow the stack)
 Nonessential features moved to deptypes_extra
 type_eq overhauled: now have a TypeNe and no longer uses Uninhabited
 Terms now use checked_*, avoiding overflows, making them sound
 Ops terms now require ConstOps, since nonconst ops would make them unsound
 term! only supports fnlike syntax
 DPair is now a struct and no longer a macro
 Arithmetic theorems are now proven using only a small number of axioms
 More arithmetic theorems
Version 0.1
Initial version
Dependencies
~0.5–1MB
~23K SLoC