Hello!

[viclib]

Hello! What you've doing here is really interesting for me, but I don't really know what it is. You just found automatically the definition of a function by giving a few of its input->output pairs. What exactly are you doing there, how is it called and how can I learn more about it?

Thanks!

[luqui]

Sorry it has taken me so long to reply, I just now cleaned out my inbox.

You can see how it's called in examples.hs. E.g.

add2 :: Integer -> Integer
add2 = f 0 (1+)
    where
    f = search "forall Integer. Integer -> (Integer -> Integer) -> Integer -> Integer" $ \(f :: forall i. i -> (i -> i) -> i -> i) ->
        let f' = f (0 :: Integer) (1+) in
        and [
            f' 0 == 2,
            f' 2 == 4,
            f' 4 == 6
        ]

So this is Haskell code, and if you want to learn about what I'm doing, I suggest you learn some Haskell if you don't already know it. I use some fundamental concepts from the language which aren't as clearly presented in other languages.

The main guidance that my algorithm uses is the type of the generated function. That is

"forall Integer. Integer -> (Integer -> Integer) -> Integer -> Integer"

(which is duplicated in the subsequent lambda as

forall i. i -> (i -> i) -> i -> i)

for technical reasons. These are the same type.)

This function is supposed to be adding 2, so why does it have 3 arguments? It's because in order to add 2, you need some stuff to work with. One of the bases for working with natural numbers is zero and succ (the function that adds 1). So that's what the first two arguments are:

"forall Integer. Integer -> (Integer -> Integer) -> Integer -> Integer"
                 ^^^^^^^     ^^^^^^^^^^^^^^^^^^^^    ^^^^^^^    ^^^^^^^
                 zero       succ                    input      output

Then my algorithm will attempt to combine zero, succ, and input in a way that satisfies the tests. It does not "reverse engineer" the tests -- rather it just tries all the functions of that type until it gets something that passes. Fortunately, the type of a function is often very informative, and reduces the search space drastically.

The search algorithm (Djest/Solver.hs) is where the fun stuff is, and while it's conceptually simple, it takes a lot to pull off -- I don't think I would have been able to do it nearly this easily in any other language. Essentially it just looks at the type and creates terms of that type. Let's work with the type we have been working with as an example (but abbreviated)

forall i. i -> (i -> i) -> i -> i

There are various rules for how to create a term of that type based on the shape of a type, which you can see in rules in the the Solver module. To create a function of forall, we just create a new "rigid" variable and substitute it. Let's call it I. So now we need to create a term of type

I -> (I -> I) -> I -> I

(which, recall, associates as I -> ((I -> I) -> (I -> I)))

Now we use the rArrow rule, which says to create a lambda, and add the domain type to the environment

GOAL :: (I -> I) -> I -> I
result = \x -> [GOAL]
x :: I

The only rule that can still apply is rArrow, so we try it one more time:

GOAL :: I -> I
result = \x -> \y -> [GOAL]
x :: I
y :: I -> I

Now there are a few things that can happen. We already have an answer of the desired type I -> I, which is y, so we can just finish right now, giving:

result = \x -> \y -> y

If this satisfies the tests (it doesn't) then we're done. Otherwise we move on to applying rArrow again from the previous state:

GOAL :: I
result = \x -> \y -> \z -> [GOAL]
x :: I
y :: I -> I
z :: I

So now we have two immediate answers of the desired type, so we try them both and see if they pass the tests

result = \x -> \y -> \z -> x
result = \x -> \y -> \z -> z

(they don't). But there was one more thing we could do, that's the refine rule. y has a type that is compatible with the desired result type, if it had an argument. So we apply rRefine, which means "try applying the function and deducing its arguments", to get

GOAL :: i   -- (this i comes from the domain of `y :: i -> i`)
result = \x -> \y -> \z -> y [GOAL]
x :: i
y :: i -> i
z :: i

leading to two more immedate answers

result = \x -> \y -> \z -> y x
result = \x -> \y -> \z -> y z

neither of which pass the tests, but we can rRefine again:

GOAL :: i   -- again from the domain of `y :: i -> i`
result = \x -> \y -> \z -> y (y [GOAL])
x :: i
y :: i -> i
z :: i

Leading to two more immediate answers

result = \x -> \y -> \z -> y (y x)
result = \x -> \y -> \z -> y (y z)

the latter of which passes the tests, so we have found our function!

There are some technicalities. If you do this search naively, you might not hit all functions; i.e. you might get caught checking an infinite chain, when the solution is somewhere else. Djest/Delay.hs is a "weight" monad that solves this -- with each solution path it associates a weight, and it yields the least weight solutions first. Each time we apply a rule we increment the weight, so we yield all the solutions which apply the fewest rules first, which ensures that we will get to every solution eventually.

Does that help? I'm open to answering more questions. Thanks for your interest!