This commit is contained in:
Michael Zhang 2023-11-07 00:50:27 -06:00
parent f42dbda234
commit 3c8e43d02d
3 changed files with 91 additions and 14 deletions

View file

@ -15,12 +15,13 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
None => bail!("existential variable {a} doesn't exist in context"), None => bail!("existential variable {a} doesn't exist in context"),
}, },
Type::Polytype(_, _) => todo!(), Type::Polytype(a, t) => Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?))),
Type::Arrow(a, b) => Ok(Type::Arrow( Type::Arrow(a, b) => Ok(Type::Arrow(
Box::new(app_ctx(ctx, a)?), Box::new(app_ctx(ctx, a)?),
Box::new(app_ctx(ctx, b)?), Box::new(app_ctx(ctx, b)?),
)), )),
_ => todo!("shiiet"), _ => todo!("shiiet ctx = {ctx:?}, ty = {ty:?}"),
} }
} }
@ -152,28 +153,73 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
Ok((ty_a.clone(), ctx_delta)) Ok((ty_a.clone(), ctx_delta))
} }
// →I⇒ rule // →I⇒' rule
// > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we
// > create new existential variables ^α (for the function domain) and ^β (for
// > the codomain) and check the function body against ^β. As in ∀App, we do
// > not place a marker before ^α, because ^α and ^β appear in the output type
// > (λx. e ⇒ ^α → ^β).
Term::Lam(x, e) => { Term::Lam(x, e) => {
let ex_a_s = gensym_existential(); let ex_a_s = gensym_existential();
let ex_b_s = gensym_existential(); let ex_b_s = gensym_existential();
let ex_gen = format!("{}->", ex_a_s);
let ex_a = Type::Existential(ex_a_s.clone()); let ex_a = Type::Existential(ex_a_s.clone());
let ex_b = Type::Existential(ex_b_s.clone()); let ex_b = Type::Existential(ex_b_s.clone());
let aug_ctx = ctx.add(vec![ let aug_ctx = ctx.add(vec![
ContextEntry::Marker(ex_a_s.clone()),
ContextEntry::ExistentialVar(ex_a_s.clone()), ContextEntry::ExistentialVar(ex_a_s.clone()),
ContextEntry::ExistentialVar(ex_b_s.clone()), ContextEntry::ExistentialVar(ex_b_s.clone()),
ContextEntry::TermAnnot(x.clone(), ex_a.clone()), ContextEntry::TermAnnot(x.clone(), ex_a.clone()),
]); ]);
let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?; let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
println!("the wtf ctx is {wtf_ctx:?}"); println!("WTF CTX {wtf_ctx:?}");
Ok((Type::Arrow(Box::new(ex_a), Box::new(ex_b)), ctx.clone()))
// Split back out at the marker
let (before_marker, after_marker) = {
let marker_idx = wtf_ctx
.0
.iter()
.position(|entry| match entry {
ContextEntry::Marker(m) if *m == ex_a_s => true,
_ => false,
})
.unwrap();
// println!("Marker index: {marker_idx}");
wtf_ctx.0.clone().split_at(marker_idx)
};
let before_marker = Context(before_marker);
let after_marker = Context(after_marker);
let mut tau = app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
for name in after_marker.unsolved_existentials() {
tau = tau.subst(name, &Type::Var(ex_gen.clone()));
}
Ok((Type::Polytype(ex_gen, Box::new(tau)), before_marker))
} }
// // →I⇒ rule
// // > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we
// // > create new existential variables ^α (for the function domain) and ^β (for
// // > the codomain) and check the function body against ^β. As in ∀App, we do
// // > not place a marker before ^α, because ^α and ^β appear in the output type
// // > (λx. e ⇒ ^α → ^β).
// Term::Lam(x, e) => {
// let ex_a_s = gensym_existential();
// let ex_b_s = gensym_existential();
// let ex_a = Type::Existential(ex_a_s.clone());
// let ex_b = Type::Existential(ex_b_s.clone());
// let aug_ctx = ctx.add(vec![
// ContextEntry::ExistentialVar(ex_a_s.clone()),
// ContextEntry::ExistentialVar(ex_b_s.clone()),
// ContextEntry::TermAnnot(x.clone(), ex_a.clone()),
// ]);
// let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
// println!("the wtf ctx is {wtf_ctx:?}");
// Ok((Type::Arrow(Box::new(ex_a), Box::new(ex_b)), ctx.clone()))
// }
// →E rule // →E rule
Term::App(e1, e2) => { Term::App(e1, e2) => {
let (ty_a, ctx_theta) = synthesize(ctx, e1)?; let (ty_a, ctx_theta) = synthesize(ctx, e1)?;

View file

@ -1,4 +1,4 @@
use std::{fmt, hash::Hash}; use std::{fmt, hash::Hash, mem::replace};
use im::{HashSet, Vector}; use im::{HashSet, Vector};
@ -38,7 +38,7 @@ impl fmt::Debug for Type {
Self::Unit => write!(f, "𝟙"), Self::Unit => write!(f, "𝟙"),
Self::Var(arg0) => write!(f, "{}", arg0), Self::Var(arg0) => write!(f, "{}", arg0),
Self::Existential(arg0) => write!(f, "{}", arg0), Self::Existential(arg0) => write!(f, "{}", arg0),
Self::Polytype(arg0, arg1) => write!(f, "(∀{}.{:?})", arg0, arg1), Self::Polytype(arg0, arg1) => write!(f, "(∀ {} . {:?})", arg0, arg1),
Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1), Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1),
} }
} }
@ -93,6 +93,21 @@ impl Type {
free_vars_with_context(&Context::default(), self) free_vars_with_context(&Context::default(), self)
} }
pub fn subst(&self, var: impl AsRef<str>, replacement: &Type) -> Type {
let var = var.as_ref();
match self {
Type::Unit => Type::Unit,
Type::Var(n) if n == var => replacement.clone(),
Type::Var(n) => Type::Var(n.clone()),
Type::Existential(s) => Type::Existential(s.clone()),
Type::Polytype(a, t) => Type::Polytype(a.clone(), Box::new(t.subst(var, replacement))),
Type::Arrow(a, b) => Type::Arrow(
Box::new(a.subst(var, replacement)),
Box::new(b.subst(var, replacement)),
),
}
}
} }
#[derive(Clone)] #[derive(Clone)]
@ -214,4 +229,19 @@ impl Context {
pub fn has_existential(&self, name: impl AsRef<str>) -> bool { pub fn has_existential(&self, name: impl AsRef<str>) -> bool {
self.lookup_existential(name).is_some() self.lookup_existential(name).is_some()
} }
pub fn unsolved_existentials(&self) -> HashSet<String> {
let mut unsolved = HashSet::new();
for entry in self.0.iter() {
match entry {
ContextEntry::ExistentialVar(n) => {
unsolved.insert(n.clone());
}
_ => {}
}
}
unsolved
}
} }

View file

@ -16,8 +16,8 @@ fn test_id() -> Result<()> {
let id = id_term!(); let id = id_term!();
let ctx = Context::default(); let ctx = Context::default();
let (ty, out_ctx) = synthesize(&ctx, &id)?; let (ty, out_ctx) = synthesize(&ctx, &id)?;
let ty2 = app_ctx(&out_ctx, &ty)?; println!("Synthesis result: {ty:?} | {out_ctx:?}");
println!("Result: {:?}", ty2);
Ok(()) Ok(())
} }
@ -26,6 +26,7 @@ fn test_id_of_unit() -> Result<()> {
let id = id_term!(); let id = id_term!();
let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit)); let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit));
let ctx = Context::default(); let ctx = Context::default();
bail!("Result: {:?}", synthesize(&ctx, &id_of_unit)); bail!("Result: {:?}", synthesize(&ctx, &id_of_unit));
Ok(()) Ok(())
} }