Because one of the principal applications of Type Theory in formalizations has been to study programing languages and computation in general, a lot of thought has gone into ways of representing possibly non-terminating programs.
I won't make a complete survey here, but I'll try and give pointers to the main thrusts of different directions.
- The "relational" approach: you can define your hypothetical programs as relations say, $F\ x\ y$ which holds iff $f$ is defined at $x$ and $f(x)=y$. This is usually what is done with the Kleene T-predicate. This works just as well in type theory formalizations as it does in classical logic, (though of course you can't prove $\forall x (\exists y, F\ x\ y)\vee (\neg\exists y, F\ x\ y)$).
A more sophisticated way to do this is the "Bove-Capretta" method (see Modelling Recursion in Type Theory, which for each recursive function, defines an "accessible predicate" which encodes the fact that a given computation is finite. The function definition takes an extra argument which is a proof that the given inputs are accessible. To define the function without this extra predicate, you need to prove that every possible combination of inputs is accessible.
The "coinductive" approach: this is possibly the most explored approach, and what Andrej's comments refer to. A computation of type $A$ is defined as the inductive type (from Andrej's link, by Capretta, Altenkirch & Uustalu:
codata Delay A =
| Now : A -> Delay A
| Later (Delay A)
This codes a possibly infinite stream of Later tokens ("ticks" of computation) maybe ending with a result Now a. Non-termination is equivalent to being bisimilar with the program
loop = Later loop
and termination can be defined by an inductive predicate over Delay A:
data Terminates : Delay A -> Prop =
| Term_now : forall x, Terminates (Now x)
| Term_later : forall d, Terminates d -> Terminates (Later d)
I think the agda-istas have a lot to say about this which they call the partiality monad (see e.g. Danielsson).$ $
- The "partial type theory" approach: this is a bit more experimental (the theory is still being worked out), but there are some type theories that are being developed to cope with the fact that there are essentially two types of functions we want to write in type theory: the proof terms and the programs. It turns out to be tough to get a reasonable theory of these things (and retain consistency of the theory), but a serious attempt is made here by Casinghino et al, and a similar effort by Kimmel et al.
I'm sure there are other approaches I'm not aware of, and I'd be happy if someone wants to complete this list.
I should probably note that adding a termination oracle to a (consistent) type theory is a lot like adding a truth oracle for $\Pi^0_1$ sentences, with relatively well understood consequences.
There are other, quite fruitful interactions between type theory and complexity theory, usually under the umbrella of implicit computational complexity.
