diff --git a/bidir/src/abstract_data.rs b/bidir/src/abstract_data.rs new file mode 100644 index 0000000..cf73885 --- /dev/null +++ b/bidir/src/abstract_data.rs @@ -0,0 +1,9 @@ +pub trait Data { + /* Required methods */ + /* */ + + /* Provided methods */ + /* */ + + fn synthesize() {} +} diff --git a/bidir/src/bidir_debruijn.rs b/bidir/src/bidir_debruijn.rs new file mode 100644 index 0000000..e69de29 diff --git a/bidir/src/convert_data.rs b/bidir/src/convert_data.rs new file mode 100644 index 0000000..d704684 --- /dev/null +++ b/bidir/src/convert_data.rs @@ -0,0 +1,51 @@ +use crate::DEPTH; +use crate::{data, data_debruijn, gensym::gensym_type}; + +pub fn convert_term(term: &data::Term) -> data_debruijn::Term { + fn convert_term_with_context(ctx: &data::Context, term: &data::Term) -> data_debruijn::Term { + match term { + data::Term::Unit => data_debruijn::Term::Unit, + + data::Term::Var(name) => { + let (idx, _) = ctx.lookup_type(name).unwrap(); + let ctx_len = ctx.0.len(); + data_debruijn::Term::Var(ctx_len - 1 - idx) + } + + data::Term::Lam(arg, body) => { + let ty = gensym_type(); + let ctx2 = ctx.add(vec![data::ContextEntry::TermAnnot( + arg.to_owned(), + data::Type::Var(ty.clone()), + )]); + let body = convert_term_with_context(&ctx2, body); + data_debruijn::Term::Lam(Box::new(body)) + } + + data::Term::App(func, arg) => { + let func = convert_term_with_context(ctx, &func); + let arg = convert_term_with_context(ctx, &arg); + data_debruijn::Term::App(Box::new(func), Box::new(arg)) + } + + data::Term::Annot(term, ty) => { + let term = convert_term_with_context(ctx, &term); + let ty = convert_ty_with_context(ctx, &ty); + data_debruijn::Term::Annot(Box::new(term), ty) + } + } + } + + fn convert_ty_with_context(ctx: &data::Context, ty: &data::Type) -> data_debruijn::Type { + match ty { + data::Type::Unit => data_debruijn::Type::Unit, + + data::Type::Var(_) => todo!(), + data::Type::Existential(_) => todo!(), + data::Type::Polytype(_, _) => todo!(), + data::Type::Arrow(_, _) => todo!(), + } + } + + convert_term_with_context(&data::Context::default(), term) +} diff --git a/bidir/src/data.rs b/bidir/src/data.rs index 34ad544..2cab8e8 100644 --- a/bidir/src/data.rs +++ b/bidir/src/data.rs @@ -1,4 +1,4 @@ -use std::{fmt, hash::Hash, mem::replace}; +use std::{fmt, hash::Hash}; use anyhow::{bail, Result}; use im::{HashSet, Vector}; diff --git a/bidir/src/data_debruijn.rs b/bidir/src/data_debruijn.rs new file mode 100644 index 0000000..ba7f526 --- /dev/null +++ b/bidir/src/data_debruijn.rs @@ -0,0 +1,332 @@ +use std::{fmt, hash::Hash}; + +use anyhow::{bail, Result}; +use im::{HashSet, Vector}; + +use crate::gensym::gensym_existential; + +/// A lambda calculus term. +#[derive(Clone)] +pub enum Term { + /// Unit type + Unit, + + /// Variable, with a reference into the context. + /// The entry pointed to by this index MUST be a TypeVar. + Var(usize), + + /// Lambda abstraction. + Lam(Box), + + /// Lambda application. + App(Box, Box), + + /// Type annotation + Annot(Box, Type), +} + +impl fmt::Debug for Term { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Unit => write!(f, "unit"), + Self::Var(arg0) => write!(f, "{}", arg0), + Self::Lam(arg1) => write!(f, "(ฮป.{:?})", arg1), + Self::App(arg0, arg1) => write!(f, "({:?} ยท {:?})", arg0, arg1), + Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1), + } + } +} + +#[derive(Clone)] +pub enum Type { + Unit, + Var(usize), + Existential(usize), + Polytype(Box), + Arrow(Box, Box), +} + +impl fmt::Debug for Type { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Unit => write!(f, "๐Ÿ™"), + Self::Var(arg0) => write!(f, "{}", arg0), + Self::Existential(arg0) => write!(f, "{}", arg0), + Self::Polytype(arg1) => write!(f, "(โˆ€.{:?})", arg1), + Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1), + } + } +} + +impl Type { + /// Attempt to turn this polytype into a monotype. + /// + /// This fails if any sub-expression of this type contains a polytype expression. + pub fn try_into_mono(&self) -> Option { + match self { + Type::Unit => Some(Monotype::Unit), + Type::Var(x) => Some(Monotype::Var(*x)), + Type::Existential(x) => Some(Monotype::Existential(*x)), + + // Polytypes cannot be converted to monotypes + Type::Polytype(_) => None, + + Type::Arrow(a, b) => Some(Monotype::Arrow( + Box::new(a.try_into_mono()?), + Box::new(b.try_into_mono()?), + )), + } + } + + #[inline] + pub fn is_mono(&self) -> bool { + self.try_into_mono().is_some() + } +} + +impl Type { + // pub fn free_vars(&self) -> HashSet { + // fn free_vars_with_context(ctx: &Context, ty: &Type) -> HashSet { + // match ty { + // Type::Unit => HashSet::default(), + // Type::Var(x) if ctx.lookup_type(x).is_some() => HashSet::default(), + // Type::Var(x) => [FreeVar::Var(x.to_owned())].into_iter().collect(), + // Type::Existential(x) if ctx.lookup_existential(x).is_some() => HashSet::default(), + // Type::Existential(x) => [FreeVar::Existential(x.to_owned())].into_iter().collect(), + // Type::Polytype(x, ty_a) => { + // let new_ctx = ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]); + // free_vars_with_context(&new_ctx, &ty_a) + // } + // Type::Arrow(ty_a, ty_b) => { + // let a_vars = free_vars_with_context(&ctx, &ty_a); + // let b_vars = free_vars_with_context(&ctx, &ty_b); + // a_vars.union(b_vars) + // } + // } + // } + + // free_vars_with_context(&Context::default(), self) + // } + + // /// Substitute all variables with this variable with the replacement type. + // pub fn subst(&self, var: &str, replacement: &Type) -> Type { + // match self { + // Type::Unit => Type::Unit, + // Type::Var(n) if n == var => replacement.clone(), + // Type::Var(n) => Type::Var(n.clone()), + // Type::Existential(s) if s == var => replacement.clone(), + // Type::Existential(s) => Type::Existential(s.clone()), + // Type::Polytype(t) => { + // // Type::Polytype(a.clone(), Box::new(t.subst(var, replacement))), + // todo!() + // } + // Type::Arrow(a, b) => Type::Arrow( + // Box::new(a.subst(var, replacement)), + // Box::new(b.subst(var, replacement)), + // ), + // } + // } +} + +#[derive(Clone)] +pub enum Monotype { + Unit, + Var(usize), + Existential(usize), + Arrow(Box, Box), +} + +impl fmt::Debug for Monotype { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Unit => write!(f, "๐Ÿ™"), + Self::Var(arg0) => write!(f, "{}", arg0), + Self::Existential(arg0) => write!(f, "{}", arg0), + Self::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"), + } + } +} + +impl Monotype { + pub fn into_poly(&self) -> Type { + match self { + Monotype::Unit => Type::Unit, + Monotype::Var(x) => Type::Var(x.clone()), + Monotype::Existential(x) => Type::Existential(x.clone()), + Monotype::Arrow(a, b) => Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly())), + } + } +} + +#[derive(Clone)] +pub enum ContextEntry { + TypeVar(String), + TermAnnot(String, Type), + ExistentialVar(String), + ExistentialSolved(String, Monotype), + Marker(String), +} + +impl fmt::Debug for ContextEntry { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::TypeVar(arg0) => write!(f, "{}", arg0), + Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1), + Self::ExistentialVar(arg0) => write!(f, "{}", arg0), + Self::ExistentialSolved(arg0, arg1) => write!(f, "{} โ‰” {:?}", arg0, arg1), + Self::Marker(arg0) => write!(f, "โ–ถ{}", arg0), + } + } +} + +#[derive(Debug, Clone)] +pub enum CompleteContextEntry { + TypeVar(String), + TermAnnot(String, Type), + ExistentialSolved(String, Monotype), + Marker(String), +} + +#[derive(Clone, Default)] +pub struct Context(pub(crate) Vector); + +impl fmt::Debug for Context { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str("ฮ“")?; + for rule in self.0.iter() { + f.write_str(", ")?; + rule.fmt(f)?; + } + Ok(()) + } +} + +impl Context { + pub fn add(&self, entries: Vec) -> Context { + let mut new_ctx = self.clone(); + for entry in entries { + new_ctx.0.push_back(entry); + } + new_ctx + } + + /// Looks up a polytype by name, also returning an index + pub fn lookup_type(&self, name: impl AsRef) -> Option<(usize, Type)> { + self + .0 + .iter() + .enumerate() + .find_map(|(i, entry)| match entry { + ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some((i, t.clone())), + _ => None, + }) + } + + #[inline] + pub fn has_type(&self, name: impl AsRef) -> bool { + self.lookup_type(name).is_some() + } + + /// Looks up an existential variable by name + /// - Returns Some(Some(t)) if solved + /// - Returns Some(None) if exists but unsolved + /// - Returns None if not found + pub fn lookup_existential(&self, name: impl AsRef) -> Option<(usize, Option)> { + self + .0 + .iter() + .enumerate() + .find_map(|(i, entry)| match entry { + ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some((i, None)), + ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some((i, Some(t.clone()))), + _ => None, + }) + } + + #[inline] + pub fn has_existential(&self, name: impl AsRef) -> bool { + self.lookup_existential(name).is_some() + } + + /// Returns a list of names of unsolved existentials + pub fn unsolved_existentials(&self) -> HashSet { + let mut unsolved = HashSet::new(); + + for entry in self.0.iter() { + match entry { + ContextEntry::ExistentialVar(n) => { + unsolved.insert(n.clone()); + } + _ => {} + } + } + + unsolved + } + + /// Returns (before, after) + pub fn split_by

(&self, p: P) -> Option<(Context, Context)> + where + P: Fn(&ContextEntry) -> bool, + { + let (before, after) = { + let idx = self.0.iter().position(p)?; + self.0.clone().split_at(idx) + }; + + Some((Context(before), Context(after))) + } + + pub fn unsplit(left: &Context, center: ContextEntry, right: &Context) -> Context { + let mut res = left.clone(); + res.0.push_back(center); + res.0.extend(right.0.clone().into_iter()); + res + } + + // pub fn split_existential_function(&self, var: &str) -> Result<(String, String, Context)> { + // let mut ctx = self.clone(); + // let idx = match ctx.lookup_existential(var) { + // Some((idx, _)) => idx, + // None => bail!("wtf?"), + // }; + + // let ex_a1_s = gensym_existential(); + // let ex_a2_s = gensym_existential(); + // ctx.0[idx] = ContextEntry::ExistentialSolved( + // var.to_owned(), + // Monotype::Arrow( + // Box::new(Monotype::Existential(ex_a1_s.to_owned())), + // Box::new(Monotype::Existential(ex_a2_s.to_owned())), + // ), + // ); + // ctx + // .0 + // .insert(idx, ContextEntry::ExistentialVar(ex_a1_s.to_owned())); + // ctx + // .0 + // .insert(idx, ContextEntry::ExistentialVar(ex_a2_s.to_owned())); + + // Ok((ex_a1_s, ex_a2_s, ctx)) + // } +} + +/// An index into the context. +pub struct ContextIndex { + context_length: usize, + context_index: usize, + context_level: usize, +} + +impl ContextIndex { + /// Bump an index, creating a new one when entering a new context level + /// + /// This should ensure the index is still referring to the same context entry. + pub fn bump(&self) -> Self { + ContextIndex { + context_length: self.context_length + 1, + context_index: self.context_index + 1, + context_level: self.context_level, + } + } +} diff --git a/bidir/src/lib.rs b/bidir/src/lib.rs index 4168c21..7e0681e 100644 --- a/bidir/src/lib.rs +++ b/bidir/src/lib.rs @@ -5,9 +5,15 @@ extern crate trace; use lalrpop_util::lalrpop_mod; +pub mod abstract_data; pub mod bidir; pub mod data; +pub mod convert_data; + +pub mod bidir_debruijn; +pub mod data_debruijn; + mod gensym; #[cfg(test)] mod tests; diff --git a/bidir/src/main.rs b/bidir/src/main.rs index afdc348..caab26b 100644 --- a/bidir/src/main.rs +++ b/bidir/src/main.rs @@ -1,6 +1,7 @@ use anyhow::Result; use bidir::{ bidir::{app_ctx, synthesize}, + convert_data::convert_term, data::Context, parser::TermParser, }; @@ -18,6 +19,8 @@ fn main() -> Result<()> { Err(_) => break, }; + // let line = r"\x.\y.x"; + let parsed_term = match term_parser.parse(&line) { Ok(term) => term, Err(err) => { @@ -28,6 +31,9 @@ fn main() -> Result<()> { println!("parsed: {:?}", parsed_term); let ctx = Context::default(); + let converted_term = convert_term(&parsed_term); + println!("converted: {converted_term:?}"); + let (ty, out_ctx) = match synthesize(&ctx, &parsed_term) { Ok(v) => v, Err(err) => { @@ -47,6 +53,7 @@ fn main() -> Result<()> { }; println!("synthesized: {:?}", ty); + // break; } Ok(()) diff --git a/hwk2.typ b/hwk2.typ index edab7d5..6fa1619 100644 --- a/hwk2.typ +++ b/hwk2.typ @@ -2,6 +2,12 @@ #set page("us-letter") #import "@preview/prooftrees:0.1.0": * #import emoji: face +#let prooftree(..args) = tree( + tree_config: tree_config( + vertical_spacing: 6pt, + ), + ..args +) = Homework 2 @@ -11,10 +17,12 @@ Michael Zhang \ set text(gray) body } +#let subst = $"subst"$ +#let tt = $"tt"$ #c[Assume you have $"Id"$ and $"U"$ but not $"Eq"$ (or $hat("Eq")$). Write down an abstraction $p$ such that -#tree( +#prooftree( axi[$a in A [Gamma]$], axi[$b in B [Gamma]$], bin[$p(a, b) in "Id"(A+B, "inl"(a), "inr"(b)) arrow.r emptyset [Gamma]$] @@ -25,11 +33,25 @@ is derivable. You do not have to prove in your submission that it is derivable.] Wait isn't this just the same as the Peano's fourth axiom as given in the book? $ - p(a, b) &equiv lambda ((x) "subst"(x, "tt")) \ + p(a, b) &equiv lambda ((x) subst(x, tt)) \ $ where -- $P(m) = "Set"("when"(m, (x)hat(top), (y)hat({})))$ + +- $subst(c, p) equiv "apply"("idpeel"(c, (x) lambda x.x), p)$ + +#prooftree( + axi[$A "set"$], + axi[$B "set"$], + bin[$A + B "set"$], + axi[$a in A$], + axi[$b in B$], + axi[$p in "Id"(A + B, "inl"(a), "inr"(b))$], + axi[$P(x) "set" [x in A + B]$], + nary(5)[$subst(p, "inl"(a)) equiv "apply"("idpeel"(p, (g) lambda y.y), "inl"(a)) in P("inr"(b))$], +) + +- $P(m) equiv "Set"("when"(m, (x)hat(top), (y)hat({})))$ // (Agda implementation #face.smile.slight)