JIT type checking for program synthesis

[ngeiswei]

A simple program synthesis experiment reveals the need for a form of Just-In-Time type checking.

The following metta code tries all possible ways to serially compose two unary functions f and g:

;; Define composition operator
(: . (-> (-> $b $c) (-> $a $b) (-> $a $c)))
(= ((. $g $f) $x) ($g ($f $x)))

;; Define functions to compose
(: f (-> Number String))
(= (f $x) (if (== $x 42) "42" "Not-42"))
(: g (-> String Bool))
(= (g $x) (== $x "42"))

;; Test composition via superpose
!(. (superpose (f g)) (superpose (f g)))

However, although only one composition is valid (. g f), it outputs

[(. f f), (. f g), (. g f), (. g g)]

Moving superpose outside of the composition operators makes it clear that the it is due to the lack of dynamicity of the type checker. For instance, the following

!(superpose ((. f f) (. f g) (. g f) (. g g)))

outputs

[(Error f BadType), (Error g BadType), (. g f), (Error g BadType)]

which is what we want.

Replacing superpose with non-determinism via over-definition leads to the same result. For instance:

(= (fns) f)
(= (fns) g)
!(. (fns) (fns))

outputs

[(. f f), (. f g), (. g f), (. g g)]

Finally, although that might be a separate issue, one may notice that

!((. g f) 42)

outputs

[(g '42')]

instead of

True

[Necr0x0Der]

JIT type checking is related to (yet different from) #177 , because when we have a dependently typed function, e.g. (-> (: $t $T) $T) its "real" (JIT) type will depend on the type of the fed argument. For the same reason, it might be relevant to #183 , and also to #181 , which could be solved by JIT types. Thus, it seems that JIT type checking can be an important component to solve different issues.