Expand description

(representation) Polymorphically-typed lambda calculus.

Examples

use polytype::{ptp, tp};
use programinduction::{Task, lambda::{task_by_evaluation, Language, SimpleEvaluator}};

fn evaluate(name: &str, inps: &[i32]) -> Result<i32, ()> {
    match name {
        "0" => Ok(0),
        "1" => Ok(1),
        "+" => Ok(inps[0] + inps[1]),
        _ => unreachable!(),
    }
}

let dsl = Language::uniform(vec![
    ("0", ptp!(int)),
    ("1", ptp!(int)),
    ("+", ptp!(@arrow[tp!(int), tp!(int), tp!(int)])),
]);

// task: sum 1 with two numbers
let tp = ptp!(@arrow[tp!(int), tp!(int), tp!(int)]);
let examples = vec![(vec![2, 5], 8), (vec![1, 2], 4)];
let task = task_by_evaluation(SimpleEvaluator::from(evaluate), tp, &examples);

// solution:
let expr = dsl.parse("(λ (+ (+ 1 $0)))").unwrap();
assert!(task.oracle(&dsl, &expr).is_finite())

Structs

Enums

Traits

  • A specification for evaluating lambda calculus expressions in a domain.
  • Like Evaluator, but you get to decide whether certain arguments should be evaluated.

Functions

Type Aliases