Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total languages]", to "show that static type checking in Fω can exclude the proof’s diagonalization gadget, leaving open the possibility for a self-interpreter".
There has been some debate [1] over the precise definition of "interpreter" and "self-interpreter" within [0], and more broadly in the field. The general impression I draw from this discussion is that the "representation" and "reduction" of a program are a spectrum, with different evaluators performing different degrees of representation/reduction, partially dependent on the design of the evaluator, as bounded by the capabilities of the implementation language.
However, my question does not concern whether Brown and Palsberg's self-interpreter accomplishes interpretation, but instead whether and how their mechanism of forbidding diagonalization relates to other domains. As analogy, I appeal to Lawvere's Fixed Point Theorem (LFPT), which has been used to unify the presentation of a number of limitative theorems proven using diagonalization methods [2].
Can Brown and Palsberg's evasion of the effects of diagonalization be applied with similar breadth? Can their diagonalization-exclusion mechanism be translated to other diagonalization-based proofs? How does it stand with respect to the preconditions for the Fixed Point Theorem (e.g., does the LPFT simply not apply to the problem of total language self-interpretation)?
A further extension of this question would be to compare Brown and Palsberg's mechanism with Dan Willard's mechanism for avoiding diagonalization in his Self-Justifying Axiom Systems, as is asked in [3].
[0] http://compilers.cs.ucla.edu/popl16/
[1] http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/
