Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Pull-based tree processing for lambda calculi.
//! See [this twitter thread](https://twitter.com/brendanzab/status/1191233778854662144).
//!
//! Traditional syntax trees suffer from lots of pointer indirections and poor data locality!
//! Could we stream things instead, using [pull-based events](http://www.xmlpull.org/history/index.html)
//! as opposed to trees? This should be equivalent to our tree based approaches, but might
//! require us to think carefully about what our core calculus looks like in order to make
//! this kind of thing easier.
use std::sync::Arc;
/// Types as a tree, for checkpointing.
#[derive(Clone, Debug)]
pub enum TypeTree {
/// Base type.
Base,
/// Function type.
Function {
parameter_ty: Arc<TypeTree>,
body_ty: Arc<TypeTree>,
},
/// Pair type.
Pair {
first_ty: Arc<TypeTree>,
second_ty: Arc<TypeTree>,
},
}
/// Terms in event form, for pull-based tree processing.
#[derive(Copy, Clone, Debug)]
pub enum TypeEvent {
/// Base type.
Base,
/// Start a function type.
FunctionStart,
/// End a function type.
FunctionEnd,
/// Start a pair type.
PairStart,
/// End a pair type.
PairEnd,
}
/// Terms as a tree, for checkpointing.
#[derive(Clone, Debug)]
pub enum TermTree<Binder, Var> {
/// A variable that refers to a binder.
Var(Var),
/// A term that is explicitly annotated with a type.
The {
term_ty: Arc<TypeTree>,
term: Arc<TermTree<Binder, Var>>,
},
/// Function term.
///
/// Also known as:
/// - anonymous function
/// - lambda abstraction
FunctionTerm {
binder: Binder,
body: Arc<TermTree<Binder, Var>>,
},
// TODO: Dependent types
// /// Function type.
// ///
// /// Also known as:
// /// - Π type
// /// - dependent function type
// /// - dependent product
// FunctionType {
// parameter_ty: Arc<TermTree<Binder, Var>>,
// parameter_binder: Binder,
// body_ty: Arc<TermTree<Binder, Var>>,
// },
/// Function elimination.
///
/// Also known as:
/// - function application
FunctionElim {
head: Arc<TermTree<Binder, Var>>,
argument: Arc<TermTree<Binder, Var>>,
},
// TODO: Dependent types
// /// Pair type.
// ///
// /// Also known as:
// /// - Σ type
// /// - dependent pair type
// /// - dependent sum
// PairType {
// first_ty: Arc<TermTree<Binder, Var>>,
// first_binder: Binder,
// second_ty: Arc<TermTree<Binder, Var>>,
// },
/// Pair term.
PairTerm {
first: Arc<TermTree<Binder, Var>>,
second: Arc<TermTree<Binder, Var>>,
},
/// Pair elimination.
PairElim {
head: Arc<TermTree<Binder, Var>>,
binders: (Binder, Binder),
body: Arc<TermTree<Binder, Var>>,
},
}
/// Terms in event form, for pull-based tree processing.
#[derive(Copy, Clone, Debug)]
pub enum TermEvent<Binder, Var> {
/// A variable that refers to a binder.
Var(Var),
/// Start an annotated term.
TheStart,
/// End an annotated term.
TheEnd,
/// Start a function term.
FunctionTermStart(Binder),
/// End a function term.
FunctionTermEnd,
/// Start a function elimination.
FunctionElimStart,
/// End a function elimination.
FunctionElimEnd,
/// Start a pair term.
PairTermStart,
/// End a pair term.
PairTermEnd,
/// Start a pair elimination.
PairElimStart,
/// Pair binder.
PairElimBinders(Binder, Binder),
/// End a pair elimination.
PairElimEnd,
/// A type event.
Type(TypeEvent),
}
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Type event processing
//
////////////////////////////////////////////////////////////////////////////////////////////////////
/// An error produced when attempting to call `TypeTree::from_events`.
#[derive(Clone, Debug)]
pub enum FromTypeEventError {
ExpectedFunctionEnd,
ExpectedPairEnd,
UnexpectedFunctionEnd,
UnexpectedPairEnd,
UnexpectedEof,
}
impl TypeTree {
/// Convert this type tree into a stream of type events.
pub fn into_events(self) -> impl Iterator<Item = TypeEvent> {
// TODO: Implement this!
match self {
TypeTree::Base => Some(TypeEvent::Base).into_iter(),
TypeTree::Function {
parameter_ty,
body_ty,
} => None.into_iter(),
TypeTree::Pair {
first_ty,
second_ty,
} => None.into_iter(),
}
}
/// Create a type tree from a stream of type events.
pub fn from_events(
events: &mut impl Iterator<Item = TypeEvent>,
) -> Result<TypeTree, FromTypeEventError> {
// TODO: Error recovery.
match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
TypeEvent::Base => Ok(TypeTree::Base),
TypeEvent::FunctionStart => {
// Stack depth?
let parameter_ty = Arc::new(TypeTree::from_events(events)?);
let body_ty = Arc::new(TypeTree::from_events(events)?);
match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
TypeEvent::FunctionEnd => Ok(TypeTree::Function {
parameter_ty,
body_ty,
}),
_ => Err(FromTypeEventError::ExpectedFunctionEnd),
}
}
TypeEvent::FunctionEnd => Err(FromTypeEventError::ExpectedFunctionEnd),
TypeEvent::PairStart => {
// Stack depth?
let first_ty = Arc::new(TypeTree::from_events(events)?);
let second_ty = Arc::new(TypeTree::from_events(events)?);
match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
TypeEvent::PairEnd => Ok(TypeTree::Pair {
first_ty,
second_ty,
}),
_ => Err(FromTypeEventError::ExpectedPairEnd),
}
}
TypeEvent::PairEnd => Err(FromTypeEventError::ExpectedPairEnd),
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Term event processing
//
////////////////////////////////////////////////////////////////////////////////////////////////////
/// An error produced when attempting to call `TermTree::from_events`.
#[derive(Clone, Debug)]
pub enum FromTermEventError {
ExpectedTheEnd,
ExpectedFunctionTermEnd,
ExpectedFunctionElimEnd,
ExpectedPairTermEnd,
ExpectedPairElimBinders,
ExpectedPairElimEnd,
UnexpectedTheEnd,
UnexpectedFunctionTermEnd,
UnexpectedFunctionElimEnd,
UnexpectedPairTermEnd,
UnexpectedPairElimBinders,
UnexpectedPairElimEnd,
UnexpectedType,
FromTypeEvent(FromTypeEventError),
UnexpectedEof,
}
impl From<FromTypeEventError> for FromTermEventError {
fn from(src: FromTypeEventError) -> FromTermEventError {
FromTermEventError::FromTypeEvent(src)
}
}
impl<Binder, Var> TermTree<Binder, Var> {
/// Convert this term tree into a stream of term events.
pub fn into_events(self) -> impl Iterator<Item = TermEvent<Binder, Var>> {
// TODO: Implement this!
match self {
TermTree::Var(var) => Some(TermEvent::Var(var)).into_iter(),
TermTree::The { term_ty, term } => None.into_iter(),
TermTree::FunctionTerm { binder, body } => None.into_iter(),
TermTree::FunctionElim { head, argument } => None.into_iter(),
TermTree::PairTerm { first, second } => None.into_iter(),
TermTree::PairElim {
head,
binders,
body,
} => None.into_iter(),
}
}
/// Create a term tree from a stream of term events.
pub fn from_events(
events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
) -> Result<TermTree<Binder, Var>, FromTermEventError> {
// TODO: Error recovery.
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::Var(var) => Ok(TermTree::Var(var)),
TermEvent::TheStart => {
// Stack depth?
let term_ty =
Arc::new(TypeTree::from_events(&mut events.by_ref().map(
|event| match event {
TermEvent::Type(ty) => ty,
_ => unimplemented!(), // FIXME
},
))?);
let term = Arc::new(TermTree::from_events(events)?);
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::TheEnd => Ok(TermTree::The { term_ty, term }),
_ => Err(FromTermEventError::ExpectedTheEnd),
}
}
TermEvent::FunctionTermStart(binder) => {
// Stack depth?
let body = Arc::new(TermTree::from_events(events)?);
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::FunctionTermEnd => Ok(TermTree::FunctionTerm { binder, body }),
_ => Err(FromTermEventError::ExpectedFunctionTermEnd),
}
}
TermEvent::FunctionElimStart => {
// Stack depth?
let head = Arc::new(TermTree::from_events(events)?);
let argument = Arc::new(TermTree::from_events(events)?);
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::FunctionElimEnd => Ok(TermTree::FunctionElim { head, argument }),
_ => Err(FromTermEventError::ExpectedFunctionElimEnd),
}
}
TermEvent::PairTermStart => {
// Stack depth?
let first = Arc::new(TermTree::from_events(events)?);
let second = Arc::new(TermTree::from_events(events)?);
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::PairTermEnd => Ok(TermTree::PairTerm { first, second }),
_ => Err(FromTermEventError::ExpectedPairTermEnd),
}
}
TermEvent::PairElimStart => {
// Stack depth?
let head = Arc::new(TermTree::from_events(events)?);
let binders = match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::PairElimBinders(first, second) => (first, second),
_ => return Err(FromTermEventError::ExpectedPairElimBinders),
};
let body = Arc::new(TermTree::from_events(events)?);
match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
TermEvent::PairElimEnd => Ok(TermTree::PairElim {
head,
binders,
body,
}),
_ => Err(FromTermEventError::ExpectedPairElimEnd),
}
}
TermEvent::TheEnd => Err(FromTermEventError::UnexpectedTheEnd),
TermEvent::FunctionTermEnd => Err(FromTermEventError::UnexpectedFunctionTermEnd),
TermEvent::FunctionElimEnd => Err(FromTermEventError::UnexpectedFunctionElimEnd),
TermEvent::PairTermEnd => Err(FromTermEventError::UnexpectedPairTermEnd),
TermEvent::PairElimBinders(_, _) => Err(FromTermEventError::UnexpectedPairElimBinders),
TermEvent::PairElimEnd => Err(FromTermEventError::UnexpectedPairElimEnd),
TermEvent::Type(_) => Err(FromTermEventError::UnexpectedType),
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Renaming pass
//
////////////////////////////////////////////////////////////////////////////////////////////////////
/// A locally nameless variable.
pub enum LnVar<Name> {
/// Free variables.
Free(Name),
/// De Bruijn index. This is the number of binders we need to skip to get to
/// the binder that bound this variable.
Bound(usize),
}
/// Erase variable names where possible, turning them into locally nameless variables.
pub fn remove_names<'a, Binder: Clone + PartialEq<Var> + 'a, Var>(
named_events: &'a mut impl Iterator<Item = TermEvent<Binder, Var>>,
) -> impl Iterator<Item = TermEvent<Binder, LnVar<Var>>> + 'a {
named_events.scan(Vec::new(), |names, named_event| match named_event {
TermEvent::Var(var) => match names.iter().rposition(|name| *name == var) {
None => Some(TermEvent::Var(LnVar::Free(var))),
Some(index) => Some(TermEvent::Var(LnVar::Bound(index))),
},
TermEvent::TheStart => Some(TermEvent::TheStart),
TermEvent::TheEnd => Some(TermEvent::TheEnd),
TermEvent::FunctionTermStart(binder) => {
names.push(binder.clone());
Some(TermEvent::FunctionTermStart(binder))
}
TermEvent::FunctionTermEnd => {
names.pop();
Some(TermEvent::FunctionTermEnd)
}
TermEvent::FunctionElimStart => Some(TermEvent::FunctionElimStart),
TermEvent::FunctionElimEnd => Some(TermEvent::FunctionElimEnd),
TermEvent::PairTermStart => Some(TermEvent::PairTermStart),
TermEvent::PairTermEnd => Some(TermEvent::PairTermEnd),
TermEvent::PairElimStart => Some(TermEvent::PairElimStart),
TermEvent::PairElimBinders(first, second) => {
names.push(first.clone());
names.push(second.clone());
Some(TermEvent::PairElimBinders(first, second))
}
TermEvent::PairElimEnd => {
names.pop();
names.pop();
Some(TermEvent::PairElimEnd)
}
TermEvent::Type(event) => Some(TermEvent::Type(event)),
})
}
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Typing
//
////////////////////////////////////////////////////////////////////////////////////////////////////
pub fn check<Binder, Var>(
state: &mut Vec<(&str, TypeTree)>, // TODO
term_events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
expected_type: &TypeTree,
) -> Option<bool> {
match term_events.next()? {
TermEvent::FunctionTermStart(binding) => {
// TODO:
unimplemented!()
}
event => {
// TODO: conversion checking
unimplemented!()
}
}
}
pub fn synth<Binder, Var>(
state: &mut Vec<(&str, TypeTree)>, // TODO
term_events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
) -> Option<TypeTree> {
match term_events.next()? {
TermEvent::Var(var) => unimplemented!(), // TODO: lookup in context
TermEvent::TheStart => {
let term_ty =
TypeTree::from_events(&mut term_events.by_ref().map(|event| match event {
TermEvent::Type(ty) => ty,
_ => unimplemented!(), // FIXME
}))
.ok()?;
if check(state, term_events, &term_ty)? {
// TODO: expect TheEnd
Some(term_ty)
} else {
None
}
// FIXME: errors
}
TermEvent::FunctionElimStart => {
// TODO: synth head
// TODO: check body
unimplemented!()
}
TermEvent::PairTermStart => {
// TODO: synth first
// TODO: synth second
unimplemented!()
}
TermEvent::PairElimStart => {
// TODO: synth head
// TODO: expect binders
// TODO: synth body
unimplemented!()
}
_ => None,
}
}