Type-safe and static higher-order functions

[yihozhang]

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]

CodSpeed Performance Report

Merging #452 will not alter performance

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

Summary

✅ 6 untouched benchmarks

[yihozhang]

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

;; 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]

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]

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]

@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.

[saulshanabrook]

@yihozhang and I talked on a call about this PR. We discussed that it would be possible to avoid the addition of the new # sort and constructor if we know when calling the get method of TypeConstraint if we are in the checking or the resolution phase. In the checking phase, we can be exact in our type checking of functions, because we know the name of the function based on the term. In the resolution, we can't be exact, because the term is no longer a literal, but that's fine.

We also discussed possible ways the function interface could evolve to make it accessible to users, i.e. what kind of public interface to have. I was hesitant to get closer to something user friendly without just going all the way and allowing functions to be passed as symbols to other functions.

If you still think this it he best approach for the typechecker and for consts long term @yihozhang I defer to you and would support this PR.

I think a few more tests would be helpful to nail down the expected behavior as well, as I said above, so we can be precise about what this change brings.