10
$\begingroup$

The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka and the dependently-typed language F-star appear to have a built-in primitive "divergence" effect whose presence is inferred by termination-checking.

From a logical perspective, general recursion leads to inconsistency by allowing the definition of non-terminating programs of type $\bot$, so unrestricted general recursion is unacceptable in a proof assistant. But marking general recursion by a divergence effect in the type system ought to restore logical consistency in the pure fragment. (Of course, in a dependent type theory one also has to decide to what extent types can depend on possibly nonterminating computations, and hence whether the latter may be executed during typechecking.)

Aside from explicit general recursion, non-termination and hence logical inconsistency can also be derived from universe inconsistencies such as $\rm Type:Type$. Has anyone ever considered a dependent type theory / programming language in which universe inconsistencies are permitted but similarly guarded by a built-in effect?

$\endgroup$
14
  • $\begingroup$ I was told that linearity can forbit the construction of Girard paradox but I'm not so sure $\endgroup$
    – ice1000
    Dec 16, 2022 at 21:14
  • $\begingroup$ Linearity prevents most "Russel-like" paradoxes, e.g. the linear set theory with unrestricted comprehension: kurims.kyoto-u.ac.jp/~terui/lastfin.pdf $\endgroup$
    – cody
    Dec 16, 2022 at 22:05
  • $\begingroup$ I'm actually having trouble imagining a "universe guarded" type theory that does not look very much like normal MLTT with universes. Is it possible that the answer is "this is already what we're doing"? $\endgroup$
    – cody
    Dec 16, 2022 at 22:07
  • 1
    $\begingroup$ @cody I'm imagining a type theory in which one could write Girard's paradox as a proof of $\bot ! \mathsf{univ}$, indicating a contradiction involving the effect of universe inconsistency, just as one might have by general recursion a proof of $\bot ! \mathsf{div}$ indicating a contradiction involving the effect of divergence. In normal MLTT with universes, Girard's paradox cannot be given any type. $\endgroup$ Dec 16, 2022 at 23:00
  • 1
    $\begingroup$ Could you just define a Universe ala Tarski using induction-recursion, and then have it refer to itself using general recursion as an effect? Something like the guarded modality. Then you would be able to express Type:Type with the same effect as non-termination $\endgroup$ Dec 17, 2022 at 23:10

1 Answer 1

6
$\begingroup$

I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature.

Some background information

Computational effects and dependent type theories is a topic that has been explored quite a bit, see for instance [1, 2, 3]. I draw attention to the fire triangle paper, which explains the fundamental dilemma one faces when effects and dependent type theory meet.

The immediate idea one has is to express computational effects as a monad $T$, a la Eugenio Moggi. We may also split the monad $T$ into an adjunction $F \dashv U$ with $F : \mathcal{V} \to \mathcal{C}$ and $U : \mathcal{C} \to \mathcal{V}$. We think of $\mathcal{V}$ as value types whose elements are values (“inert data”) and of $\mathcal{C}$ as computation types whose elements are computations (“active code“). This approach is known as call-by-push-value [4].

In programming syntax the unit of the adjunction is written as return, and composition in the Kleisli category of the monad with the do notation.

When computational effects are represented as algebraic operations of an equational theory $\mathcal{E}$, the obvious adjunction $F_\mathcal{E} \dashv U_\mathcal{E}$ is the one induced by the free algebra construction. Languages that use this approach typically use the notation $A ! \mathcal{E}$ for the computation type $F_\mathcal{E}(A)$, and call the algebraic theory $\mathcal{E}$ “effect information“ or “dirt“. (In contrast, a value type $A$ is “pure” because its elements are values, free of effects.) Quite often $\mathcal{E}$ is just a signature, i.e., it has no equational axioms, because those are difficult or impossible to type check algorithmically.

General recursion

Let us apply the above idea to incorporating general recursion into type theory in a safe manner. We equip type theory with a monad $T$ whose purpose is to indicate the possibility of divergence. The elements of $T(A)$ are referred to as “(possibly divergent) computation”. Next, we introduce general recursion operator $$\frac{x : A \vdash e : T A}{\vdash \mathsf{fix}_A(x . e) : T A}$$ and the equation $$\mathsf{fix}_A (x . e) \equiv \mathsf{do} \, \{ x {\leftarrow} \mathsf{fix}_A (x . e) \,;\, e \}.$$ Note that $\mathsf{fix}_A(x . e)$ lands in $T A$. To actually extract the result from $T A$ we need passage back to $A$. How exactly this is accomplished depends on the particularities of $T$, see for instance the delay monad.

$\mathsf{Type} : \mathsf{Type}$?

Type theories with $\mathsf{Type} : \mathsf{Type}$ are perfectly good and intersting, and they play a role in programming language theory, but cannot easily be used propositions-as-types style because $\mathsf{Type} : \mathsf{Type}$ entails inhabitation of every type. One can of course set up some barriers, such as a two-level type theory with logic sitting on top of the “$\mathsf{Type} : \mathsf{Type}$” layer – which kind of misses the point of propositions-as-types.

Perhaps there's one remark I can make that isn't completely devoid of content. In a type theory a la Coq, we can freely pretend to have $\mathsf{Type} : \mathsf{Type}$, and the system generates a set of constraints on universe indices that must be satisfied. But this reminds one of a computation situated in a “context” – to be understood more generally than “typing context”. And this has been studied under the name coeffects, see for instance [5, 6]. The idea is that a computation runs in an envirornment which has certain capabilities (variables, memory layout, communication channels, etc.). A coeffect system describes the capabilities and we can either compute the capabilities required by a program, or check whether a program fits available capabilities. I can well imagine that one could describe "universe capabilities" in this way. In a way Coq does this by computing the universe constraints, and there could be a way of exposing them explicitly in type theory using coeffects.

$\endgroup$
8
  • $\begingroup$ Thanks! I had found most of this already (except for coeffects, which now I need to go read about!), but it's nice to have it laid out so I know I'm not missing something. Do I understand correctly that CBPV solves the "fire triangle" problem by restricting effects to occur in computations whereas dependent elimination happens only on values? $\endgroup$ Dec 18, 2022 at 16:48
  • 1
    $\begingroup$ Someone pleaase summon @pierre-marie-pédrot, I am just going to say something dumb about the fire triangle. $\endgroup$ Dec 18, 2022 at 17:26
  • $\begingroup$ Indeed, dependent elimination is restricted to values. But you also need a way to evaluate value-returning computations while remembering the evaluation in the type, otherwise you would get a fairly boring system without any type-dependency on computations. That's the rôle of the dependent let. $\endgroup$ Dec 20, 2022 at 10:45
  • $\begingroup$ I find it easier to understand what is going on in call-by-name, since this is the normal state of affairs in MLTT. In this case, the one difference introduced by effects is the restriction that the return predicates of eliminators must be linear, i.e. in some sense they must commute with effects. This might seem a bit counter-intuitive when I claimed above that dependent matches must be restricted to values, but this is what you get from the call-by-name embedding into CBPV. $\endgroup$ Dec 20, 2022 at 10:45
  • $\begingroup$ Linearity is precisely ensuring that the predicate does not treat computations differently from values. A prime example of a linear predicate 𝔹 → □ is something like λb. if b then True else False, i.e. a function that evaluates its argument once and for all before proceeding with the rest of the computation. $\endgroup$ Dec 20, 2022 at 10:45

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.