PL Theory etc

links.md

On Understanding Data Abstraction, Revisited: http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

CLU Reference Manual: http://publications.csail.mit.edu/lcs/pubs/pdf/MIT-LCS-TR-225.pdf

Semantics Engineering with Redex: https://mitpress.mit.edu/books/semantics-engineering-plt-redex

On Understanding Types, Data Abstraction, and Polymorphism: http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf

Practical Foundations of Programming Languages: http://www.cs.cmu.edu/~rwh/plbook/book.pdf

Crash Course on Notation in PL Theory: http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html

Interactive Tutorial of Sequent Calculus: http://logitext.mit.edu/logitext.fcgi/tutorial

Polymorphic Type Inference: http://web.cecs.pdx.edu/~antoy/Courses/TPFLP/lectures/TYPE/typeinf.pdf

Basic Polymorphic Type Checking: http://lucacardelli.name/Papers/BasicTypechecking.pdf

bjz's notes on the lambda calculus: https://gist.github.com/bjz/9595098

ski-log.txt

(On http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html)

 cmr | " It's generally understood that parentheses are allowed in any language. "
 cmr | Is this true in practice?
 cmr | ski: how is the down-arrow in that post read as? I read it as "e evaluates to i", not sure if that's very precise or if there's a better interpretation.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
 ski | yes "e evaluates to i" is a fine rough way to think about it
 ski | "It's generally understood that parentheses are allowed in any language."
 ski | usually, in PL theory, it's true
 cmr | swag
 ski | strictly speaking, grammars deal with words/strings (sequences of symbols/tokens)
 cmr | yeah I know a bit about parsing.
 ski | which in case of a programming language corresponds to the *concrete* syntax of the language
 ski | however, the BNF-like notation used in PLT usually really talk about *abstract* syntax (trees), and hence explicit brackets aren't need
 ski | ed
 ski | do you know any functional programming language ?
 cmr | handful of scheme, spattering of haskell.
 ski | ok, do you understand basic data types in Haskell ?
 cmr | scheme I picked up working through the first ~third of sicp, Haskell I've been slowly working through in spare time.
 cmr | such as Int?
 ski | like e.g. defining binary trees of integers
 cmr | yes.
 ski | ok, fine
 ski | then, think of
 ski |   e ::= i
 ski |       | - e
 ski |       | e + e
 ski | as defining abstract syntax trees, like a data type definition
 ski |   data Expr = Literal Integer
 ski |             | Negate Expr
 ski |             | Add Expr Expr
 cmr | makes sense.
 ski | in practice, we could write
 ski |   e ::= lit(i)
 ski |       | neg(e)
 ski |       | add(e,e)
 ski | (and some do)
 ski | but we usually prefer looking at the "sugared" view above
 ski | with the understanding that we should insert bracketting wherever needed, for complex expression (trees)
 ski | iow, we can't say
 ski |   2 + 3 + - 4
 ski | we'd have to say
 ski |   ((2 + 3) + (- 4))
 ski | e.g., if we mean that
 ski | well, strictly speaking, perhaps even
 ski |   (((2) + (3)) + (- (4)))
 ski | but we quickly decide on the convention that we don't wrap "atomic" subexpressions in brackets
 ski | quickly followed by the convention that we don't both to wrap the whole expression in brackets either (unless we use it inside some other kind of formula, in which case we might still nee
     | those)
 ski | so, then we'd write
 ski |   (2 + 3) + (- 4)
 ski | to describe which abstract syntax tree we mean
 ski | cmr : makes sense ?
 cmr | ski: yes, thanks!
 ski | in short, the BNF-like notation used in PLT (usually) isn't actually about strings (like BNF in grammar normally is about), but rather *trees*
 ski | and therefore we don't need an explicit case for bracketting
 ski | because if we draw them as trees, visually, we don't need any brackets
 ski | we only need them when we want to, unambiguously, represent such a tree in linear text, e.g. like the text in this IRC channel
 ski | in we had subtraction, we might agree that if we write `e_0 - e_1 - e_2', then we mean the tree `(e_0 - e_1) - e_2' rather than the tree `e_0 - (e_1 - e_2)' (here which abbrviation convention
     | choice we make, if any, affects the result we get, starting from a not fully bracketted linear portrayal of some expression tree)
 ski | similarly, we may decide `e_0 + e_1 + e_2' means `(e_0 + e_1) + e_2' rather than `e_0 + (e_1 + e_2)' -- in this case, which choice we make (if any) doesn't affect the result value, starting
     | from a linearized, not-fully-bracketted, expression
 ski | still, as trees, those two are difference, so we need to distinguish them, because one means something like `add(add(e_0,e_1),e_2)' and the other means `add(e_0,add(e_1,e_2))' and those two
     | abstract syntax trees are distinguishable, even though we intend to evaluate or reduce them to the same ultimate result value
 ski | cmr : these latter points may be more or less obvious to you. i mention them in case it wasn't fully clear