Add type reconstruction to Adelfa signatures

[cjohnson19]

Writing Adelfa signatures can be quite cumbersome since it requires every term to be explicitly typed. Other systems like Beluga and Twelf will perform type reconstruction to infer terms' types when possible. Having this capability is really essential to accomplish palatable system.

For example, consider the following signature which encodes typing in the lambda calculus:

tp : type.
arr : tp -> tp -> tp.

tm : type.
app : tm -> tm -> type.
lam : tp -> (tm -> tm) -> type.

of : tm -> tp -> type.
of-app: {E1:tm}{E2:tm}{T1:tp}{T2:tp}
        of E1 (arr T1 T2) ->
        of E2 T1 ->
        of (app E1 E2) T2.
of-lam: {E: tm -> tm}{T1:tp}{T2:tp}
        ({x:tm} of x T1 -> of (E x) T2) ->
        of (lam T1 ([x] E x)) (arr T1 T2).

In the of-app and of-lam rules, we have to specify, {E1:tm}, {T1:tp} etc. Yet we can infer their types by their occurrences within later terms. Rewritten to implicitly type these terms, of may be specified as:

of : tm -> tp -> type.
of-app: of E1 (arr T1 T2) ->
        of E2 T1 ->
        of (app E1 E2) T2.
of-lam: ({x:tm} of x T1 -> of (E x) T2) ->
        of (lam T1 ([x] E x)) (arr T1 T2).

Brigitte Pientka has written An insider’s look at LF type reconstruction which describes the method which Beluga uses to accomplish type reconstruction. Adapting this to Adelfa systems should be fairly straightforward -- and purely a challenge of engineering.