5 ms·

Turner, Bird, Eratosthenes: An eternal burning thread

48 points by matt_d 2y ago

nozzlegear 2y ago
I love the name of this paper. It's a play on Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter. https://en.m.wikipedia.org/wiki/Gödel,_Escher,_Bach https://en.m.wikipedia.org/wiki/Gödel,_Escher,_Bach
- deleted 2y ago
  [deleted]
- dtjohnnymonkey 2y ago
  Came here to see if I was just imagining things. Thanks for confirming!
  - memorydial 2y ago
    Glad I wasn’t the only one who saw the reference! Now I just need a version that ties in M.C. Escher’s impossible staircases with infinite loops.
    - osullivj 2y ago
      My mind was boggling over a JMW Turner connection to Hofstadter!? Guess I don't know CS ..
      - intuitionist 2y ago
        I was really excited to see how a 19th-century landscape painter was connected with one of the best NBA players of the 1980s and an Ancient Greek mathematician. Not what I got, but the actual subject is still pretty interesting.
memorydial 2y ago
[flagged]
- deleted 2y ago
  [deleted]
- mrkeen 2y ago
  Turner hoped that we could have programming languages that wouldn't go into (useless) infinite loops. They should either terminate, or keep producing values forever (be 'productive'). The author sets out to prove that Bird's version of the prime number generator (Sieve of Eratosthenes) is productive. Fwiw I'm lost almost immediately in section 4 - the actual proof. I think I get one point, which is to immediately ignore the actual values of the primes, and only prove that they keep being generated (which I guess is the purpose of `approx`), but I'm immediately lost by the overall strategy: that is, not so much showing that primes spec is a fixed point of makeP · makeC, but that it is the least fixed point.
  - boomer_joe 2y ago
    You're interacting with an LLM.
jonstewart 2y ago
My programming languages course in college had a section on Miranda. That’s 25 years ago and I’ve forgotten almost all of it, and I am not a Haskell programmer. But those few weeks proved essential for me and has benefitted my C++ tremendously.
- taolson 2y ago
  I've written a new (self-hosting) compiler for Miranda, with additional features from Haskell and other functional languages: https://github.com/taolson/Miranda2 https://github.com/taolson/Miranda2 and have updated the examples with David Turner's original "sieve" implementation.
  - felixyz 2y ago
    Lovely!
  - 082349872349872 2y ago
    any chance of expanding on doc/Language.md?
    - taolson 2y ago
      Yes, I plan to get to that; I'm currently working on documenting the compiler. I might put a pointer to existing documentation on Miranda there, as a placeholder in the meantime.
      - taolson 2y ago
        [edit to add]: There are also hundreds of small example programs of using Miranda2 to solve Advent of Code puzzles, here: https://github.com/taolson/advent-of-code https://github.com/taolson/advent-of-code Advent of Code Puzzle Descriptions can be found here: https://adventofcode.com/ https://adventofcode.com/ While they don't have the puzzle-supplied data sets included, they can be used to see how various solutions are written in Miranda2.
      - 2y ago
temptemptemp111 2y ago
[dead]
fanf2 2y ago
The author and editor should be ashamed for leaving out O’Neill from the title.
- deleted 2y ago
  [deleted]
082349872349872 2y ago
> Turner said that he was “interested in finding something simpler” than full dependent types. What are some current options for avoiding full dependent types?
- gsf_emergency_2 2y ago
  Lagniappe: https://youtu.be/KBzlkPS7ZUw https://youtu.be/KBzlkPS7ZUw https://arxiv.org/abs/1909.04628 https://arxiv.org/abs/1909.04628 >replace any theory which does not explain symmetrical observational situations as the manifestation of deeper symmetries
  - 082349872349872 2y ago
    now I'd like to see Cambrian knot-fish! is there a slogan for how Spekkens' metaphysics (epistemology?) differs from "working up to isomorphism"? (we prefer theories which result from applying condensation to situations in order to form DAGs? minimise strongly connected components?)
    - gsf_emergency 2y ago
      Not that I know of but maybe! Let me know if you see/come up with one (edit: did you mean "homomorphism"?) The trick to getting yt to return nonLatin recs seems to be: keep only high quality not-dubbed comedy in history.. Edit: maybe he should panned the cam https://youtube.com/shorts/TWLZMVSbi6c https://youtube.com/shorts/TWLZMVSbi6c (What do you mean by "condensation"?)
      - 082349872349872 2y ago
        https://en.wikipedia.org/wiki/Directed_acyclic_graph#Construction_from_cyclic_graphs https://en.wikipedia.org/wiki/Directed_acyclic_graph#Constru...
        gsf_emergency 2y ago

48 points by matt_d 2y ago

I love the name of this paper. It's a play on Gödel, Escher, Bach: An Eternal Golden Braid by Douglas Hofstadter. https://en.m.wikipedia.org/wiki/Gödel,_Escher,_Bach https://en.m.wikipedia.org/wiki/Gödel,_Escher,_Bach

deleted 2y ago
[deleted]
dtjohnnymonkey 2y ago
Came here to see if I was just imagining things. Thanks for confirming!
- memorydial 2y ago
  Glad I wasn’t the only one who saw the reference! Now I just need a version that ties in M.C. Escher’s impossible staircases with infinite loops.
  - osullivj 2y ago
    My mind was boggling over a JMW Turner connection to Hofstadter!? Guess I don't know CS ..
    - intuitionist 2y ago
      I was really excited to see how a 19th-century landscape painter was connected with one of the best NBA players of the 1980s and an Ancient Greek mathematician. Not what I got, but the actual subject is still pretty interesting.

memorydial 2y ago

[flagged]

deleted 2y ago
[deleted]
mrkeen 2y ago
Turner hoped that we could have programming languages that wouldn't go into (useless) infinite loops. They should either terminate, or keep producing values forever (be 'productive'). The author sets out to prove that Bird's version of the prime number generator (Sieve of Eratosthenes) is productive. Fwiw I'm lost almost immediately in section 4 - the actual proof. I think I get one point, which is to immediately ignore the actual values of the primes, and only prove that they keep being generated (which I guess is the purpose of `approx`), but I'm immediately lost by the overall strategy: that is, not so much showing that primes spec is a fixed point of makeP · makeC, but that it is the least fixed point.
- boomer_joe 2y ago
  You're interacting with an LLM.

jonstewart 2y ago

My programming languages course in college had a section on Miranda. That’s 25 years ago and I’ve forgotten almost all of it, and I am not a Haskell programmer. But those few weeks proved essential for me and has benefitted my C++ tremendously.

taolson 2y ago
I've written a new (self-hosting) compiler for Miranda, with additional features from Haskell and other functional languages: https://github.com/taolson/Miranda2 https://github.com/taolson/Miranda2 and have updated the examples with David Turner's original "sieve" implementation.
- felixyz 2y ago
  Lovely!
- 082349872349872 2y ago
  any chance of expanding on doc/Language.md?
  - taolson 2y ago
    Yes, I plan to get to that; I'm currently working on documenting the compiler. I might put a pointer to existing documentation on Miranda there, as a placeholder in the meantime.
    - taolson 2y ago
      [edit to add]: There are also hundreds of small example programs of using Miranda2 to solve Advent of Code puzzles, here: https://github.com/taolson/advent-of-code https://github.com/taolson/advent-of-code Advent of Code Puzzle Descriptions can be found here: https://adventofcode.com/ https://adventofcode.com/ While they don't have the puzzle-supplied data sets included, they can be used to see how various solutions are written in Miranda2.
    - 2y ago

temptemptemp111 2y ago

[dead]

fanf2 2y ago

The author and editor should be ashamed for leaving out O’Neill from the title.

deleted 2y ago
[deleted]

082349872349872 2y ago

> Turner said that he was “interested in finding something simpler” than full dependent types. What are some current options for avoiding full dependent types?

gsf_emergency_2 2y ago
Lagniappe: https://youtu.be/KBzlkPS7ZUw https://youtu.be/KBzlkPS7ZUw https://arxiv.org/abs/1909.04628 https://arxiv.org/abs/1909.04628 >replace any theory which does not explain symmetrical observational situations as the manifestation of deeper symmetries
- 082349872349872 2y ago
  now I'd like to see Cambrian knot-fish! is there a slogan for how Spekkens' metaphysics (epistemology?) differs from "working up to isomorphism"? (we prefer theories which result from applying condensation to situations in order to form DAGs? minimise strongly connected components?)
  - gsf_emergency 2y ago
    Not that I know of but maybe! Let me know if you see/come up with one (edit: did you mean "homomorphism"?) The trick to getting yt to return nonLatin recs seems to be: keep only high quality not-dubbed comedy in history.. Edit: maybe he should panned the cam https://youtube.com/shorts/TWLZMVSbi6c https://youtube.com/shorts/TWLZMVSbi6c (What do you mean by "condensation"?)
    - 082349872349872 2y ago
      https://en.wikipedia.org/wiki/Directed_acyclic_graph#Construction_from_cyclic_graphs https://en.wikipedia.org/wiki/Directed_acyclic_graph#Constru...
      - gsf_emergency 2y ago