Functional Programming in C {with categories} (Dimitris Papadimitriou) (Z-Library)

Functional In C# {with: categories} Gain advanced understanding of the mathematics behind modern functional programming. Programming dimitris papadimitriou v 2.2.1

1 FUNCTIONAL PROGRAMMING IN C# WITH CATEGORIES Gain advanced understanding of the mathematics behind modern functional programming Dimitris Papadimitriou Version : 2.2.1 last updated 26-Apr-2021 This is a Leanpub book. Leanpub empowers authors and publishers with the Lean Publishing process. Lean Publishing is the act of publishing an in-progress ebook using lightweight tools and many iterations to get reader feedback, pivot until you have the right book and build traction once you do. Feel free to contact me at: https://www.linkedin.com/in/dimitrispapadimitriou/ https://leanpub.com/u/dimitrispapadim https://github.com/dimitris-papadimitriou-chr dimitrispapadim@live.com Resources Source Code: https://github.com/dimitris-papadimitriou-chr/FunctionalCSharpWithCategories Also contains https://github.com/dimitris-papadimitriou-chr/Practical-Functional-CSharp © 2021 Dimitris Papadimitriou

2 Contents About this book coding conventions ...................................................................................... 7 The language-ext C# library .............................................................................................. 7 1 Language Functional support ......................................................................................... 8 1.1 Pure functions and Side effects............................................................................... 8 1.2 Evolution of Delegates in C# ................................................................................. 11 1.3 Built-in .NET Delegates ......................................................................................... 14 1.4 Essential Typed Lambda calculus and C# ............................................................ 17 1.5 Higher-order functions .......................................................................................... 25 1.6 Simple Function Composition ............................................................................... 28 1.7 Callbacks .............................................................................................................. 33 1.8 Named parameters and Tuples ............................................................................. 35 Lambda expressions and tuples..................................................................... 37 1.9 Extension Methods ............................................................................................... 39 1.10 Using static directive ............................................................................................. 41 1.11 LINQ support for custom Data structures .............................................................. 42 1.12 Currying and partial application ............................................................................. 43 2 Algebras of Programming ............................................................................................ 46 2.1 Categories ............................................................................................................ 46 2.2 Monoids ................................................................................................................ 48 Folding monoids ............................................................................................ 50 2.3 Folding monoids showcase ................................................................................... 52 2.4 Function composition as a monoid ........................................................................ 54 2.5 Composing monoids ............................................................................................. 55 2.6 Composite Design pattern - Functional Perspective .............................................. 58 2.7 Decorator Design pattern - Functional Perspective ............................................... 59 2.8 Predicate monoidal Composition ........................................................................... 62 2.9 Specification Pattern - Functional Perspective ...................................................... 65 Monoid homomorphisms and Parallelism ....................................................... 67 3 Algebraic Data Types ................................................................................................... 73 3.1 The Product .......................................................................................................... 75 3.2 One ...................................................................................................................... 77 Lambda Calculus with Product Types ............................................................ 78 3.3 The Co-Product (aka Union) ................................................................................. 83 Lambda Calculus with Co-Product Types ...................................................... 85 3.4 Extending Union Types ......................................................................................... 88

3 Adding Pattern Matching extensions to Union Types ..................................... 89 Rewriting Union Type methods with MatchWith ............................................. 90 The C#8.0 Pattern matching Feature ............................................................. 91 3.5 A brief intro to Recursion....................................................................................... 91 Lambda Calculus Again- Gödel’s System T ................................................... 95 3.6 Recursive Algebraic Types ................................................................................... 97 3.7 Practical Structural Induction ............................................................................... 99 Rewriting Map with MatchWith ..................................................................... 101 On the value of the symbolic representation ................................................ 102 Adding Pattern Matching extension to List<T> ............................................. 103 3.8 Recompose the List ............................................................................................ 104 3.9 Passing More arguments .................................................................................... 105 3.10 Returning More items .......................................................................................... 106 3.11 Filtering ............................................................................................................... 106 3.12 Inserting items in an Ordered List ....................................................................... 107 3.13 Insertion Sort ...................................................................................................... 108 4 Functors ..................................................................................................................... 110 4.1 The Identity Functor ............................................................................................ 111 4.2 Commutative Diagrams ...................................................................................... 113 4.3 The Functor Laws ............................................................................................... 115 4.4 Pattern Matching ................................................................................................. 117 4.5 Id<T> Functor on the Fly ..................................................................................... 122 Some more Isomorphisms ........................................................................... 122 The Basic Functor Mechanics ...................................................................... 124 4.6 Extending Task<T> to Functor ............................................................................ 125 4.7 IO Functor, a Lazy Id Functor ............................................................................. 127 Func<T> Delegates as Functor .................................................................... 127 IO Functor .................................................................................................... 128 4.8 Reader Functor ................................................................................................... 129 4.9 LINQ Native Query syntax: Functor Support ....................................................... 130 4.10 Maybe Functor aka Option<T>............................................................................ 132 Dealing with null ........................................................................................... 132 The Null Object Design pattern .................................................................... 132 The Functional equivalent - Maybe as Functor ............................................. 134 Maybe Functor Example .............................................................................. 137 Maybe in Language-ext / Option .................................................................. 138 Maybe Functor Example With language-ext Option ..................................... 139

4 C# 8. pattern matching Support for Option ................................................... 139 Folding Maybe ............................................................................................. 140 Using the Linq syntax ................................................................................... 141 4.11 Either Functor ..................................................................................................... 141 Pattern matching for Either <T> ................................................................... 142 Using C# 8.0 pattern matching ..................................................................... 143 Either Functor Example ............................................................................... 144 C# 8. pattern matching Support for language-ext Either ............................... 145 Using Either for exception handling .............................................................. 146 4.12 Explicitly Compositing Functor ............................................................................ 149 4.13 Combining Task and Option – Task<Option<T>> ............................................... 150 4.14 Combining Task and Option – OptionAsync<T> ................................................. 153 4.15 Combining Task and Either – Task<Either<,>> ................................................... 154 4.16 Combining Task and Either – EitherAsync<> ...................................................... 156 4.17 Functors from Algebraic Data Types ................................................................... 157 4.18 Applicative Functors ............................................................................................ 160 4.19 Reader Applicative Functor ................................................................................. 162 5 Monads ...................................................................................................................... 164 5.1 Monads in Category Theory ................................................................................ 166 5.2 The List Monad ................................................................................................... 170 5.3 The Identity Monad ............................................................................................. 170 Monad laws for Identity Monad .............................................................. 171 5.4 Maybe Monad ..................................................................................................... 172 Using language-ext Option........................................................................... 174 Using the LINQ syntax with Option Monad ................................................... 175 5.5 Either Monad ...................................................................................................... 176 Using Either Monad for exception handling .................................................. 177 Using language-ext Either<> ........................................................................ 178 Using the LINQ syntax with Either Monad .................................................... 179 Using Either for Validation............................................................................ 179 5.6 Validation Monad ................................................................................................ 180 Using Validation.Apply to Collect validations ................................................ 181 5.7 Task<T> as Monad ............................................................................................. 182 5.8 The Task - Option Monad Combination -Task<Option<>> .................................. 183 5.9 The Task - Option Monad Combination -OptionAsync<> .................................... 185 5.10 The Task - Either Monad Combination -Task<Either<,>>.................................... 187 5.11 The Task - Either Monad Combination -EitherAsync<> ....................................... 189

5 6 Catamorphisms Again ................................................................................................ 191 6.1 A brief mentioning of F-algebras ......................................................................... 191 6.2 Catamorphisms ................................................................................................... 192 6.3 Initial algebra ...................................................................................................... 194 F-Algebras Homomorhisms ......................................................................... 194 6.4 Catamorphisms for Trees .................................................................................... 196 6.5 Catamorphisms with the Visitor Design pattern ................................................... 198 The Base Functor of the List<T> .................................................................. 199 A brief mentioning of Anamorhisms ............................................................. 203 F-Coalgebra ................................................................................................. 204 Corecursion ................................................................................................. 204 A brief mentioning of Hylomorphisms ........................................................... 206 Hylomorphism example: Mergesort .............................................................. 207 6.6 Fold’s relation to Cata ......................................................................................... 209 7 Traversable ................................................................................................................ 210 7.1 Traversable Algebraic data structures ................................................................. 213 7.2 Traversing with The Task<T> aka Parallel .......................................................... 214 7.3 Applicative Reader Isomorphism with the Interpreter Design pattern .................. 216 Standard Catamorphism implementation ..................................................... 217 Reader applicative implementation .............................................................. 219 Object Oriented Interpreter Pattern implementation ..................................... 220 7.4 Explicitly Composing Traversables ..................................................................... 221 7.5 Foldable .............................................................................................................. 222 FoldMap ....................................................................................................... 223 Explicitly Composing Foldables ................................................................... 225 8 A Clean Functional Architecture Example .................................................................. 227 8.1 Download and Setup the Project ......................................................................... 227 Clean Architecture with .NET core ............................................................... 228 8.2 A Functional Applications Architecture ................................................................ 230 8.3 The Contoso Clean Architecture with .NET core and language-ext ..................... 231 8.4 Web Api .............................................................................................................. 232 8.5 Domain Model ..................................................................................................... 233 Repositories ................................................................................................. 236 8.6 CQRS ................................................................................................................. 237 8.7 CQRS and MediatR ............................................................................................ 239 The Command Pattern with a Mediator ........................................................ 239 Query Workflow ........................................................................................... 242

6 Command Workflow ..................................................................................... 246 Purpose The tools we use have a profound (and devious!) influence on our thinking habits, and, therefore, on our thinking abilities. — Edsger Dijkstra OO makes code understandable by encapsulating moving parts. FP makes code understandable by minimizing moving parts. —Michael Feathers (Twitter) One of the main reasons for this book is to transfer in the community of object- oriented developers some of the ideas and advancements happening to the functional side. This book wants to be pragmatic. Unfortunately, some great ideas are coming from academia that cannot be used by the average developer in his day to day coding. This is not an Introductory book to functional programming, even if I restate some of the most basic concepts in the light of category theory and the object-oriented paradigm. This book covers the middle ground. Nonetheless, it is written in a way that if someone pays attention and goes through the examples, he or she could understand the concepts. An introductory book will follow in Leanpub, covering more basic ideas, along with the extended version of this book covering more advanced topics. In this book, I will try to simplify the mathematical concepts in a way that can be displayed with code. If something cannot be easily displayed with code probably will not be something that can be readily available to a developer’s arsenal of techniques and patterns. If you think a section is boring, then skip it and maybe finish it later. One thing I admire in Software Engineers is their ability to infer things. The ability to connect the dots is what separates the exceptional developer from the good one. In some parts of the book, I might indeed have gaps or even assume things that you are not familiar with. Nonetheless, I am sure that even an inexperienced developer will connect the dots and assign meaning, as I usually do when left with unfinished

7 About this book coding conventions Let’s be pragmatic here, this style of coding that promotes purity should not be an end in itself, and we should always be able to convince ourselves to go back into an object- oriented style of coding even if it is not that pure. The important thing is to write functional code that provides business value to the organization and to the end-user that will eventually use it. We must be pragmatic and utilitarian when we code and abstractionists when we think about code. This book is aiming to present the basics of functional programming using the language- ext library. We will try to exhibit the usage of the basic Functional types: Option, Either, Task and Validation within an ASP.NET MVC web paradigm. There is a WebApplicationExample solution that has multiple simpler examples of language-ext in a .net core web application. The intention is to build up an understanding behind the architecture of the Sample Contoso web Application in the language-ext GitHub project which is examined in the last chapter of this book. The language-ext C# library This book is all about the specialization of the concepts of functional programming with the language-ext C# library. There are some functional libraries out there for C#, but currently the only complete library that could be used in a commercial project is the language-ext. In this section we are going to see a couple of the basic crosscutting ideas in the library and then in the following Chapters we will introduce all the different structures. In this book we are going only to use the Nu-get package LanguageExt.Core.

8 C# Functional Features An overview “1996 - James Gosling invents Java. Java is a relatively verbose, garbage collected, class based, statically typed, single dispatch, object oriented language with single implementation inheritance and multiple interface inheritance. Sun loudly heralds Java's novelty. 2001 - Anders Hejlsberg invents C#. C# is a relatively verbose, garbage collected, class based, statically typed, single dispatch, object oriented language with single implementation inheritance and multiple interface inheritance. Microsoft loudly heralds C#'s novelty.” -Brief, Incomplete and Mostly Wrong History of Programming Languages, 1 Language Functional support 1.1 Pure functions and Side effects No matter the programming paradigm the minimal unit of processing is a function a→b. There would not be any motion if a value could not be transformed into another value. In Object oriented programming we call them methods. the most important thing about a function is its Type signature. A type signature or type annotation defines the inputs and outputs for a function, subroutine or method. In Object oriented programming we do not think about the function types that much, whilst in functional programming the function types are the main focus. Look for example, the following function: public double GetDiscountedPrice(double price, double discount) { return price * (1 - discount); } This function has a signature like this GetDiscountedPrice: (double, double) → double. This is almost a perfect function. First, it’s called total because no matter what value you input for the price and discount it will yield a result. Does not throw exceptions or return null. If only all functions where like this one. Also, its Pure because it does not access any outside

9 variable or modifies in any way the computational environment (this means that has no side effects) In object-oriented programming the importance of the Type signature is diminished by the fact that there is so much coupling going on. Let me explain. Look at the following object: public class Product { public double Price { get; set; } public Product(double price) { Price = price; } public void AddDiscount(double discount) { this.Price = this.Price * (1 - discount); } } Now we placed the previous function in an object. What is the type signature of the AddDiscount method? is it double→ ( ) ? It Sure, looks like that it just takes a double and returns nothing. So why not. Well almost. The fact is that the function access in a hidden manner the this.Price so this counts as an additional input argument (double, double)→(). There is no return output that is suspicious. Because also access the this.Price of the Product and mutate its state. Side effects are operations that change the global state of a computation. Formally, all assignments and all input/output operations are considered side-effects. The functional programming style tries to avoid /reduce side effects. double discount Side effect AddDiscount Price { set; } Product Side effects 1.1.1.1.1 Funtional Programming

10 First, the fact that the object exposes the Price can lead to bugs. For example, we can have this sequence: var product = new Product(100); product.AddDiscount(0.1); //... //somewhere else product.Price = 80;//what now? this cancels the previous discount you can even have simple multithread applications that just access the Price in a different order of what was intended. We can of course hide the Price from the outside environment (the class scope). public class Product { public double Price { get; private set; } public Product(double price) { Price = price; } public void AddDiscount(double discount) { this.Price = this.Price * (1 - discount); } } Of course, we can just remove the setter all together and every time create a new updated product. Thus, make the Product immutable. public class Product { public double Price { get; } public Product(double price) { Price = price; } public Product GetDiscountedProduct(double discount) { return new Product(this.Price * (1 - discount)); } } Now we could completely extract the method from the Product and place it in a PricingService: public class PricingService { public Product GetDiscountedProduct(Product product, double discount) { Better. Now the Product price cannot be changed directly from the outside environment. No setter We return a new Product

11 return new Product(product.Price * (1 - discount)); } } var discountedProduct = new PricingService() .GetDiscountedProduct(new Product(100), 0.1); The type signature of the GetDiscountedProduct function now is (Product, double) → Product Finally, this type reflects the real intention of the Pricing computation. 1.2 Evolution of Delegates in C# The most prominent language feature that facilitates functional programming is the existence of First-Class functions. This means the language needs to support the ability to treat functions as you would any variable and pass them around to other functions as you see fit. Lambda functions extend this concept, allowing the creation of an anonymous function, in a compressed and easy to read syntax. Here we are going to display in rapid succession in just a section all the C# features related to lambdas. Consider this as a small reference guide. From .net 1.0 version the delegate was introduced. The delegate is a thing of the past and you probably will not see it anywhere but is behind all other concepts. A delegate Type is just a declaration of a function signature. Delegates For example, we can declare this delegate: public delegate double DiscountDelegate(double price, double discount); this informs us that anything that looks like the following: double ___(double price, double discount) can be assigned at a variable of type DiscountDelegate. If we have the following function: double GetDiscountedPrice(double price, double discount) { return price * (1 - discount); } This is a perfectly valid declaration: DiscountDelegate discountFunc = GetDiscountedPrice; You will see if you try to use this discountFunc variable the intellisense informs you that this expects 2 arguments of double and returns a double

12 C#3.0 lambda expression After C# 3.0 we do not have to declare delegates anymore, and we instead use the generic Func<>. For example, we can write the following: Func<double, double,double> discountFunc = GetDiscountedPrice The Func<double, double, double> represents a Delegate Type that has the following signature (A x, B y) → C Func<A, B, C> And we can assign a lambda expression directly to a Func<...> If you go to the definition you will see the framework Func<> implementation for different number of input arguments: public delegate TResult Func<in T, out TResult>(T arg); public delegate TResult Func<in T1, in T2, out TResult>(T1 arg1, T2 arg2); .net source they are just delegate declarations. All the following statements are equivalent : Func<double,double,double> getDiscount = (double price,double discount) => {return price-discount * price; }; Func<double, double, double> getDiscount1= (double price, double discount)=> price-discount * price; Func<double, double, double> getDiscount2 = (price, discount) => price-discount * price; hopefully, you are already familiar with this notation, but in case you are not, let us go through each one by one briefly. Firstly, the following is an lambda expression : (double price,double discount) =>{return price – discount * price; }; And is just a function. We can remove the {return ___ }; with the resulting expression: First argument Second argument The return Type Intellisense information Remove return {…} Remove double keyword

13 Func<double, double, double> getDiscount = (double price, double discount) => price-discount * price; if the function returns a result immediately and we do not need multiple lines. Because in functional programming we try to chain computations usually there is no need for the braces. Finally, we can remove the types inside the input arguments: (double price, double discount)=>_ resulting to the following: Func<double, double, double> getDiscount2 = (price, discount) => price-discount * price; Local functions Starting with C# 7.0, C# supports local functions. With local functions you can just nest functions inside other functions, methods or even lambdas: public class Demo { public double GetDiscountedPrice(double price, double discount) { double getCustomerDiscount() { return discount * 0.5; }; return price * (1 - discount - getCustomerDiscount()); } } We can nest local functions in local functions all the way down: public class Demo { public double GetDiscountedPrice(double price, double discount) { double getCustomerDiscount() { return discount * 0.5; double getCustomer () { throw new NotImplementedException(); }; }; return price * (1 - discount - getCustomerDiscount()); } Also, we can nest inside lambdas: Func<double, double, double> getDiscount = (price, discount) => { decimal getCustomerDiscount() nested local function Double nested local function

14 { throw new NotImplementedException(); }; return price - discount * price; }; 1.3 Built-in .NET Delegates .NET contains a set of delegates designed for commonly occurring use cases, so we do not have to declare custom delegates. Those are residing in the System namespace. Here are the most important and most used : Func<T,R> The most common delegate by far will be the Func<T, R>, which represents functions and methods that look like this R f(T t) taking one argument and returning one result. Visually this could be represented by just an arrow: Func<T,U,R> Represents a function Type that has the following signature R f(T t1, U t2). The Func<T,U,R> represents a Delegate Type that has the following signature (T , U) → R Func<T, U, R> If you wanted to visualize this could be a join: f T R f T R U First argument The return Type Second argument

15 Action<T> The Action<T> Functional interface represents functions that have this signature void f(T t). In functional programming we usually do not like the void because it is not a Type like all the others, and this forces us to treat it differently. Action<T> is just a Func<T, void> but because void is not a Type .NET had to invent Action<T>. As an example of usage look at the following, where we “consume” a string returning nothing: Action<string> print = (string x) => Console.WriteLine(x); When you return void is an indication that you create a side effect of some sort. We can shorten the declaration, using the point free notation : Action<string> print1 = Console.Write; A visualization for Action<T> could be: Func<T> The Func<T> represents functions that have this signature T f() that do not take any arguments. A simple example would be: Func<string> getName =()=>"jim"; visualize this as a value coming out of nothing: Func<T> is the dual of Action<T> and in this way we can compose them and annihilate them into a void. Action<string> print = Console.Write; Func<string> getName =()=>"jim"; print(getName()); // prints Jim as side effect with return type void f T This represents the void f T "jim" print getName IO operation Console.Write Side effect

16 Predicate<T> The Predicate<T> Functional interface represents functions that have this signature bool f(T t1) that returns a bool. This is equivalent to a Func<T, bool>. Summary Table Action<T1> void f(T1 a){…} Action<T1,T2> void f(T1 arg1, T2 arg2){…} Func<TResult> TResult f(){…} Func<T1,TResult> TResult f(T1 arg1){…} Func<T1,T2,TResult> TResult f(T1 arg1, T2 arg2){…} Func<T1,T2,…T16,TResult> TResult f(T1 arg1, T2 arg2,…,T16 arg16){…} Predicate<T> bool f(T arg1){…} Remember : 1. The Action delegates only have input arguments. 2. The Func<_,,,_> is the general case. 3. For Any Func<_,,,TResult> the Result is always at the Last position. 4. If you only want to return a result ()=>… you must use a Func<TResult>. Since we can declare Func delegates as variables, it is possible that the delegate variable has not been assigned at the time of Invocation: Func<string> getName = null; var name = getName(); // we get a Null Reference Exception in order to avoid this situation we usually use the ?.Invoke() method on the Delegates getName?.Invoke(); //because of the ? operator we dont have an Exception. .NET Conventions ?.Invoke(…)

17 1.4 Essential Typed Lambda calculus and C# Lambda calculus is the original functional language. Lambda calculus is a formal system in mathematical logic, that was used to express computations. It was created by the great Alonzo Church in the 1930s. In this section we are going to see the simply typed lambda calculus (the usual symbol is λ→ ) and how this relates to the C# lambdas. In order to do that we will keep only for this section a subset of C# equivalent to the λ→. Simple typed lambda calculus is a very simple system that does not support Generics but allows for simple types. Terms The formulation of the lambda expressions is constructed bottom up-in an inductive manner using as its base the term Term. A Term can be one of three things: 1. A Variable: x is a Term 2. An Abstraction: λx:A.M is a Term, where M is a Term and x is a variable. 3. An Application: (M N) is a Term, where M and N are Terms 4. A Constant c is a Term From those the peculiar ones are the (2), and (3) which correspond in C# loosely to the following (we are going to elaborate on this): 1. The lambda abstraction λx:A.M corresponds to a C# function Func<A, B> f = (A x) => ... 2. And the application (M N) corresponds to the trivial function call f(x) Of course, only with those expressions you cannot expect to do any meaningful computation because you must introduce syntax related with the Natural Numbers (+, -, …), Booleans (if, then… ). Nonetheless, one could go down the road of defining Numerals using the Church encoding (we will skip this part in this book) which are typable in λ→ using only one type: Func<Func<_, _>, Func<_, _>> zero = (Func<_, _> f) => (_ x) => x; Func<Func<_, _>, Func<_, _>> one = (Func<_, _> f) => (_ x) => f(x); Func<Func<_, _>, Func<_, _>> two = (Func<_, _> f) => (_ x) => f(f(x)); For some single arbitrary empty type class _ { }.

18 In mathematics the Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. 0 ≅ λf. λf. x 1 ≅ λf. λf. f(x) 2 ≅ λf. λf. f(f(x)) The type of those numerals is (_→_) →(_→_), which we can define as delegate for simplicity: delegate Func<_, _> N (Func<_, _> f); Then you can define things like the Successor function, addition etc. Func<N, N> Succ = (N n) => (f) => x => f(n(f)(x)); // add an additional f in front This is just a Hacky way to do arithmetic, imagined by the genius of Alonzo Church during the 30’s, which constitute the ancient history of computer science. Now, in the untyped lambda calculus we could have a lambda application (M N) of any two Terms. This led to problems early on because it allowed Russel type paradoxes [Curry's paradox]. That is why Types were introduced to restrict the operations of Terms based on their type. This idea of types is considered today common knowledge, in all strongly typed, languages like C#. Types The only types in λ→ is the Set of some base types B, and anything whatever is produced by this simple grammar in BNF form: τ ::= τ→ τ | T where T ∈ B this means the only types that occur in λ→ are inductively defined and are either of the form τ→ τ where τ is some already created type, or some type belonging to the base types. If for example B = {σ, ρ} then the types generated look like this : σ, ρ, σ→ σ, ρ→ρ, ρ→ σ, (ρ→ σ) → ρ, …, (ρ→ σ) →(ρ→ σ) … If we take the C# type system with the usual primitive build-in types then a simple λ→ restricted version of C# would have as base types B= {int, char, bool, …} and everything that would be generated using the τ ::= τ→ τ | T grammar. This would result in syntax trees like the following: Church encoding 1.1.1.1.2

19 The (int→ int) → int in C# is the delegate Func<Func<int,int>, int> while the second one (int→ bool) → (int → char) would be Func<Func<int,bool>, Func<int,char>> As one can see an embedded λ→ version within C# would only allow for things that look like this Func<Func<... , ...>, Func<..., ...>> with nested Func delegates. Introduction and Elimination Rules Introduction Rule Now we have used an inductive definition to create a Set of Types and used an inductive definition to define a Set of Terms, the next step is to link them. We have to give an Inductive definition of how specific Terms belong to specific Types. First there is the introduction rule which signifies the way we construct a lambda abstraction. Here you see the mechanism to create a λx:A.M Term and why this Term is of type A →B and that is the only way to create τ→ τ types. The [x: A]1 means that at some point we make an assumption of having a variable x of type A, or in another phrasing we have a context where we have a variable x of type A. In C# this is expressed by the declaration: (A x) => ... By starting a lambda, you might assume that you introduce a x:A out of thin air. Then in this setting we finally construct a term M:B we can discharge the assumption and introduce this implication sign ⇒ (equivalently the => in C#) and this gives us the Int ∈ B → → Int ∈ B Int ∈ B (int→ int) → int (int→ bool) → (int → char) → → bool ∈ B Int ∈ B char ∈ B Int ∈ B → ⇒I1 M:B [x:A]1 . . . . λx.Μ: A →B