6
$\begingroup$

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?

$\endgroup$
11
  • $\begingroup$ Related: github.com/UlfNorell/insane $\endgroup$
    – ice1000
    Commented Sep 14, 2022 at 23:32
  • $\begingroup$ Did you ask this because OHTT seems to need this? $\endgroup$
    – ice1000
    Commented Sep 14, 2022 at 23:40
  • $\begingroup$ @ice1000 Why would you think that? $\endgroup$ Commented Sep 15, 2022 at 14:45
  • 1
    $\begingroup$ Thanks. There he says only that it's similar. $\endgroup$ Commented Sep 17, 2022 at 3:15
  • 1
    $\begingroup$ Jason Gross just pointed me to github.com/UlfNorell/insane/blob/master/Sigma.agda#L14-L15, which shows how very dependent functions can be encoded using insanely dependent types, which wasn't clear to me at first. The idea is that insanely dependent types allow functions whose domains behave like (a 'mutual' generalization of) a very dependent function type. One can then reify a single very dependent function type by using it as the domain of the constructor of a datatype. It would be really nice to have a formal description of what exactly is implemented by the "insane" implementation. $\endgroup$ Commented Dec 16, 2022 at 0:39

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ The conclusion of {}-form seems to have an extraneous "$f :$" in the conclusion, and something is wrong with the context in the conclusion of {}-intro. $\endgroup$ Commented Sep 21, 2022 at 8:50
  • $\begingroup$ @AndrejBauer Edited, thanks. $\endgroup$ Commented Sep 21, 2022 at 11:55
  • 1
    $\begingroup$ I have trouble understanding how rules like this would work in practice, and how we can believe that they will be well-behaved. Generally I think of a typechecking algorithm as taking some surface syntax (unchecked term) as input and producing some internal values (checked term) as output. The types appearing in a context, and the type being checked against, are always internal values. But here, in {}-form, you are placing $\{f\mid \Delta \to B\}$ in the context before you've finished typechecking it, so you don't have an internal value to put there. The other rules are similar. $\endgroup$ Commented Dec 15, 2022 at 18:27
  • $\begingroup$ That's indeed the most troubling part of these rules. I don't have a full proof or prototype, but considering the occurrences of $f$ have to be structurally decreasing applications, as long as there's a substitution algorithm for the external form this should work out. A really precise specification of this would have a special part of the context for 'conjectured' $f$ of this sort, and maybe even a special judgement form and a copy of the elimination rule therein. (I've also tried to find some kind of alternate rules that have logical harmony but this is still the best I've come up with.) $\endgroup$ Commented Dec 17, 2022 at 15:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.