Bindings And Functions

Course Videos

Programming Languages CSE341 - Unit 1 (videos)

Formal Method of Understanding PL

Focus on three aspects for a programming expression:

1. Syntax: This is how you write it (keywords and their order)
2. Semantics: This is about what it means (broken into two parts)
   • Type checking: How the expression type checks before program runs
   • Evaluation: How the expression gets evaluated as program runs
3. Idioms: This is about best practices and common styles of using the expression

• Example: Addition Expression
  • Syntax: e1 + e2 where e1 and e2 are expressions
  • Semantics:
    • Type checking: Expression type same as type of e1 and e2 (e1 and e2 must be of same type)
    • Evaluation: Evaluate e1 and e2 to values and evaluate sum of e1 and e2

Variable Bindings

• Program in SML is just a sequence of variable bindings
• Binding is different than assignment as it is immutable
• Introducing a new binding with same name just shadows the earlier binding
• Syntax: val x = expression;
  • On left hand side, you have variable name
  • On right hand side, expression to be evaluated
• Semantics:
  • Type checking: type check expression and extend static environment
  • Evaluation: evaluate expression and extend dynamic enviornment
• Static environment is created before program runs by the type checker and it holds all assigned types
• Dynamic environment is created and updated as program runs by the actual bound values to variables

Using Variables in Expressions

• Syntax: Sequence of letters, digits, _ but not starting with digit
• Semantics:
  • Type checking: Lookup type in current static environment
  • Evaluation: Lookup value in current dynamic environment

Conditional Expressions

• Syntax: if e1 then e2 else e3;
• Semantics:
  • Type checking: e1 -> bool, e2,e2 -> same type ==> expr -> same type as e2,e3
  • Evaluation: Evaluate e1 if true then evaluate e2 else evaluate e3

Function Bindings

• Syntax: fun x0 (x1:t1, ..., xn:tn) = expr; where xn and tn is name and type of param respectively
• Semantics:
  • Type checking: Adds binding to static env x0 : (t1 * ... * tn) -> t where t is type of expression
  • Evaluation: A function is a value. Adds x0 in dynamic env so later expressions can call it.
• The function parameters are in static and dynamic environment for only the expression (scope)

Function Call

• Syntax: val x = x0 x1 ... xn where x0 is function name and x1 ... xn are expressions
• Semantics:
  • Type checking: Checks number of arguments and types of each and compares to the type of function x0 from static env
  • Evaluation: Evaluates each expression to get value which is passed to function as arguments and evaluates function body by getting x0 from dynamic env

Tuples

• Can have fixed number of elements that can have different type
• Syntax: (expr1, ..., exprn)
• Semantics:
  • Type checking: Get type of each expression and extend static env by t1 * ... * tn
  • Evaluation: Evaluate each expression to a value and extend dynamic env by (v1, ..., vn)

Lists

• Can have any number of elements that have same type
• Building List:
  • Empty list []
  • With values [v1, v2, ..., vn]
  • "Cons" operator (prepending element to list) e1::e2 where function type is `a -> `a list (`a is called alpha and can be any type)
• Operations on Lists:
  • null <list> returns true if list empty else false (function type: `a list -> bool)
  • hd <list> returns the first element of list (function type: `a list -> `a)
  • tl <list> returns the whole list except the first element (function type: `a list -> `a list)
• Syntax: [expr1, expr2, ... exprn]
• Semantics:
  • Type checking: Type check each expression and they should have same type t and extend static env by t list
  • Evaluation: Evaluate each expression to a value and extend dynamic env with a list of values

Functions over Lists

fun sum_list (xs : int list) =
    if null xs
    then 0
    else hd(xs) + sum_list(tl xs)

fun countdown (x : int) =
    if x=0
    then []
    else x :: countdown(x-1)

fun append (xs : int list, ys : int list) =
    if null xs
    then ys
    else (hd xs) :: append(tl xs, ys)

Let Expressions

• Introduces local bindings for a sub-expression
• Key idea is that it introduces a scope where bindings are available only local to the sub-expression
• Syntax: let b1 b2 ... bn in e end where b is any binding and e is any expression
• Semantics:
  • Type checking: Type check each b and e in current static env and extend it with type of e which is type of whole let expression
  • Evaluation: Evaluate each b and e in current dynamic env and extend it with result of evaluating e

Lack of Mutation

• In ML, there is no way to change the contents of a binding, a tuple, or a list. If x maps to some value like the list of pairs [(3,4),(7,9)] in some environment, then x will forever map to that list in that environment.
• There is no assignment statement that changes x to map to a different list. (You can introduce a new binding that shadows x, but that will not affect any code that looks up the “original” x in an environment.)
• There is no assignment statement that lets you change the head or tail of a list. And there is no assignment statement that lets you change the contents of a tuple.
• So we have constructs for building compound data and accessing the pieces, but no constructs for mutating the data we have built.
• The biggest benefit of having no mutations is that it makes aliasing irrelevant and we cannot even tell if there is aliasing

For example in function for list append:

fun append (xs : int list, ys : int list) =
    if null xs
    then ys
    else (hd xs) :: append(tl xs, ys)

• We can ask : Does the list returned share any elements with the arguments?
• The answer does not matter because no caller can tell.
• The answer happens to be yes: we build a new list that “reuses” all the elements of ys. This saves space, but would be very confusing if someone could later mutate ys.
• Saving space is a nice advantage of immutable data, but so is simply not having to worry about whether things are aliased or not when writing down elegant algorithms.
• In fact, tl (tail of list function) itself thankfully introduces aliasing (though you cannot tell): it returns (an alias to) the tail of the list, which is always “cheap,” rather than making a copy of the tail of the list, which is “expensive” for long lists