Type-safe and static higher-order functions

yihozhang commented 1 month ago

The current implementation of higher-order functions (#348) does only a best-effort type checking: It works well for functions, but does little for primitives. This PR fixes this by statically check the type even for primitives. Moreover, we no longer rely on get_sort_from_value to get the dynamic type of a value for unstable-fn, which will unblock #448.

Moreover, the previous type checking for higher order functions is bad because the type of a primitive is derived by looking at the argument. This PR changes that by introducing a concept similar to constexpr: (# "a") is a value of type Const<"a"> and is the only inhabitant of this type. This way, the type of (unstable-fn (# "*")) can be determined by pure type-level inspection. This allows us to guarantee ResolvedCall::from_resolution can infer which primitive to take with only the types of the arguments. Imagine otherwise, from_resolution cannot determine the type of (unstable-fn "+" 1) if all it sees it that the arguments have type (String, i64) (instead of (Const<"+">, 1))

More specifically, this PR does the following:

Let Instruction takes a SpecializedPrimitive instead of a Primitive so we can pass down the type information when applying a primitive (this gets rid of the need for get_sort_from_value
Introduce a sort for type-level constants ConstSort and its constructor #.
To enable static type checking, I have to introduce another type constraint called LazyConstraint, that will be applied only when the type of certain variable becomes known. This also requires adding lifetime annotation to Constraint because we need to ensure TypeInfo is still available during the delayed constraint generation.

codspeed-hq[bot] commented 4 weeks ago

CodSpeed Performance Report

Merging #452 will not alter performance

_{Comparing yihozhang-typesafe-higher-order-functions (1c5b0c7) with main (b0db068)}

Summary

✅ 6 untouched benchmarks

yihozhang commented 4 weeks ago

No one asked for it but here's something you can do (type-safely) :laughing:

;; name of the higher-order function defined elsewhere
(sort i64i64->i64 (UnstableFn (i64 i64) i64))

(relation ints (i64))
(rule ((= x (unstable-fn y))
       (= y (# "+")))
      ((ints (unstable-app x 1 2))))

(run 1)
(print-function ints 10) ;; (ints 3)

;; unstable-fn^2
(sort lazyi64 (UnstableFn () i64))
(sort i64i64->lazyi64 (UnstableFn (i64 i64) lazyi64))

(let lazy (unstable-fn (# "unstable-fn") (# "+")))
(extract (unstable-app (unstable-app lazy 1 2))) ;; 3

saulshanabrook commented 4 weeks ago

Thanks for these changes! I was wondering if you would be down to add some more tests to show whats now possible or at least what errors are caught at type checking time now.

I had an idea looking at this that it might be possible to remove the additional # function and ConstSort, but preserve the sorts being passed to apply to remove the need for get_sort_from_value and the deferred typechecking piece...

Alex-Fischman commented 4 weeks ago

If we pass sorts to apply (which is I guess not as large a change as I thought, although this PR is the same size as #448) then that unblocks #448 on its own.

yihozhang commented 4 weeks ago

@saulshanabrook @Alex-Fischman

Right, this PR actually does two separate but related things:

Pass the type information we obtained from type checking/type resolution to apply, so that we can get rid of get_sort_from_value. This is only a few dozen of LOCs.
Making the type checker for higher-order functions sound. This requires # and LazyConstraint. This is about 200 LOCs, and the rest is just interface changes of apply.

As for if # is necessary, I didn't use # in the first place, and found myself having to do a lot of hacks in order to make type-checking sound: 1) we can only infer a type of a primitive when we know both the argument types and the argument expressions (something already done in the existing implementation) and more critically 2) Primitive::accept also need to take the values of argument expressions to fully determine the types because of 1. It also requires some hacks to get these values in some cases (e.g., in call_fn), and the resulting system will be more restrictive than in this PR.

This is not to say we don't have any hacks in this PR. Notably, because of the way we implement this, to get the type of (# "a"), the type checker does need to look at the value of its argument "a". A better approach is to support #a as a constant at the parser level, so we don't need to go through the primitive mechanism. This is a bigger change and we can implement it in the future. However, in this implementation, having this # as a single utility for supporting type dispatching on "literals" already seems to be a good idea.

egraphs-good / egglog