In following post I saw
def increment (x : Nat) : Nat :=
x + 1
theorem increment_is_larger (x : Nat) :
increment x > x := by
exact Nat.lt_succ_self x
And I was wondering how close could I get in PHP.
Explain Lean like I'm an eighteen year old
Lean is a language that is a language where tests are a part of the code that gets compiled as you can see in the example.
With the usual programming languages there is the code, and separate from it there is the mental model that is part in the tests and part in the documentation.
One of the biggest reasons for bugs is that the tests didn't check all options of the mental model, or that the documentation has diverged from the code.
This has become a bigger problem with the use of AI because of the mountain of code, tests and documentation it can generate.
This is were Lean tries to bundle the code and the mental model together, which makes it easier for humans and AI to spot errors.
Building a similar concept in PHP
Compiling ahead of time is not going to happen in PHP. The closest that it can get is describing the theorem close to the function or method.
This is a job for an attribute.
In Lean all argument values and outputs will be checked at runtime. But in PHP the attribute will be used by a runner.
#[Attribute(Attribute::TARGET_FUNCTION | Attribute::TARGET_METHOD | Attribute::IS_REPEATABLE)]
class Theorem
{}
#[Theorem]
function increment(int $int) : int
{
return $i + 1;
}
The Theorem attribute without arguments could be used to run a randomised argument type and/or output type test.
Nat in Lean is a natural or positive integer. In PHP I'm going to create an Input interface with a value method. The Theorem attribute is going to have an $inputs argument which uses the interface.
For the proof check the PHP 8.5 feature Closures and First-Class Callables in Constant Expressions comes in handy.
Every proof needs a description to distinguish the theorems.
#[Attribute(Attribute::TARGET_FUNCTION | Attribute::TARGET_METHOD | Attribute::IS_REPEATABLE)]
class Theorem
{
private $inputs = [];
public function __construct(
public string $description,
public Closure $proof,
Input ...$inputs,
)
{
$this->inputs = $inputs;
}
/**
* @return Input[]
*/
public function getInputs(): array
{
return $this->inputs;
}
}
interface Input
{
public function value();
}
class NaturalNumber implements Input
{
public function value(): int
{
return rand();
}
}
#[Theorem(
'is higher',
static function(Input $input, mixed $output) : bool { return true; },
new NaturalNumber(),
)]
function increment(int $int) : int
{
return $i + 1;
}
I decided for the NaturalNumber to use a random number. The benefit is that the input mutates, which could surface bugs that where not in frame when adding the theorem. The consequence is that the input needs to be shown to create a repeatable theorem.
Now for the runner. Because it is a POC I'm going to create a runFunctionTheorems function that accepts a function as a string.
And it is going to return the function and theorem description as the key and the theorem proof as the value of an array.
function runFunctionTheorems(string $function)
{
if(!is_callable($function)) {
throw new InvalidArgumentException("$function is not a function");
}
$functionReflection = new ReflectionFunction($function);
$theoremReflections = $functionReflection->getAttributes(Theorem::class);
if(count($theoremReflections) == 0) {
throw new InvalidArgumentException("$function has no Theorem attributes");
}
$results = [];
foreach($theoremReflections as $theoremReflection) {
$theorem = $theoremReflection->newInstance();
$inputs = array_map(fn($i) => $i->value(), $test->getInputs());
$actual = $functionReflection->invoke(...$inputs);
$results["$functionReflection->name $test->description"] = ($test->proof)(count($inputs) == 1 ? $inputs[0] : $inputs, $actual);
}
return $results;
}
$result = runFunctionTheorems('increment');
var_export($result);
// result
array (
'increment is higher' => true,
)
The next iteration will probably be a DTO that changes the runner function output into an array with that type of DTO's. This makes it possible to add the inputs and show the values when the proof has failed.
Conclusion
I have written big test suites and I'm wondering if is going to be feasible to add every possible type of test to the code.
Having the tests in the code makes it harder to overlook them. My usual workflow is to open the test file and have the code file in a split-screen.
I think having them in one file is a focus improvement.
The consequence of having the tests in the code is that the runners should not be active in production. And that also means there are attributes that are going to be compiled without any benefit.
There could be a build step that removes the attributes, but then the line numbers don't match with the development code. A solution for that problem is a sourceMap file.
So having the tests separate from the code gives the best cross environment debugging experience.
Even this simple function test runner has shown me how much work it is to create a test library. And we should thank the people who took that job upon their shoulders every day.
Top comments (0)