f :: String -> ()
f g' = case (eval g' :: Maybe (String -> ())) of
Just g -> g g'
Nothing -> ()
loop :: ()
loop = f (quote f) f :: String -> ()
f g' = case (eval g' :: Maybe (String -> ())) of
Just g -> g g'
Nothing -> ()
loop :: ()
loop = f (quote f)See also the slides titled “So what about, e.g. Fω instead of ℕ ⇒ ℕ?” in Gergo Erdi’s talk on the subject of the linked paper:
https://gergo.erdi.hu/talks/2015-11-fomega/FOmegaUnquote.pdf
Note that your sketch is one particular variation of a folklore argument, best recalled by Conor McBride in 2003:
https://mail.haskell.org/pipermail/haskell-cafe/2003-May/004...
Here’s what Conor McBride has to say on the subject in 2015:
https://www.reddit.com/r/haskell/comments/38wels/conor_mcbri...
If you are interested in discussing this further, please feel free to contact me privately.
Section 3.2 of the paper absolutely does not say that the result does not hold. The main point of the construction is that typed quoted representations can preserve totality by disallowing diagonal application. Interpreting untyped quoted representations is impossible all the same, which is what I said in grandparent post.
I know Conor's views on total programming and share them, but the 2015 comment is not particularly relevant to the current topic, nor does it reflect on the folklore self-interpreter argument.