Посоветуйте хорошую книгу по ФП

Барендрегт, "Ламбда исчисление" (именно так, через "а").

SICP?

Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы.

SICP к языку привязан, и собственно про ФП не говорит вообще ничего.

Однако, тяготеет к функциональному стилю.

Начать с Филда-Харрисона.

Тогда только первые две главы читать надо - дальше он на ML зацикливается.

Oops, я затупил, решил, что про Харрисона говорят.

Филд-Харрисон вообще для изучения ФП не годится, это хорошее такое руководство по практической реализации функциональных языков, прекрасно дополняющее книгу под редакцией С.П.Джонса. Но учиться по нему нельзя, однозначно. Кроме того, в русском издании до фига опечаток.

Я почему-то решил, что спрашивают про блямбда-исчисление, а не фп вообще.

Лямбда-исчисление и есть та теория, на которой строится ФП. Если изучать ФП, не затрагивая никакого конкретного языка, то это и сведется к изучению лямбда-исчисления, теории категорий, комбинаторной логики, и т.п.

sicp, а потом все остальное

> SICP к языку привязан, и собственно про ФП не говорит вообще ничего.

Мы один и тот же SICP читали? Он очень слабо не привязан к языку, хотя и использует только Scheme. По крайней мере все что там пишется отлично укдалывается на любой мультипарадигменный (ИП+ФП) язык. Есть же SICP с кодом на Python.

Правда, да, речь там не столько про ФП конкретно, сколько про computer science вообще.

B. Jacobs, Categorical Logic and Type Theory,

Chapter 1: Introduction to fibred category theory
1. Fibrations
2. Some concrete examples: sets, omega-sets and PERs
3. Some general examples
4. Cloven and split fibrations
5. Change-of-base and composition of fibrations
6. Fibrations of signatures
7. Categories of fibrations
8. Fibrewise structure and fibred adjunctions
9. Products and coproducts
10. Indexed categories
Chapter 2: Simple type theory
1. The basic calculus of types and terms
2. Functorial semantics
3. Exponents, products and coproducts
4. Semantics of simple type theories
5. Semantics of the untyped lambda calculus as a corollary
6. Simple parameters
Chapter 3: Equational Logic
1. Logics
2. Specifications and theories in equational logic
3. Algebraic specifications
4. Fibred equality
5. Fibrations for equational logic
6. Fibred functorial semantics
Chapter 4: First order predicate logic
1. Signatures, connectives and quantifiers
2. Fibrations for first order predicate logic
4. Functorial interpretation and internal language
5. Subobject fibrations I: regular categories
6. Subobject fibrations II: coherent categories and logoses
7. Subset types
8. Quotient types
9. Quotient types, categorically
10. A logical characterisation of subobject fibrations
Chapter 5: Higher order predicate logic
1. Higer order signatures
2. Generic objects
3. Fibrations for higher order logic
4. Elementary toposes
5. Colimits, powerobjects and well-poweredness in toposes
6. Nuclei in a topos
7. Separated objects and sheaves in a topos
8. A logical description of separated objects and sheaves
Chapter 6: The effective topos
1. Constructing a topos from a higher order fibration
2. The effective topos and its subcategories of sets, omega-sets, and PERs
3. Families of PERs and omega-sets over the effective topos
4. Natural numbers in the effective topos and some associated principles
Chapter 7: Internal category theory
1. Definition and examples of internal categories
2. Internal functors and natural transformations
3. Externalisation
4. Internal diagrams and completeness
Chapter 8: Polymorphic type theory
1. Syntax
2. Use of polymorphic type theory
3. Naive set theoretic semantics
4. Fibrations for polymorphic type theory
5. Small polymorphic fibrations
6. Logic over polymorphic type theory
Chapter 9: Advanced fibred category theory
1. Opfibrations and fibred spans
2. Logical predicates and relations
3. Quantification
4. Category theory over a fibration
5. Locally small fibrations
6. Definability
Chapter 10: First order dependent type theory
1. A calculus of dependent types
2. Use of dependent types
3. A term model
4. Display maps and comprehension categories
5. Closed comprehension categories
6. Domain theoretic models of type dependency
Chapter 11: Higher order dependent type theory
1. Dependent predicate logic
2. Dependent predicate logic, categorically
3. Polymorphic dependent type theory
4. Strong and very strong sum and equality
5. Full higher order dependent type theory
6. Full higher order dependent type theory, categorically
7. Completeness of the category of PERs in the effective topos

> речь там не столько про ФП конкретно, сколько про computer science вообще.

Именно. Про ФП там вообще ничего нет. Это общее руководство по программированию для начинающих.