This is a part of a series - start at the beginning.
imp requires javascript!
The denotational semantics define what an imp expression means, but it defines the meaning in terms of infinite sets. How can we evaluate those semantics?
The little interactive in this series so far use a simple interpreter that follows the denotational semantics closely. It takes an expression and an environment, and returns either a representation of the value of the expression or an error.
fn eval(expr: Expression, env: &Environment<Value>) -> Result<Value, String> {
...
}
When the type of the expr is finite (doesn't contain a ->) the result of the expression is represented as a finite set. When the type of the expr is maybe-infinite (contains a ->) the result of the expression is represented as a closure.
enum Value {
Set(HashSet<Vec<Scalar>>),
Closure(Name, Expression, Environment<Value>),
}
Why a closure for infinite sets? The motivation is this:
- all maybe-infinite types originate in an abstract operator
- the only way to turn a maybe-infinite type into a finite type is to apply it to something finite
Closures make a good representation for infinite sets because they make abstract and apply easy to implement, and with some trickery we can rewrite all other operations on closures into combinations of abstract, apply and operations on finite sets.
Finite values
Let's get all the easy cases out of the way:
fn eval(env: Fn(Name) -> Value, expr: Expression) -> Result<Value, String> {
Ok(match expr {
expr!(none) => Value::set(vec![]),
expr!(some) => Value::set(vec![vec![]]),
expr!(s) if is_scalar(s) => Value::set(vec![vec![s]]),
expr!(a | b) => eval_union(eval(env, a)?, eval(env, b)?),
expr!(a & b) => eval_intersect(eval(env, a)?, eval(env, b)?),
expr!(a x b) => eval_product(eval(env, a)?, eval(env, b)?),
expr!(!a) => eval_negate(eval(env, a)?),
expr!(a = b) => eval_equals(eval(env, a)?, eval(env, b)?),
expr!(n) if is_name(n) => env(n),
expr!(let n = a in b) => {
let va = eval(env, a)?;
let env2 = |n| if n == n { va } else { env(n) };
eval(env2, expr!(b))
}
expr!(a b) => eval_apply(eval(env, a)?, eval(env, b)?)?,
expr!(n -> a) => {
let closure_env = close_over(env, body.free_names());
Value::Closure(arg, body, closure_env)
}
})
}
fn eval_negate(val: Value) -> Value {
match val {
Value::Set(set) if set.is_empty() => Value::set(vec![vec![]]),
Value::Set(_) => Value::set(vec![]),
_ => unreachable!(),
}
}
fn eval_equals(val1: Value, val2: Value) -> Value {
match (val1, val2) {
(Value::Set(set1), Value::Set(set2)) if set1 == set2 => Value::set(vec![vec![]]),
(Value::Set(_), Value::Set(_)) => Value::set(vec![]),
_ => unreachable!(),
}
}
fn eval_union(val1: Value, val2: Value) -> Value {
match (val1, val2) {
(Value::Set(set1), Value::Set(set2)) => Value::set(set1.union(set2)),
_ => unreachable!(),
}
}
fn eval_intersect(val1: Value, val2: Value) -> Value {
match (val1, val2) {
(Value::Set(set1), Value::Set(set2)) => Value::set(set1.intersection(set2)),
_ => unreachable!(),
}
}
fn eval_product(val1: Value, val2: Value) -> Value {
match (val1, val2) {
(Value::Set(set1), Value::Set(set2)) => Value::set(
set1.iter()
.flat_map(|tuple1| set2.iter().map(|tuple2| concat(tuple1, tuple2))),
),
_ => unreachable!(),
}
}
It's a pretty direct translation of the denotational semantics. Not much more to say about that.
Maybe-infinite values
The remaining cases fall into three groups.
1. Determining whether an arbitrary value contain any tuples is probably not computable in general, so the type system enforces that the arguments of a negate or equals operators must have a finite type.
2. Unions, intersects and products that have a maybe-infinite type can be rewritten at compile time into equivalent expressions that only feature union/intersect/product on arguments with finite type.
3. Applying one arbitrary value to another is probably not computable in general, so the type system enforces that at least one of the arguments to apply must have finite type.
If one argument has a maybe-infinite type and the other has a finite type we can calculate the answer recursively:
f (a | b) => (f a) | (f b)f (a x b) => (f a) b(a -> ...) s => let a = s in ...(Whensis a scalar. Akin to beta-reduction)
In other words, we can map the closure over each tuple in the set and then union all the results together.
fn eval_apply(val1: Value, val2: Value) -> Result<Value, String> {
Ok(match (val1, val2) {
(fun, Value::Set(set)) | (Value::Set(set), fun) => {
let mut result = Set::new();
for tuple in set {
let mut fun = fun.clone();
let mut tuple_iter = tuple.into_iter();
loop {
match fun {
Value::Closure(name, body, mut env) => {
// if fun is a closure, beta-reduce it
// thanks to funify, if fun is a closure we must have scalars remaining
let scalar = tuple_iter.next().unwrap();
let env2 = |n| if n == name { Value::scalar(scalar) } else { env(n) };
fun = eval(env2, body)?;
}
Value::Set(set1) => {
// if fun is a set we can bail out to the easier implementation
let tuple2 = tuple_iter.collect::<Vec<_>>();
for tuple1 in set1 {
let n = min(tuple1.len(), tuple2.len());
if tuple1[..n] == tuple2[..n] {
result.insert(concat(tuple1[n..], tuple2[n..]));
}
}
break;
}
}
}
}
Value::Set(result)
}
_ => unreachable!(),
})
}
An additional complication is that in the case of partially applied closures, the intermediate results would still be closures and we wouldn't be able to represent their union. So there is an additional compile-time rewrite for partial applications that delays execution until we can represent the result as a finite set.
A smarter rewrite would generate less boilerplate, but this will do for now.
Here is the full set of rewrite rules:
pub fn arity(typ: ValueType) -> usize {
match typ {
typ!(none) => panic!("none has no arity"),
typ!(maybe) => 0,
typ!(_ x b) | typ!(_ -> b) => 1 + arity(b),
}
}
pub fn fun_arity(typ: ValueType) -> usize {
match typ {
typ!(none) => panic!("none has no arity"),
typ!(maybe) | typ!(_ x b) => 0,
typ!(_ -> b) => 1 + fun_arity(b),
}
}
pub fn funify(expr: Expression) {
// apply funify to each direct subexpr
expr.visit1(|expr| {
expr.funify()
});
let typ = get_typ(expr);
if let ValueType::None = typ {
// only one possible value for this type
return expr!(none);
}
let fun_arity = fun_arity(typ);
if fun_arity = 0 {
// doesn't need funifying
return expr;
}
let names = make_fresh_names(fun_arity);
match expr {
expr!(a | b) => expr!(names.. -> (a names..) | (b names..)),
expr!(a & b) => expr!(names.. -> (a names..) & (b names..)),
expr!(a x b) => {
let a_arity = arity(get_type(a));
let split = min(fun_arity, a_arity);
expr!(names.. -> (a names[0..split]..) x (b names[split..]..))
}
expr!(a b) => {
let (f, arg) = if is_function(get_type(a)) {
(a, b)
} else {
(b, a)
};
expr!(names.. -> f (arg x names..))
}
// doesn't need funifying
other => other,
}
}
That's it for the core language. The next few posts will likely come out slower, as we're wading now into parts of the language that I don't have a solid understanding of yet.