(really the recuurrences of Expr should be "Expr a b c")
example: let x = y*3-7 in x+y*2
here y comes from the outer/global scope, whereas x is locally defined
semantics
evaluate the definition, then use an extended environment for the body
(first Expr is the definition of the variable, second is the body, where the var is used)
a "syntactic semantics" might be to simply replace the variable by the definition in the body
(but in some cases this would be inefficient, both conseptually and in implementation)
implementation
we need to pass environments in (as for unscoped/free variables), but we also need to locally "update" (or extend) the environment for evaluation of the body expression
Imperative variables
syntax: assignment expressions (or statements) (as in Java)
Expr a b c = ... | Var c | Set c Expr
(really the recuurrence of Expr should be "Expr a b c")
example: ((x:=x+1)*((x*y)-(x:=3))
the ":=" syntax is used in honor of Pascal, to signify that this is a change to the value of the variable, over time, during the evaluation of the expression (thus "imperative")
semantics
we evaluate the right-hand side (RHS) and update the variable in the environment, then pass the updated environment in to the rest of the expression
the order of evaluation becomes crucial, since changes made in one part of the expression may affect the value of other parts
implementation
we need to pass environments in and out of the evaluation of each expression; i.e., we must pass in the environment to supply "current" values of variables, then pass it out again (with the overall value) as they change
we can either write out this "plumbing" explicitly or (in Haskell) we can package up the management of the state in a Monad and use special syntax to hide the plumbing
beyond simple expressions and environments
environments which "change" in this way are often called states or stores
one approach to managing them is to restrict expressions to pure values, and to define an "upper layer" of syntax (often called statements) which include expressions, but have an environment-transformation semantics
eval :: Expr -> Env -> Val
perf :: Stmt -> Env -> Env
Parsing combinators
nature (type) of parsers
in most basic form, a function from strings to values (for some type of values)
String -> a
but we also need to keep track of the "remaining string" left over for the rest of the parse
String -> (a,String)
and, the parse might fail, in which case there is no output at all
String -> Maybe (a,String)
but there might also be multiple possible parses, each with ts own value and remainder
Parser a = String -> [(a,String)]
combinator approach
we define some simple functions in terms of the above type (e.g., to parse a single character)
we then define higher-order functions which combine simple parsers into more complex ones
typical combinators do such things as:
eliminate whitespace (token)
allow either of two alternatives (+++)
parse multiple times with some separator character between (chainl)
parse aprentheses around some other parsed value
monads and parser combinators
used directly, this approach involves a lot of "plumbing" to pass around the remaining strings and to account for the multiplicity of ambiguous parses
we can wrap up the plumbing in a Monad in order to manage it behind the scenes, then use special syntax (do) to hide it
Monads (generally)
Monads are a techniques by which tiresome but necessary "plumbing" in a program can be suppressed or hidden
examples:
environment (or state) during expression evaluation
remaining String and ambiguity/multiplicity during parsing
exceptions or errors during computation (the Maybe monad)
a good metaphor is to think of try/catch blocks in Java: explicit checking of errors after each method call would be tiresome
syntax
in Haskell, Monads are a type class
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
in order to define a monad, we make an instance of a type class
instance Monad Maybe where return = Just Nothing >>= f = Nothing (Just x) >>= f = f x
Haskell includes special syntax for monads (the "do" notation)
example: do { x <- p; y -< q; return f p q }
this syntax is translated into uses of bind and lambda
semantics
the type class tells what functions must be defined (return and bind (>>=)), but it doesn't enforce some necessary properties of these functions (the monad laws)
(return x) >>= f == f x
m >>= return == m
(m >>= f) >>= g == m >>= (\x -> f x >>= g)
Lambda calculus
Introduction and motivations
a formal theory of functions, but one which respects the notion of function as algorithm, i.e., as having a descriptive aspect
(in contrast to the set-theoretic understanding, which codes functions as certain sets of ordered pairs)
Formal syntax
using M,N as meta-variables for terms, and x,y, … for variables:
M ::= x | λx.M | M N
terms are either variables, (lambda) abstractions with a bound variable and a body, or applications of a function to an argument
Abbreviations and conventions
we abbreviate to avoid excessive parentheses, and to consolidate multiple successive lambdas, as follows
λxy.M ≡λx.λy.M
λx.M N ≡ (λx.(M N)) ≠ (λx.M) N
M N P ≡ ((M N) P) ≠ M (N P) [just as in Haskell]
Free variables and substitution
we need to distinguish between variables which occur within a lambda that binds the same variable (bound occurrences) and ones which have no enclosing binding (free variables)
formally, we have a function which tells us the free variables of a term:
FV(x) = {x}
FV(M N) = FV(M) ∪ FV(M)
FV(λx.M) = FV(M) \ {x} [here "\" is set difference: remove x]
less formally, if we encounter a binding of a variable on the way "out" from where it occurs in a term, it is bound; else it is free
free variables must get their meaning from context (e.g., an environment); bound variables gain their meaning from how they are bound
in some sense the actual bound variable used in any context is immaterial: we could change it to another one just as well
(λx.x) is the identity function, but so is (λy.y), as is(λz.z), etc.
this idea gets formalized via the α rule of equality between terms: (λx.M) = (λy. M[y/x] )
Reduction and normal form
in addition to the alpha rule above, we have beta (β) and eta (η) rules which relate equal terms
β: (λx.M) N = M [N/x]
η: (λx.M x) = M (if x is not free in M)
the eta rule can be read to imply that "everything is a function", since any term is equivalent to an overt (lambda) function
the beta rule is used to reduce (or compute, or evaluate) terms
every time we see an abstraction as a function "next to" an argument term, we can reduce according to the rule
if we do so repeatedly (and according to a certin strategy), we will eventually arrive at an answer, if possible
the strategy (called normal order) is to reduce the leftmost/outermost such term first
if we reduce arguments to a function first, we may needlessly evaluate them (as the function may not depend on them)
in general, reduction may not terminate
consider the term (λx. xx)(λx. xx): it reduces to itself
Lambda calculus—representations
general idea
just as we can encode numbers, booleans, functions, etc. in set theory, we can do so in lambda calculus
when we do this, we must still recognize that everything in (pure, untyped) lambda calculus is a function (by the eta rule)
without a type system (or at least careful choices, or even just good luck), we may end up "mixing" representations
(e.g., adding a boolean to a number)
the following definitions are coherent in the sense that the operations given will yield correct answers on the representations of their arguments
see the Church encoding page in the on-line references for more information
representing booleans
True ≡λxy.x [given two things, pick the first]
False ≡λxy.y [given two things, pick the second]
If B then M else N ≡ B M N [given two things, pick the one specified by B]
representing natural numbers
Zero ≡λfx.x = (λf. (λx.x)) [given a function, return a function which applies it zero times, i.e. just the identity]
One ≡λfx. f x [given a function, return a function which applies it once]
Two ≡λfx. f (f x) [given a function, return a function which applies it twice]
Etc.
plus ≡λmn. (λfx. m f (n f x))
times ≡λmn. (λfx. n (m f) x)
exp ≡λmn. (λfx. n m f x) ≡ λmn. n m
representing pairs
<M,N> ≡λb. b M N [a pair is a function on Booleans]
fst M ≡ M True
snd M ≡ M False
representing recursion
we can represent recursion using a special term Y (also called the Y combinator)
Y has the property (for all terms F) that Y F = F (Y F)
Y = λf. (λx. f (x x)) (λx. f (x x))
Types—general issues
types arise naturally through the use of encodings/representations
in set theory
in lambda calculus
in bit-strings
types are forced by presence of constants
so far we have seen “pure” systems of lambda calculus (and set theory)
once we add constants “from the outside”, we need types since constants aren’t functions
of course, even with encodings, types are helpful, since they help avoid accidental “mixing” of codes
what types buy us (and cost us)
freedom from “obvious” errors
static typing (vs. dynamic typing) and strong typing
static means that we can determine type correctness by static (compile-time) analysis of program
strong means “no type mis-matches”; we may need to use dynamic (run-time) checks
esp. if statically typed, we can avoid “embarrassment” of run-time type failures
types constitute a useful tool for “coarse-grained”, high-level descriptions of systems
useful locus of information in “sketches” of a system design
allow for documentation of intended behavior (e.g., can see how to use a function)
give a coarse-grained partial correctness proof (e.g., “units” calculations)
provide interface description for interpretation by linkers, compilers
freedom from paradox
Russell first proposed types to resolve set-theoretic paradoxes
most paradoxes arise from reflection plus “negation”
consider adding logical constants T, F, λ to lambda calculus
define P = λx. not(x x); then P P = not(P P)
alternatively, in any system with recursion, define Q = æQ
termination and “analyzability”
for most of the simpler type systems, reduction will always terminate
… this means that equality is decidable (!), unlike for functions in general
furthermore, we will be able (generally) to decide type-correctness statically
but, types impose limitations on the expressiveness of our language (see below)
Types—type systems
for the bulk of the rules themselves, see the handout from lecture
type statements/judgements
a typing statement or judgement is a formal statement relating a context (Gamma: Γ), a term (M) and a type (tau: τ)
Γ⊢ M : τ
it should be read as stating that the term M has the type tau, assuming the types for free variables given by Gamma
we write the typing context Gamma as a set of variable-type associations, but use it informally as a function
if Γ = {x:τ, y:s, …} then Γ(x) = τ
inference rules and derivations
we give (see handout) a bunch of rules which tell when a certain term has a certain type
for a given term, if we can find a derivation (upside-down tree, or proof) that the term has some type, then it does (and only then)
note that the rules don't tell us how to find such a proof: we need an algorithm (type-checking) to find a proof or reject the term
Types and logic: Curry-Howard correspondence
[this is some new material as requested by Zac, for the exam]
consider a proposition (boolean formula with variables) such as you implemented for Lab 4, but assuming a top-level implication (⇒):
(P&(P⇒Q))⇒Q
(P&Q)⇒(Q&P)
(P∨Q)⇒(P⇒Q)⇒Q
(P∨Q)&(Q⇒R)⇒R [not a tautology!]
we can translate each such proposition into a type, replacing:
boolean variable (P,Q, etc.) by type variables (a,b, etc.)
implication (⇒) by function space (→)
conjunction (&) by cross product or pairing ( (_,_) )
disjunction (∨) by disjoint sum, datatype enumeration or Haskell's Either type (|)
the original formula is a tautology if and only if we can write a function (in a pure calculus, no undefined) of the corresponding type
the function is called a witness for the type (and thus for the corresponding formula)
app :: (a, a→b) → b app (x, g) = g x
swap :: (a,b) → (b,a) swap (x,y) = (y,x)
ifapp :: (a | b) → (a→b) → b ifapp (Left x) g = g x ifapp (Right y) g = y
oops :: (a | b, a→c) → c [not a tautology!] oops (Left x) g = g y ifapp (Right y) g = … [uh-oh, what to do here?]
some notes
the use of type variables is important: these functions have to be polymorphic, i.e., they must work at all types
note that we don't really need to have an implication/function, but without it, values of variable types don't exist in general
why not? because we don't have undefined values, and thus nothing of a universal/arbitrary type
adding "undefined :: a" is like adding a proof of any arbitrary proposition/formula
just as adding unbounded recursion risks the abyss, so it opens up the logic to inconsistency (every formula is provable)
the program or function we write constitutes a kind of constructive proof of the formula: we show how to:
construct a value of the result type from values of the argument types
and thus how to build a proof of the consequent formula from proofs of the antecedent ones
understanding this correspondence can reinforce both programming and proving skills with intuitions from the "other side"
the given proofs may not be the only ones possible; consider the type of Church numerals in lambda calculus
zero, one, two, three :: ((a→a) → a) → a zero f x = x one f x = f x two f x = f (f x) three f x = f (f (f x))
we can think of these same functions another way just by changing the way we write their type
zero, one, two, three :: (a→a) → (a → a) [now as "one-ingredient" transformers] zero f = id one f = f two f = f ○ f three f = f ○ f ○ f
this idea can be used to develop a system which automatically writes functions of a desired type
