Speaking of "Recursion Without Really Recursing" and deep magic, check out this Scala-related paper, "Towards Strong Normalization for Dependent Object Types (D

Speaking of "Recursion Without Really Recursing" and deep magic, check out this Scala-related paper, "Towards Strong Normalization for Dependent Object Types (DOT)": http://drops.dagstuhl.de/opus/volltexte/2017/7276/pdf/LIPIcs-ECOOP-2017-27.pdf http://drops.dagstuhl.de/opus/volltexte/2017/7276/pdf/LIPIcs... Here, some choice quotes from it: "We further showed that certain variants of DOT’s recursive self types can be integrated successfully while keeping the calculus strongly normalizing. This result is surprising, as traditional recursive types are known to make a language Turing-complete." "What is the minimum required change to achieve Turing-completeness? Consistent with our expectations from traditional models of recursive types, we demonstrate that recursive type values are enough to encode diverging computation." "But surprisingly, with only non-recursive type values via rule (TTYP), we can still add recursive self types to the calculus and maintain strong normalization." "Can we still do anything useful with recursive self types if the creation of proper recursive type values is prohibited? Even in this setting, recursive self types enable a certain degree of F-bounded quantification, ..." I wish someone would try to implement Robinson arithmetic (See here: https://en.wikipedia.org/wiki/Robinson_arithmetic https://en.wikipedia.org/wiki/Robinson_arithmetic and here: https://ncatlab.org/nlab/show/Robinson+arithmetic https://ncatlab.org/nlab/show/Robinson+arithmetic ) in this. I don't think it'd work - for what I speculate as somewhat obvious reasons - but it'd seem interesting to see where exactly doing so would fail.