Searching with first order functions

ScopeSearch.md

We start with a scope (list of names and types n : T) and a specific type A as our goal.

Initial Scope:

f : C -> B
g : D -> B -> A
h : C
i : D

First we convert everything to first order functions, by currying higher order functions, and lifting constant types T to Unit -> T

First order function scope:

f : C -> B
g : D -> (B -> A)
h : Unit -> C
i : Unit -> D

There are 2 kinds of "moves" we can make:

• compose, where we combine x : P -> Q, y : Q -> R into y . x = z : P -> R
• branch, where we turn x : Unit -> (A -> B) into x() = y : A -> B, where () : Unit

Therefore there are only 2 possible compose moves on this scope, with the pairs (f,h) and (g,i):

Move 1: f . h = j : Unit -> B

f : C -> B
g : D -> (B -> A)
h : Unit -> C
i : Unit -> D
j : Unit -> B

Move 2: g . i = k : Unit -> (B -> A)

f : C -> B
g : D -> (B -> A)
h : Unit -> C
i : Unit -> D
j : Unit -> B
k : Unit -> (B -> A)

Since our 2 moves have not revealed any new valid compose pairs, we now have to do a branch move. The only possible branch move is on k, where we do:

Move 3: k() = l : B -> A

f : C -> B
g : D -> (B -> A)
h : Unit -> C
i : Unit -> D
j : Unit -> B
k : Unit -> (B -> A)
l : B -> A

Now we have new pairs (f,l), (j,l) with valid compose moves.

Move 4: l . f = m : C -> A
Move 5: l . j = n : Unit -> A

Unit -> A was our goal, so now we're done.

Now we expand the definition of n based on the moves we made to get there:

n = l . j =  k() . j =  k() . (f . h) =  (g . i)() . (f . h)

And now we apply it to () : Unit to get our concrete A value:

((g . i)() . (f . h))() : A

We can reduce this further by undoing our intial substitions on h and i where now we say

((g . (\u i))() . (f . (\u h)))() : A
(g(i) . (f . (\u h)))() : A
(g(i)(f(h))
g(i,f(h)) : A