3 ms·

Thanks for Datafun where can I start to learn more about the syntax you are using on the README.md?

by gnocchi 11y ago

rntz 11y ago
Hm, which bits of syntax are you confused by in particular? At the beginning, when defining what types, expressions, contexts, etc. looks like. I use a bunch of BNF (https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form). I'm afraid I don't actually know a good introduction to BNF. The clearest account I know of of the most critical part of my notation, namely inference rules (those things with the big horizontal bars), is in Frank Pfenning's notes for his course on Constructive Logic: http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/02-natded.pdf http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/02-natd... (the full course of notes is at http://www.cs.cmu.edu/~fp/courses/15317-f09/schedule.html http://www.cs.cmu.edu/~fp/courses/15317-f09/schedule.html, but the one I've linked is most relevant) A lot of the rest of my notation (types like A × B, A → B, expressions like λx.e, the judgment Δ;Γ ⊢ e : A meaning "e has type A in context Δ;Γ", and the inference rules themselves) is borrowed from fairly standard type-theory-of-functional-languages stuff. Standard books to read here are Types and Programming Languages by Benjamin Pierce (https://www.cis.upenn.edu/~bcpierce/tapl/); https://www.cis.upenn.edu/~bcpierce/tapl/); or Practical Foundations for Programming Languages by Bob Harper (https://www.cs.cmu.edu/~rwh/plbook/book.pdf https://www.cs.cmu.edu/~rwh/plbook/book.pdf). Those are pretty heavy books that cover a lot of ground, including stuff that's mostly irrelevant to my work. If you're interested, though, they're a great place to start learning about formal PL theory! Was there anything else in particular you wanted to know about?
- gnocchi 11y ago
  Thank you, this is perfect to get started, I've been programming for a long time and I couldn't extract enough meaning. I've heard about the BNF notation with the recent news about Peter Naur death and before but never took to time to get my head around. I think your description of Datafun and the references you gave me are good and enough to make me learn something new and to understand your project.

Thanks for Datafun where can I start to learn more about the syntax you are using on the README.md?

by gnocchi 11y ago

Thanks for Datafun where can I start to learn more about the syntax you are using on the README.md?

rntz 11y ago

Hm, which bits of syntax are you confused by in particular? At the beginning, when defining what types, expressions, contexts, etc. looks like. I use a bunch of BNF (https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form). I'm afraid I don't actually know a good introduction to BNF. The clearest account I know of of the most critical part of my notation, namely inference rules (those things with the big horizontal bars), is in Frank Pfenning's notes for his course on Constructive Logic: http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/02-natded.pdf http://www.cs.cmu.edu/~fp/courses/15317-f09/lectures/02-natd... (the full course of notes is at http://www.cs.cmu.edu/~fp/courses/15317-f09/schedule.html http://www.cs.cmu.edu/~fp/courses/15317-f09/schedule.html, but the one I've linked is most relevant) A lot of the rest of my notation (types like A × B, A → B, expressions like λx.e, the judgment Δ;Γ ⊢ e : A meaning "e has type A in context Δ;Γ", and the inference rules themselves) is borrowed from fairly standard type-theory-of-functional-languages stuff. Standard books to read here are Types and Programming Languages by Benjamin Pierce (https://www.cis.upenn.edu/~bcpierce/tapl/); https://www.cis.upenn.edu/~bcpierce/tapl/); or Practical Foundations for Programming Languages by Bob Harper (https://www.cs.cmu.edu/~rwh/plbook/book.pdf https://www.cs.cmu.edu/~rwh/plbook/book.pdf). Those are pretty heavy books that cover a lot of ground, including stuff that's mostly irrelevant to my work. If you're interested, though, they're a great place to start learning about formal PL theory! Was there anything else in particular you wanted to know about?

gnocchi 11y ago
Thank you, this is perfect to get started, I've been programming for a long time and I couldn't extract enough meaning. I've heard about the BNF notation with the recent news about Peter Naur death and before but never took to time to get my head around. I think your description of Datafun and the references you gave me are good and enough to make me learn something new and to understand your project.