Lập trình hàm

Trong ngành khoa học máy tính, lập trình hàm là một mô hình lập trình xem việc tính toán là sự đánh giá các hàm toán học và tránh sử dụng trạng thái và các dữ liệu biến đổi. Lập trình hàm nhấn mạnh việc ứng dụng hàm số, trái với phong cách lập trình mệnh lệnh, nhấn mạnh vào sự thay đổi trạng thái. Lập trình hàm xuất phát từ phép tính lambda, một hệ thống hình thức được phát triển vào những năm 1930 để nghiên cứu định nghĩa hàm số, ứng dụng của hàm số, và đệ quy. Nhiều ngôn ngữ lập trình hàm có thể được xem là những cách phát triển giải tích lambda.
Trong thực tế, sự khác biệt giữa hàm số toán học và cách dùng từ "hàm" trong lập trình mệnh lệnh đó là các hàm mệnh lệnh có thể tạo ra hiệu ứng lề, làm thay đổi giá trị của một phép tính trước đó. Vì vậy các hàm kiểu này thiếu tính trong suốt tham chiếu, có nghĩa là cùng một biểu thức ngôn ngữ lại có thể tạo ra nhiều giá trị khác nhau vào các thời điểm khác nhau tùy thuộc vào trạng thái của chương trình đang thực thi. Ngược lại, trong lập trình hàm, giá trị xuất ra của một hàm chỉ phụ thuộc vào các tham số đầu vào của hàm, vì thế gọi hàm f hai lần với cùng giá trị tham số x sẽ cho ra cùng kết quả f(x). Việc loại bỏ hiệu ứng lề có thể làm cho chương trình dễ hiểu hơn rất nhiều và người ta có dự đoán được hành vi của một chương trình, đó chính là một trong các động lực chính cho sự phát triển của lập trình hàm.
Các ngôn ngữ lập trình hàm, đặc biệt là các loại thuần lập trình hàm, có ảnh hưởng lớn trong giới học thuật hơn là dùng để phát triển các phần mềm thương mại. Tuy vậy, các ngôn ngữ lập trình hàm nổi bật như Scheme, Erlang, Objective Caml, và Haskell đã được nhiều tổ chức khác nhau sử dụng trong các ứng dụng công nghiệp và thương mại. Lập trình hàm cũng được sử dụng trong công nghiệp thông qua các ngôn ngữ lập trình chuyên biệt như R (thống kê), Mathematica (toán học hình thức), J và K (phân tích tài chính), F# trong Microsoft.NET và XSLT (XML). Các ngôn ngữ chuyên biệt dạng khai báo được sử dụng rộng rãi hiện nay như SQL và Lex/Yacc, cũng sử dụng một số thành phần của lập trình hàm, đặc biệt để tránh các giá trị biến đổi. Các bảng tính (spreadsheet) cũng có thể được xem là các ngôn ngữ lập trình hàm.
Lập trình theo phong cách lập trình hàm cũng có thể thực hiện ở các ngôn ngữ không được thiết kế riêng cho lập trình hàm. Ví dụ, ngôn ngữ lập trình mệnh lệnh Perl đã có một cuốn sách viết về cách áp dụng các khái niệm lập trình hàm vào đó. JavaScript, một trong các ngôn ngữ được dùng nhiều hiện nay, có khả năng lập trình hàm.

Các khái niệm

Một số khái niệm và mô hình chỉ có ở lập trình hàm, và thường xa lạ với kiểu lập trình mệnh lệnh (bao gồm cả lập trình hướng đối tượng). Tuy nhiên, các ngôn ngữ lập trình thường lai tạp nhiều hình thái lập trình khác nhau để lập trình viên sử dụng các ngôn ngữ "mệnh lệnh nhất" cũng có thể tận dụng một số các khái niệm này.

Hệ thống kiểu, tính đa hình, kiểu dữ liệu đại số và so trùng mẫu

Đặc biệt kể từ sự phát triển của luận kiểu Hindley–Milner trong thập niên 1970, các ngôn ngữ lập trình hàm có khuynh hướng sử dụng phép tính lambda định kiểu, chống lại phép tính lambda bất định kiểu đã được dùng trong Lisp và các biến thể của nó (như Scheme). Việc sử dụng các kiểu dữ liệu đại số và so trùng mẫu làm cho việc thao tác các cấu trúc dữ liệu phức tạp trở nên thuận tiện và rõ ràng hơn; sự tồn tại của việc kiểm tra kiểu mạnh mẽ trong thời gian biên dịch làm cho các chương trình trở nên đáng tin cậy hơn, trong khi đó luận kiểu giải phóng lập trình viên khỏi việc cần phải khai báo thủ công các kiểu để biên dịch.
Một số ngôn ngữ lập trình hàm định hướng nghiên cứu như Coq, Agda, Cayenne, và Epigram dựa trên lý thuyết kiểu intuitionistic, thuyết này cho phép các kiểu phụ thuộc vào các term. Các kiểu như vậy được gọi là các kiểu phụ thuộc. Các hệ thống kiểu này không có các luận kiểu khả định và rất khó để hiểu và lập trình với chúng. Nhưng các kiểu phụ thuộc này có thể mô tả các mệnh đề tự do trong logic mệnh đề. Thông qua Curry–Howard isomorphism, sau đó, các chương trình định kiểu tốt trong những ngôn ngữ này sẽ trở thành các phương tiện cho việc viết các chứng minh toán học hình thức mà từ đó một trình biên dịch có thể sinh ra mã được chứng nhận. Trong khi những ngôn ngữ này chủ yếu được quan tâm trong nghiên cứu học thuật (kể cả trong toán học hình thức hóa), chúng cũng bắt đầu được sử dụng trong kĩ thuật. Compcert là một trình biên dịch cho một tập con của ngôn ngữ lập trình C được viết bằng Coq và đã được chứng thực chính thức.
Một dạng giới hạn của các kiểu phụ thuộc được gọi là kiểu dữ liệu đại số được khái quát hóa (GADT). Dạng này có thể được thực hiện theo cách cung cấp một vài trong số các lợi ích của lập trình phụ thuộc kiểu trong khi tránh hầu hết sự bất tiện của nó. GADT có sẵn trong Trình biên dịch Glasgow Haskell và trong Scala (như "case classes"), và được cho là phần bổ sung vào các ngôn ngữ khác bao gồm cả Java và C#.

Lập trình hàm trong các ngôn ngữ phi hàm

Có thể sử dụng phong cách hàm của việc lập trình trong các ngôn ngữ mà theo truyền thống không được xem là ngôn ngữ hàm. Một số ngôn ngữ phi hàm đã mượn nhiều đặc điểm như các hàm bậc cao hơn, và các quan niệm danh sách từ các ngôn ngữ lập trình hàm. Điều này làm cho việc chấp nhận phong cách hàm dễ dàng hơn khi sử dụng những ngôn ngữ này. Các cấu trúc hàm như các "hàm bậc cao hơn" và các "danh sách lười" có thể lấy được trong C++ qua các thư viện. Trong C, các con trỏ hàm có thể được dùng để đạt được một vài trong số các hiệu quả của các hàm bậc cao hơn. Ví dụ hàm chung map có thể được thực thi bằng cách dùng các con trỏ hàm. Trong Visual Basic 9 và C# 3.0 và cao hơn, các hàm lambda có thể được dùng để viết các chương trình theo phong cách hàm.  Trong Java, các lớp nặc danh đôi khi được sử dụng để mô phỏng các sự đóng, tuy nhiên các lớp nặc danh không phải luôn luôn là các thay thế chính xác cho các sự đóng bởi vì chúng có nhiều khả năng bị hạn chế hơn.
Nhiều mẫu thiết kế hướng đối tượng có thể biểu đạt bằng các thuật ngữ lập trình hàm: ví dụ, mẫu chiến lược đơn giản chỉ ra cách dùng của hàm bậc cao hơn, và mẫu khách viếng thăm gần như tương ứng với một catamorphism, hoặc fold.
Các ích lợi của dữ liệu bất biến có thể được thấy ngay cả trong các chương trình mệnh lệnh, vì thế các lập trình viên thường xuyên cố gắng làm cho một số dữ liệu bất biến ngay cả trong các chương trình mệnh lệnh.