thesis

• tiny functions, of a specified type, and made of widely-used other functions, are interesting

• we can study really simple functions at first, like of the form f . g . h

• there are certain things that are uninteresting tho

  • (id x) should always just be x
  • but like (repeat id) could be interesting

• but id is useful in other cases

tinyness

• it's probably cooler to count total function count (f . g . lolo -> 5)

scope

• we won't be treating defining new data types..

• but we'll have to include some data types like list.. data List a = Empty | Cons a (List a)

• we have to separate functions and constants even tho they are really same in haskell..

wheel

• i think this is pretty different from djinn that just finds a function without making any reference to haskell standard functions

• in same way different from coq which is just mega-djinn right

• we are repeating type inference, not sure if we could make use of ghc's or typing-hs-in-hs.. i don't know why they have tycons etc..

• breadth search is only way to find all possibilities in inf space, (but can use inf space), but there can still be some depth heuristics for efficiency etc

f g :: a means f :: b -> a and g :: b a and b can be arrow types

f g :: a1 -> a2 means f :: b -> (a1 -> a2) and g :: b

id :: a -> a const :: a -> b -> a flip :: (a -> b -> c) -> b -> a -> c (.) :: (a -> b) -> (b -> c) -> a -> c repeat :: a -> List a map :: (a -> b) -> List a -> List b (+) :: Int -> Int -> Int

example: f :: a -> a -> b f = id g where g :: a -> a -> b f = const g where g :: a -> b f = flip g where g :: a -> a -> b f = (.) g impossible f = repeat g impossible f = map g impossible f = (+) g impossible

example: f :: a -> b -> b -> c f = id g where g :: a -> b -> b -> c f = const g where g :: a -> a -> b f = flip g where g :: a -> b -> a -> c f = (.) g impossible f = repeat g impossible f = map g impossible f = (+) g impossible

Var 1 :-> (Var 2 :-> (Var 2 :-> Var 3))

id: Right (Var 1 :-> (Var 2 :-> (Var 2 :-> Var 3))) const: Right (Var 1 :-> (Var 2 :-> (Var 2 :-> Var 3))) flip: Right (Var 1 :-> (Var 2 :-> (Var 2 :-> Var 3))) (.): Right ((Var 1 :-> Var 2) :-> (Var 1 :-> (Var 3 :-> Var 4)))

f :: a -> b -> b -> c g h :: (a -> a) -> a -> b -> c