3 ms·

Previous discussion on /r/haskell: https://www.reddit.com/r/haskell/comments/3s93w1/a_selfinterpreter_for_fomega/ https://www.reddit.com/r/haskell/comments/3s9

by Kutta 9y ago

Previous discussion on /r/haskell: https://www.reddit.com/r/haskell/comments/3s93w1/a_selfinterpreter_for_fomega/ https://www.reddit.com/r/haskell/comments/3s93w1/a_selfinter... To summarize, there are a number of different notions of self-interpretation. The strongest notion is interpreting from raw untyped syntax (which entails that the input is first type checked and some failing result is returned if it's invalid). This can be relatively easily proven to be impossible in any total language. The weakest notion of interpretation is the no-op embedding: quoted terms are terms themselves and self-interpretation is the identity function. The weakest self-interpreter is trivial to implement but useless. The strongest one is very useful but impossible. The paper presents something which is weak enough to be possible but strong enough to be useful. It essentially Church encodes the terms of System F-omega as a fold over their structure. This makes it possible to implement pretty printers or structural equality. However, in this scheme all quoted terms are well-typed to begin with, also, quotation can not be invoked at runtime and is available through external preprocessing step only.

meric 9y ago
This can be relatively easily proven to be impossible in any total language. What about in the case of machine language? A valid input is a valid binary, and you can use machine language to parse binaries. I suppose one could argue machine language is implemented by the processor and it cannot interpret hardware, therefore it is not self-interpreting.
- yorwba 9y ago
  Machine language can interpret itself all right, but its not a total language. A language is total if every program stops eventually with some output. Since machine language allows infinite loops, the theorem about self-interpretation does not apply.
mietek 9y ago
> This can be relatively easily proven to be impossible in any total language. Please provide this proof.
- Kutta 9y ago
  f :: String -> () f g' = case (eval g' :: Maybe (String -> ())) of Just g -> g g' Nothing -> () loop :: () loop = f (quote f)
  - mietek 9y ago
    Your sketch of a proof does not appear substantially different from the proof given in section 3.1 of the linked paper. Section 3.2 explains that this result does not apply to strongly normalising languages. 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 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/004343.html 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_mcbride_hasochistic_containers/cs11ppm/?context=3 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.
    - Kutta 9y ago
      I am familiar with all of your listed sources (even attended one incarnation of the Érdi Gergő talk). 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.
      - mietek 9y ago
        It is great that you are interested in the subject. Please consider joining ##dependent on Freenode IRC.

by Kutta 9y ago

meric 9y ago

This can be relatively easily proven to be impossible in any total language. What about in the case of machine language? A valid input is a valid binary, and you can use machine language to parse binaries. I suppose one could argue machine language is implemented by the processor and it cannot interpret hardware, therefore it is not self-interpreting.

yorwba 9y ago
Machine language can interpret itself all right, but its not a total language. A language is total if every program stops eventually with some output. Since machine language allows infinite loops, the theorem about self-interpretation does not apply.

mietek 9y ago

> This can be relatively easily proven to be impossible in any total language. Please provide this proof.

Kutta 9y ago
f :: String -> () f g' = case (eval g' :: Maybe (String -> ())) of Just g -> g g' Nothing -> () loop :: () loop = f (quote f)
- mietek 9y ago
  Your sketch of a proof does not appear substantially different from the proof given in section 3.1 of the linked paper. Section 3.2 explains that this result does not apply to strongly normalising languages. 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 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/004343.html 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_mcbride_hasochistic_containers/cs11ppm/?context=3 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.
  - Kutta 9y ago
    I am familiar with all of your listed sources (even attended one incarnation of the Érdi Gergő talk). 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.
    - mietek 9y ago
      It is great that you are interested in the subject. Please consider joining ##dependent on Freenode IRC.