If we do decide to continue with Sasquatch, an interesting problem to solve would be that of type induction. How can we start with a type-free or type-impoverished grammar, and learn to add types to it? For example, there are an infinite number of unary functions in the lambda calculus, but only four that operate over the standard encoding of the Booleans (T = \x,y.x, F= \x,y.y). How could we learn about the type of Booleans and use that information to constrain search?
If we do decide to continue with Sasquatch, an interesting problem to solve would be that of type induction. How can we start with a type-free or type-impoverished grammar, and learn to add types to it? For example, there are an infinite number of unary functions in the lambda calculus, but only four that operate over the standard encoding of the Booleans (T = \x,y.x, F= \x,y.y). How could we learn about the type of Booleans and use that information to constrain search?