Very dependent functions

Question

A "very dependent function" is a function whose output type at input $n$ depends on its own output values at inputs $k<n$. Is there a precise definition of such things that makes sense in formal dependent type theory (e.g. Martin-Lof Type Theory or the Calculus of Constructions)?

The reference everyone points to for very dependent functions is Hickey's Formal Objects in Type Theory Using Very Dependent Types (section 3). But it looks to me like he only gives a PER-style semantics, not a syntax that stands on its own. In particular, his definition might be implementable in a NuPRL-like proof assistant (maybe --- I don't know enough about such proof assistants to be sure), but it's not clear to me how it could be implemented in a proof assistant like Agda, Coq, or Lean. Is my reading of Hickey correct? Has anyone ever implemented very dependent functions in a proof assistant based on something like MLTT or CoC?

Answer 1

It looks like the rules in Table 1 of Hickey's Formal Objects in Type Theory Using Very Dependent Types (section 3) as cited in the question are syntactic in nature and can be implemented immediately in a tactic-and-realizability-based type theory with refinement types. The rules as written would make typing of terms undecidable even with a separate syntactic form for very-dependent lambdas since it would be necessary to invent a well-founded order for each type and term formation. They would also be rather horrible to write out in full thanks to the $WellFounded_i$ predicate.

To adapt them to actual practical implementation in an intensional type theory, what I think I would do is rely on the structural order. That is, the formation rule for the type $\lbrace f | x : A \to B \rbrace$ would allow multiple arguments inside the braces, but only allow $f$ to be called in a structurally decreasing way just as in structural termination checking. This is much more amenable to syntactic checking and the full power of very dependent types could be recovered via accessibility predicates as in the usual library-based implementation of well-founded recursion. Something like: $$ \frac{\Gamma, \Delta, f : \lbrace f\ |\ \Delta \to B\rbrace \vdash B\ \mathrm{type}\ \text{($B$ structurally decreasing in $\Delta$)}}{\Gamma \vdash \lbrace f\ |\ \Delta \to B\rbrace\ \mathrm{type}} \text{$\lbrace\rbrace$-form} \\ \ \\ \frac{\Gamma \vdash \lbrace f\ |\ \Delta \to B\rbrace\ \mathrm{type} \\ \Gamma, \Delta \vdash B[t/f]\ \mathrm{type} \\ \Gamma, \Delta \vdash t : B[t/f] }{\Gamma \vdash\rho\ \Delta \to t : \lbrace f\ |\ \Delta \to B\rbrace} \text{$\lbrace\rbrace$-intro} \\ \ \\ \frac{\Gamma \vdash \lbrace f\ |\ \overline{x_i : A_i} \to B\rbrace\ \mathrm{type} \\ \overline{\Gamma \vdash t_i : A_i[\overline{t_{j<i}/x_{j<i}}]} \\ \Gamma \vdash u : \lbrace f\ |\ \overline{x_i : A_i} \to B\rbrace \\ \Gamma \vdash B[u/f,\overline{t_i/x_i}]\ \mathrm{type}}{\Gamma \vdash u.[\overline{t_i}] : B[u/f,\overline{t_i/x_i}]} \text{$\lbrace\rbrace$-elim} \\ $$ (for now I've elided the rules for $\beta$, type equality and value equality).

I think https://github.com/UlfNorell/insane implements something similar to this but without the structural recursion restriction, so unsafe.