A type is name for collection of related values.
E.g. Bool contains False and True.
e :: t means that e has type t.
Haskell is strongly typed as type errors are found at compile-time.
A list is a sequence of values of the same type: [t] is the type of list with elements of type t.
A tuple is a sequence of values of (possibly) different types: (False, 'a', True) :: (Bool, Char, Bool).
A function is a mapping from values of one type to values of another type: even :: Int -> Bool.
You can do function with muliple arguments or results by using lists or tuples.
Haskell has multiple type classes, e.g.
Num — numeric typesEq — equality typesOrd — ordered totally (linearly) types. Strings, lists, and tuples are lexicographically ordered (same was as words in a dictionary). Comparison occurs like you’d compare strings. One character at a time.Show — types whose values can be converted to strings of charactersRead — types whose values can be converted from strings of charactersIntegral — types that are instances of Num but are integersFractional — types that are instances of Num but are fractional typesYou can also have functions with multiple arguments by returning functions as results.
add' :: Int -> (Int -> Int)
add' x y = x+y -- takes int x and returns function add' x. That takesan integer y and returns x+y.
-- Haskell says the type of add' is add' :: Num a => a -> a -> aIn JS, this would be const add = x => y => x + y.
Conventions
Int -> Int -> Int -> Int means Int -> (Int -> (Int -> Int)).mult x y z means ((mult x) y) z.A function is polymorphic if its type contains one or more type variables.
length :: [a] -> Int is polymorphic. It doesn’t care which type of list you give it. So now a is a type variable.
A polymorphic function is overloaded if its type contains one or more class constraints.
(+) :: Num a => a -> a -> a means for any numeric type a, (+) takes two values of type a and returns a value of type a.
The => defines a class constraint: everything before it is part of the constraint.
An expression can be 3 things: a variable, abstraction, or application.
$\lambda x.e_{1}$ denotes a function with formal parameter $x$ and body $e_{1}$.
Scope of $x$ is all of $e_{1}$, but parentheses can be introduced to delimit scope.
$e_{1}e_{2}$ denotes that function $e_{1}$ is to be applied to argument $e_{2}$.
Scope rules: In $\lambda x.e$, the scope of the Formal parameter $x$ is the body $e$ of that abstraction. We say $x$ is bound in $e$.
But in $\lambda x.xy$, $x$ is bound but $y$ is not—so it’s free.
Beta-reduction
This is the most important rule. There are multiple rules in the reduction relation, but this one is central.
The reduction relation is how an expression can be reduced to some other expression.
It says that if we have the application $(\lambda x.e_{1})e_{2}$, we can substitute the formal parameter $x$ with $e_{2}$ inside the body $e_{1}$.
This is beta-reduction: if we apply a function to an argument, we substitute the formal parameter by the actual parameter. This is the call-by-name parameter mechanism (SS 13 - Parameter Mechanisms).
An expression of this form is called a redex.
A redex is a subexpression for which reduction is possible. If the reduction is a $\beta$-reduction, it’s a $\beta$-redex. It stands for reducable expression.
We need some more rules now:
The left part of the application is what should become a function (abstraction).
We could also reduce to the right component.
In abstraction $\lambda x.e$, the $x$ is called a binding occurrence of $x$. If the same $x$ occurs inside $e$, it’s called a bound occurrence of $x$. A binding occurrence is like a placeholder—the name isn’t important. Just like parameter names in functions, it doesn’t matter what they’re called: they shouldn’t conflict with outside variable names.
If an expression $e_{2}$ can be obtained from some other expression $e_{1}$ by systematically renaming zero or more binding occurrences and their bound occurrences, $e_{1}$ and $e_{2}$ are $\alpha$-convertible, and write $e_{1}\equiv_{a}e_{2}$.
Examples
Applying a function on another expression:
The above gives 49.
Lambda Calculus | Brilliant Math & Science Wiki
Lambda Calculus Calculator
Abstractions are function definitions, and are denoted by $\lambda$. After the symbol you write the input variables, followed by a dot, and then the output of a function where you describe what you want to get (the body of the function).
Variables are the same as variables in programming languages. They contain values. The scope of a variable is defined by its closest function or parentheses. Variables can be free or bound. Bound variables are those used in its scope after it was delared in the closest function input, otherwise it’s free. In the following lambda, $x$ is bound and $y$ is free: $\lambda x.xy$
A Lambda term is a basic entity. It can be a variable or function. So any variable, application, or abstraction is a valid term. These can be given names for easier reusability, e.g. $I := \lambda x.x$, for the identity term.
Alpha conversion (alpha renaming) says that names of bound variables in abstraction can be changed. Variables not bound in abstractions don’t work.
Function is a process of associating input to output. But here, functions are anonymous (can’t be given names), can take only one variable, and are treated as first-class values, so they can be both inputs and outputs of functions.
Application is applying a lambda term to another. To write it, just write the terms with whitespace between them: $x\ y$.
More than 1 argument through currying:
$\lambda xy.x$ becomes $\lambda x.\lambda y.x$.
To make a function that takes multiple arguments, make a function that takes the first argument, and returns a function which takes the second argument and returns an output.
Substitution
Replacing all free occurrences of a variable in the expression with another expression.
Beta-reduction
The process of applying a variable to a function.
Like calling a function with an argument.
E.g. multiplyByFive(2) would look like:
When you apply a function to a term, take the function’s body and run it with the applied argument as an input.
Recursion
A function using itself.
To do this in a language where every function is anonymous, describe a function and then describe it again in its argument:
This is the Y combinator (fix-point combinator).
quango and tango that have the following types; it is not important what the definitions do as long as they are type correctquango :: a -> [a]
tango :: Num p1 => (a, b) -> p2 -> p1Are quango and tango polymorphic? If so, tell us if for each of them if this involves parametric Polymorphism or overloading (ad hoc Polymorphism) or maybe both — and how. If not, tell us why.
quango :: a -> [a]
quango a = [a]
tango :: Num p1 => (a, b) -> p2 -> p1
tango (a, b) p2 = 1Yes, they are. Both involve typed variables.
quango is parametric polymorphism, as it doesn’t matter which value is given as argument, it simply returns a list of that type.
And tango is overloaded as it contains class constraints in its type.
To do this, use the reduction rules of the note.
It reduces to $xy$ and I have no idea why.
twice f x = f(f(x))
-- Initial guess
twice :: f -> x -> f(f x)
-- Actual answer
twice :: (t -> t) -> t -> tIt is parametric polymorphic, as it contains a type variable.
How would you go about figuring this out? First, observe that the function takes two arguments. Since functions in Haskell take exactly one argument, we know that it returns a function which takes the second argument.
So we can infer the following:
So the question is, what is $t_{f}$, $t_{x}$, and $t_{r}$?
Well, in the result, you see a function application, which is an argument of another function application.
We know that $f$ is a function, just from the syntax. So $f:t_{a}\rightarrow t_{b}$
From page 23 in the book. we know that if a function is of type $f::A\rightarrow B$, and its argument has type $x :: A$, then $f\ x :: B$.
So in this case, $x :: t_{a}$ and $f(x) :: t_{b}$.
And $f(f(x))::t_{b}$ and $f(x)::t_{a}$.
Otherwise we couldn’t apply $f$ to $f(x)$.
And from this we observe that $f(x)::t_{b}=t_{a}$. They must be the same type.
So now we know that $t_{r} = t_{a}$, and $t_{x}$ is also $t_{a}$.
And then it must be the case that $t_{f}=(t_{a}\rightarrow t_{a})$.
dingo (x,y) = [x,y]
--- Initial guess ✅
dingo :: (t, t) = [t]Because even if tuples can take different types, lists cannot. This is parametric polymorphic, as it a type variable.
defined a Haskell function bighead that can tell us how many elements in a list xs are greater than the head of xs. As an example of the behavior of the function, the result of bighead [7,4,5,8,9] is 2. They claim the type os [Num] -> Num. Why is this incorrect?
Ehh, the list can be empty?
It isn’t just any number, but an integer it spits out?
I’d say that the type is
[Num] -> IntBut that’s actually wrong. It’s more like
bighead :: (Num a, Ord a) => [a] -> Int
bighead xs = count
where h = head xs
count = length [e | e <- tail xs, e > h]The Eq type class checks equality.
How can you ever know if two functions are equal?
That is impossible.
Can encounter halting problen when checking equality of functions.
mango x y z = x * y + z - 42What is the type of mango 14?
--- Initial guess
mango 14 :: y -> z -> Num
--- Answer
mango 14 :: Num a => a -> a -> aI got it wrong in that it should have just been a class constraint for a single type variable, because we’d expect all the inputs to be numeric for this function to work.
that has the following type. Definition doesn’t matter as long as it’s type correct:
bingo :: a -> abingo a = aIt’s parametric polymorphism, as it has a type variable.
thesamethat takes a list of pairs xs and gives us the list of pairs whose first and second component are the same
for example, we want thesame [(1,2),(4,4),(6,7),(17,17)] to return [(4,4),(17,17)]
What should the type of thesame be?
thesame [(a, b)] -> [(a,a)][(+),(*),(+),(-)]What does it contain and what is the type of the expression?
What can you say about the type of [(+), (*), (+), (-), (++)]
It’s a list of functions.
Not wrong…
[(+),(*),(+),(-)] :: Num a => [a -> a -> a]
But the real answer:
Check page 34 in the book.
There the types of these functions are given.
The type of the list is
[(+), (*), (+), (-)] :: Num a => [a->a->a]Also a list of functions?
Not wrong…
[(+),(*),(+),(-), (++)] :: Num [a] => [[a] -> [a] -> [a]]
Are the bound variables in the term distinct? If not, rename so they are. Then find a reduction step that the term can take.
They are distinct. Recall the scope rules for the bound variables.
Reduction step reduces to $x x$ by beta-reduction.
Left fn takes right fn as input.
mapp :: (i -> o) -> [i] -> [o]
mapp f xs = [f x | x <- xs]A type is name for collection of related values.
E.g. Bool contains False and True.
e :: t means that e has type t.
Haskell is strongly typed as type errors are found at compile-time.
A list is a sequence of values of the same type: [t] is the type of list with elements of type t.
A tuple is a sequence of values of (possibly) different types: (False, 'a', True) :: (Bool, Char, Bool).
A function is a mapping from values of one type to values of another type: even :: Int -> Bool.
You can do function with muliple arguments or results by using lists or tuples.
Haskell has multiple type classes, e.g.
Num — numeric typesEq — equality typesOrd — ordered totally (linearly) types. Strings, lists, and tuples are lexicographically ordered (same was as words in a dictionary). Comparison occurs like you’d compare strings. One character at a time.Show — types whose values can be converted to strings of charactersRead — types whose values can be converted from strings of charactersIntegral — types that are instances of Num but are integersFractional — types that are instances of Num but are fractional typesYou can also have functions with multiple arguments by returning functions as results.
add' :: Int -> (Int -> Int)
add' x y = x+y -- takes int x and returns function add' x. That takesan integer y and returns x+y.
-- Haskell says the type of add' is add' :: Num a => a -> a -> aIn JS, this would be const add = x => y => x + y.
Conventions
Int -> Int -> Int -> Int means Int -> (Int -> (Int -> Int)).mult x y z means ((mult x) y) z.A function is polymorphic if its type contains one or more type variables.
length :: [a] -> Int is polymorphic. It doesn’t care which type of list you give it. So now a is a type variable.
A polymorphic function is overloaded if its type contains one or more class constraints.
(+) :: Num a => a -> a -> a means for any numeric type a, (+) takes two values of type a and returns a value of type a.
The => defines a class constraint: everything before it is part of the constraint.
An expression can be 3 things: a variable, abstraction, or application.
$\lambda x.e_{1}$ denotes a function with formal parameter $x$ and body $e_{1}$.
Scope of $x$ is all of $e_{1}$, but parentheses can be introduced to delimit scope.
$e_{1}e_{2}$ denotes that function $e_{1}$ is to be applied to argument $e_{2}$.
Scope rules: In $\lambda x.e$, the scope of the Formal parameter $x$ is the body $e$ of that abstraction. We say $x$ is bound in $e$.
But in $\lambda x.xy$, $x$ is bound but $y$ is not—so it’s free.
Beta-reduction
This is the most important rule. There are multiple rules in the reduction relation, but this one is central.
The reduction relation is how an expression can be reduced to some other expression.
It says that if we have the application $(\lambda x.e_{1})e_{2}$, we can substitute the formal parameter $x$ with $e_{2}$ inside the body $e_{1}$.
This is beta-reduction: if we apply a function to an argument, we substitute the formal parameter by the actual parameter. This is the call-by-name parameter mechanism (SS 13 - Parameter Mechanisms).
An expression of this form is called a redex.
A redex is a subexpression for which reduction is possible. If the reduction is a $\beta$-reduction, it’s a $\beta$-redex. It stands for reducable expression.
We need some more rules now:
The left part of the application is what should become a function (abstraction).
We could also reduce to the right component.
In abstraction $\lambda x.e$, the $x$ is called a binding occurrence of $x$. If the same $x$ occurs inside $e$, it’s called a bound occurrence of $x$. A binding occurrence is like a placeholder—the name isn’t important. Just like parameter names in functions, it doesn’t matter what they’re called: they shouldn’t conflict with outside variable names.
If an expression $e_{2}$ can be obtained from some other expression $e_{1}$ by systematically renaming zero or more binding occurrences and their bound occurrences, $e_{1}$ and $e_{2}$ are $\alpha$-convertible, and write $e_{1}\equiv_{a}e_{2}$.
Examples
Applying a function on another expression:
The above gives 49.
Lambda Calculus | Brilliant Math & Science Wiki
Lambda Calculus Calculator
Abstractions are function definitions, and are denoted by $\lambda$. After the symbol you write the input variables, followed by a dot, and then the output of a function where you describe what you want to get (the body of the function).
Variables are the same as variables in programming languages. They contain values. The scope of a variable is defined by its closest function or parentheses. Variables can be free or bound. Bound variables are those used in its scope after it was delared in the closest function input, otherwise it’s free. In the following lambda, $x$ is bound and $y$ is free: $\lambda x.xy$
A Lambda term is a basic entity. It can be a variable or function. So any variable, application, or abstraction is a valid term. These can be given names for easier reusability, e.g. $I := \lambda x.x$, for the identity term.
Alpha conversion (alpha renaming) says that names of bound variables in abstraction can be changed. Variables not bound in abstractions don’t work.
Function is a process of associating input to output. But here, functions are anonymous (can’t be given names), can take only one variable, and are treated as first-class values, so they can be both inputs and outputs of functions.
Application is applying a lambda term to another. To write it, just write the terms with whitespace between them: $x\ y$.
More than 1 argument through currying:
$\lambda xy.x$ becomes $\lambda x.\lambda y.x$.
To make a function that takes multiple arguments, make a function that takes the first argument, and returns a function which takes the second argument and returns an output.
Substitution
Replacing all free occurrences of a variable in the expression with another expression.
Beta-reduction
The process of applying a variable to a function.
Like calling a function with an argument.
E.g. multiplyByFive(2) would look like:
When you apply a function to a term, take the function’s body and run it with the applied argument as an input.
Recursion
A function using itself.
To do this in a language where every function is anonymous, describe a function and then describe it again in its argument:
This is the Y combinator (fix-point combinator).
quango and tango that have the following types; it is not important what the definitions do as long as they are type correctquango :: a -> [a]
tango :: Num p1 => (a, b) -> p2 -> p1Are quango and tango polymorphic? If so, tell us if for each of them if this involves parametric Polymorphism or overloading (ad hoc Polymorphism) or maybe both — and how. If not, tell us why.
quango :: a -> [a]
quango a = [a]
tango :: Num p1 => (a, b) -> p2 -> p1
tango (a, b) p2 = 1Yes, they are. Both involve typed variables.
quango is parametric polymorphism, as it doesn’t matter which value is given as argument, it simply returns a list of that type.
And tango is overloaded as it contains class constraints in its type.
To do this, use the reduction rules of the note.
It reduces to $xy$ and I have no idea why.
twice f x = f(f(x))
-- Initial guess
twice :: f -> x -> f(f x)
-- Actual answer
twice :: (t -> t) -> t -> tIt is parametric polymorphic, as it contains a type variable.
How would you go about figuring this out? First, observe that the function takes two arguments. Since functions in Haskell take exactly one argument, we know that it returns a function which takes the second argument.
So we can infer the following:
So the question is, what is $t_{f}$, $t_{x}$, and $t_{r}$?
Well, in the result, you see a function application, which is an argument of another function application.
We know that $f$ is a function, just from the syntax. So $f:t_{a}\rightarrow t_{b}$
From page 23 in the book. we know that if a function is of type $f::A\rightarrow B$, and its argument has type $x :: A$, then $f\ x :: B$.
So in this case, $x :: t_{a}$ and $f(x) :: t_{b}$.
And $f(f(x))::t_{b}$ and $f(x)::t_{a}$.
Otherwise we couldn’t apply $f$ to $f(x)$.
And from this we observe that $f(x)::t_{b}=t_{a}$. They must be the same type.
So now we know that $t_{r} = t_{a}$, and $t_{x}$ is also $t_{a}$.
And then it must be the case that $t_{f}=(t_{a}\rightarrow t_{a})$.
dingo (x,y) = [x,y]
--- Initial guess ✅
dingo :: (t, t) = [t]Because even if tuples can take different types, lists cannot. This is parametric polymorphic, as it a type variable.
defined a Haskell function bighead that can tell us how many elements in a list xs are greater than the head of xs. As an example of the behavior of the function, the result of bighead [7,4,5,8,9] is 2. They claim the type os [Num] -> Num. Why is this incorrect?
Ehh, the list can be empty?
It isn’t just any number, but an integer it spits out?
I’d say that the type is
[Num] -> IntBut that’s actually wrong. It’s more like
bighead :: (Num a, Ord a) => [a] -> Int
bighead xs = count
where h = head xs
count = length [e | e <- tail xs, e > h]The Eq type class checks equality.
How can you ever know if two functions are equal?
That is impossible.
Can encounter halting problen when checking equality of functions.
mango x y z = x * y + z - 42What is the type of mango 14?
--- Initial guess
mango 14 :: y -> z -> Num
--- Answer
mango 14 :: Num a => a -> a -> aI got it wrong in that it should have just been a class constraint for a single type variable, because we’d expect all the inputs to be numeric for this function to work.
that has the following type. Definition doesn’t matter as long as it’s type correct:
bingo :: a -> abingo a = aIt’s parametric polymorphism, as it has a type variable.
thesamethat takes a list of pairs xs and gives us the list of pairs whose first and second component are the same
for example, we want thesame [(1,2),(4,4),(6,7),(17,17)] to return [(4,4),(17,17)]
What should the type of thesame be?
thesame [(a, b)] -> [(a,a)][(+),(*),(+),(-)]What does it contain and what is the type of the expression?
What can you say about the type of [(+), (*), (+), (-), (++)]
It’s a list of functions.
Not wrong…
[(+),(*),(+),(-)] :: Num a => [a -> a -> a]
But the real answer:
Check page 34 in the book.
There the types of these functions are given.
The type of the list is
[(+), (*), (+), (-)] :: Num a => [a->a->a]Also a list of functions?
Not wrong…
[(+),(*),(+),(-), (++)] :: Num [a] => [[a] -> [a] -> [a]]
Are the bound variables in the term distinct? If not, rename so they are. Then find a reduction step that the term can take.
They are distinct. Recall the scope rules for the bound variables.
Reduction step reduces to $x x$ by beta-reduction.
Left fn takes right fn as input.
mapp :: (i -> o) -> [i] -> [o]
mapp f xs = [f x | x <- xs]