explaining $\lambda$-calculus/functional programming to someone used to Turing machines/procedural programming?

I have the following background:

-
I have experience with object-oriented programming languages

-
I find Turing machines and the concept of a "procedure" very intuitive.

Yet I'm interested to understand the idea behind the abstract $\lambda$-calculus, and its application in the form of functional programming.

When I read about either $\lambda$-calculus or functional programming, these explanations tend to either:

-
make reference to practical benefits that seem generally beneficial to me, but don't give me a fundamental-principled understanding. E.g. that functional programming languages are more modular and less error-prone because there are no state-dependencies.

-
or assume an already existing intuitive familiarity with either $\lambda$-calculus or the practicalities of functional programming. (Essentially these explanations suffer from the curse of knowledge: the authors cannot place themselves in the shoes of someone who doesn't have their intuition yet).

So I am looking for a general, principled, theoretical understanding of the conceptual and formal difference between (1) $\lambda$-calculus and Turing machines, and between (2) functional programming and procedural programming.

I'd like to second both Derek Elkins' and Chi's comments. You can do Functional Programming in most languages, but it requires the discipline to adhere to the functional principles. It's probably harder to learn FP in a language like Javascript\Python because you'll have to fight against the urge to do things the old way you already know.

In a Functional Programming Language (i.e. purely functional) you'll have to do stuff THE FUNCTIONAL WAY, without taking corners. Also, doing practical stuff means you'll have to learn some theory as well.

• make reference to practical benefits that seem generally beneficial to me, but don't give me a fundamental-principled understanding. E.g. that functional programming languages are more modular and less error-prone because there are no state-dependencies.

Something I really like about functional languages (and is kinda contained in what you said about error-proneness) is they often have some pretty amazing Type Systems.

Let's look at a "Hello World" in C:

#include 

int main(){
    printf("Hello World\n");
    return 0;
}

The function main takes no arguments and returns an Int, but there's no way I would know that it is actually doing IO inside it's body, unless I look at the functions body.

I can even change it and only get a warning.

#include 

char* main(){
    printf("Hello World\n");
    return 0;
}

hello.c:3:7: warning: return type of ‘main’ is not ‘int’ [-Wmain]
 char* main(){

The same code in Haskell,

module Main where

main :: IO ()
main = do
  putStrLn "hello world"

The function putStrLn has type Str -> IO(), to put it simply, it takes a String and returns some IO() stuff. Main also returns IO().

If I try to change the main's type to main :: String I would get the following error:

module Main where

main :: String
main = do
  putStrLn "hello world"

hello/src/Main.hs:4:1: error:

    • Couldn't match type ‘[Char]’ with ‘IO t0’
      Expected type: IO t0
        Actual type: String
    • In the expression: main
      When checking the type of the IO action ‘main’
  |
4 | main = do
  | ^

hello/src/Main.hs:5:3: error:
    • Couldn't match type ‘IO ()’ with ‘[Char]’
      Expected type: String
        Actual type: IO ()
    • In a stmt of a 'do' block: putStrLn "hello world"
      In the expression: do putStrLn "hello world"
      In an equation for ‘main’: main = do putStrLn "hello world"
  |
5 |   putStrLn "hello world"
  |   ^^^^^^^^^^^^^^^^^^^^^^

That is, Haskell is telling me that putStrLn will return some IO(), so main is expected to do the same, since it returns putStrLn. Actually it wasn't even required to give main a type, since Haskell has a pretty powerful Type System based on Hindley–Milner Type Inference.

This was a really trivial example, but it is often the case that most Runtime Errors in many languages will be caught as Compilation Errors in pure functional languages. Some languages, like Coq, are so strong that you can prove theorems with it!

• or assume an already existing intuitive familiarity with either $\lambda$-calculus or the practicalities of functional programming. (Essentially these explanations suffer from the curse of knowledge: the authors cannot place themselves in the shoes of someone who doesn't have their intuition yet).

This is actually a problem with Haskell (Survey 2017)


Most people want the Haskell community to be bigger. To that end, many
people want the community to be less divisive (for example Stack
versus Cabal) or less elitist (for example putting down other
languages). Also more beginner and intermediate documentation and
tutorials would help.

Some pure Functional languages you might want to give a try:

• Haskell

• Elm

• Coq

Here are some references I've been using through the years to get some familiarity with FP and it's theory.

Some references on the $\lambda$-Calculus:

Books

• Lambda-Calculus and Combinators: I've only read the first 3 chapters, but it's a pretty solid introduction to the theory of $\lambda$-calculus.

Lecture Notes

• Lambda-Calculus and Types: Lecture notes from a Oxford class with the same name.

• Lecture Notes on the Lambda Calculus: Lecture notes from the University of Ottawa.

• Introduction to Functional Programming: Lecture notes from a Cambridge course.

Quick Talks

• Adam McCullough - Greek Classics: Lambda Calculus For Beginners

• Steven Syrek - Lambda Calculus For People Who Can't Be Bothered to Learn It - part 1 of 2

• Steven Syrek - Lambda Calculus For People Who Can't Be Bothered to Learn It - part 2 of 2

Lectures

• Dana Scott - Theory and Models of Lambda Calculus Untyped and Typed : A five lecture series by Dana Scott.

Some theory about Functional Programming:

Books

• The Algebra of Programming

• Purely Functional Data Structures

• Type Theory and Functional Programming

• Software Foundations: A free course on Coq, Functional Programming, Logic and Progra

StackExchange Computer Science Q#86937, answer score: 4