on the `infer` function, we usually have something like this:
infer (App f x) ctx =
infer <- infer f ctx
case infer of
All a b -> do
check x a ctx
return $ out arg
otherwise ->
fail
this causes `x : a` to be happen before `infer (f x)` returns `b x`.
this is generally fine, but, in situations such as dependent
eliminations:
λx (bool-elim ?A x t f) : (P x)
we really want `(elim ...)` to return `P x` BEFORE we check `t : ?A
true` and `t : ?A false`. that would allow the unification problem `?A x
== P x` to generate the solution `?A = λx (P x)` **before** the `t : ?A
true` check possibly fails.
being able to fill that metavar is very important for Kind2, since that
would allow us to omit motives in pattern-matches. because of that, I
think that the more sensible order is for infer to return its result
first, and then its inner checks occur. this is via a very lightweight
mechanism that consists of a list of suspended checks (`susp`), which we
push to inside `infer`, and fully consume inside `check`.
this is a middle-ground between checking in order (from left-to-right)
and a more complex suspension mechanism (involving dependency graphs).
with this simple solution, we're able to use metavars inside the motive
of dependent eliminations, greatly reducing the need for annotations in
practical code.
initially, I wanted Kind2 to be bootstrapped, but I'm facing
difficulties, because pure hvm parser is still much slower than the
typescript parser; a few seconds vs instant to parse the entire
codebase. I think HVM2 will need to have proper immutable strings (i.e.,
nodes that expand as if they were cons-strings, but are stored as
buffers) before it can have fast parsers. as such, I'm making the
decision to NOT bootstrap it now. that is a tough decision becase,
honestly, if we don't do it as soon as possible in the development
process, it is very unlikely we'll ever do it. but the tech isn't ready
for it, and we need to move forward, so, that's the only solution.
as such, I'll be rewritting the typescript to Rust, and we'll have a
very similar design to former Kind2, with Rust doing the parsing, IO and
error reporting, and a checker.hvm1 / checker.hvm2 file doing the actual
type-checking (and HOAS-based type-level evaluation).
also, I believe we'll not even generate .hvm from a .kind bootstrap.
while losing types is significant, being able to manually edit the HVM
is very helpful to debugging, it simplifies and accelerates the
development process and removes many complications that are bought by
bootstrapping