✨Lập trình hàm

Trong ngành khoa học máy tính, lập trình hàm (lập trình chức năng) 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. 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.

Hàm hạng nhất và hàm bậc cao

Hàm bậc cao là các hàm số hoặc có thể nhận các hàm số khác làm tham số hoặc có thể trả về kết quả là hàm số (phép toán vi phân $d/dx$ để tính vi phân của hàm $f$ là một ví dụ của hàm bậc cao trong giải tích).

Các hàm bậc cao có liên hệ chặt chẽ với hàm hạng nhất, ở chỗ các hàm bậc cao và hàm hạng nhất đều cho phép nhận hàm số làm tham số và trả về các hàm khác. Sự khác biệt giữa hai loại này rất mờ nhạt: "bậc cao" mô tả một khái niệm hàm trong toán học tính toán trong các hàm khác, còn "hàm hạng nhất" là một thuật ngữ của ngành khoa học máy tính mô tả các thực thể của ngôn ngữ lập trình trong đó không có giới hạn về việc sử dụng (vì vậy các hàm hạng nhất có thể xuất hiện ở bất cứ đâu trong chương trình, giống như các thực thể hạng nhất khác nhau con số, trong đó có cả việc làm tham số cho các hàm khác và làm giá trị trả về của hàm khác).

Các hàm bậc cao cho phép áp dụng bán phần hoặc currying, một kỹ thuật trong đó hàm lần lượt sử dụng từng tham số của nó, mỗi lần sử dụng lại trả về một hàm mới và chấp nhận tham số tiếp theo. Việc làm này cho phép người lập trình biểu diễn một cách súc tích hàm số kế thừa, tương tự như toán tử cộng sẽ lần lượt cộng từng số tự nhiên lại với nhau.

Hàm thuần túy

Các hàm (hoặc biểu thức) thuần túy hàm không có bộ nhớ hoặc các hiệu ứng lề nhập/xuất. Điều này có nghĩa là các hàm thuần túy có một số đặc tính hữu ích, mà đa số trong chúng có thể dùng để tối ưu mã nguồn:

• Nếu kết quả của một biểu thức thuần túy không được sử dụng, ta có thể xóa nó đi mà không ảnh hưởng đến các biểu thức khác.
• Nếu một hàm thuần túy được gọi cùng với các tham số không tạo ra hiệu ứng lề, kết quả sẽ là hằng số tương ứng với danh sách tham số cụ thể (có khi gọi là trong suốt tham chiếu), tức là hàm thuần túy nếu được gọi lần nữa với cùng bộ tham số, kết quả trả về cũng sẽ y hệt như trước (điều này cho phép tối ưu hóa lưu đệm như memoization).
• Nếu không có sự phụ thuộc về dữ liệu giữa hai biểu thức thuần túy, thì thứ tự của chúng có thể đảo cho nhau, hoặc chúng có thể thực hiện song song mà không ảnh hưởng đến nhau (hay nói cách khác, đánh giá một biểu thức thuần túy bất kỳ là an toàn về luồng (thread-safe)).
• Nếu toàn bộ ngôn ngữ không cho phép hiệu ứng lề, thì chiến thuật đánh giá hàm nào cũng dùng được; việc này trao cho trình biên dịch quyền tự do sắp xếp lại hoặc phối hợp việc đánh giá biểu thức trong một chương trình (ví dụ, dùng kỹ thuật loại bỏ cây).

Trong khi đa số trình biên dịch dành cho các ngôn ngữ lập trình mệnh lệnh có thể nhận dạng hàm thuần túy, và thực hiện các phép khử biểu thức con thường gặp trong các lệnh gọi hàm thuẫn túy, chúng không thể lúc nào cũng làm như vậy đối với các thư viện đã dịch sẵn, thường không tiết lộ thông tin này, vì thế làm cản trở sự tối ưu hóa liên quan đến các hàm bên ngoài như vậy. Một số trình biên dịch, như gcc, thêm từ khóa bổ sung để giúp lập trình viên đánh dấu hàm nào là hàm thuần túy, để cho phép tối ưu hóa kiểu như vậy. Fortran 95 cho phép hàm được chỉ định "thuần túy".

Đệ quy

Vòng lặp trong các ngôn ngữ hàm thường được thực hiện thông qua đệ quy. Hàm đệ quy sẽ tự gọi chính nó, cho phép thực hiện đi thực hiện lại một tác vụ. Việc đệ quy có thể đòi hỏi phải sử dụng một chồng (stack), nhưng đệ quy đuôi vẫn có thể được trình biên dịch nhận ra và tối ưu hóa nó thành cùng đoạn mã được dùng để hiện thực vòng lặp trong ngôn ngữ mệnh lệnh. Tiêu chuẩn của ngôn ngữ Scheme là phải nhận diện và tối ưu hóa được đệ quy đuôi. Một trong những cách tối ưu hóa đệ quy đuôi là chuyển chương trình thành kiểu truyền liên tiếp trong quá trình dịch.

Các mẫu đệ quy phổ biến đều có thể được khử đệ quy bằng các hàm bậc cao, catamorphism và anamorphism (hay "fold" và "unfold" - gấp và mở gấp) là những ví dụ rõ nhất. Các hàm bậc cao như vậy đóng vai trò tương tự như các cấu trúc điều khiển có sẵn như vòng lặp trong ngôn ngữ mệnh lệnh.

Đa số các ngôn ngữ lập trình hàm đa mục đích đều cho phép đệ quy không giới hạn và là Turing complete, khiến cho bài toán dừng trở nên không quyết định được, có thể gây ra sự thiếu căn cứ cho việc suy diễn công thức, và nói chung đòi hỏi phải có khái niệm không nhất quán trong logic do hệ thống kiểu của ngôn ngữ quy định. Một vài ngôn ngữ lập trình với mục đích đặc biệt như Coq chỉ cho phép đệ quy well-founded và chuẩn hóa mạnh (tính toán không dừng chỉ có thể biểu diễn bằng dòng giá trị vô hạn gọi là codata). Kết quả là, những ngôn ngữ như vậy không phải Turing complete và một số hàm không thể biểu diễn trong ngôn ngữ, dù ngôn ngữ đó vẫn có thể biểu diễn được rất nhiều cách tính toán thú vị mà tránh được vấn đề do đệ quy không giới hạn gây ra. Lập trình hàm giới hạn trong việc đệ quy well-founded với một số ràng buộc khác được gọi là lập trình hàm hoàn toàn (total). Xem Turner 2004 để biết thêm.

Tính toán chặt và không chặt

Có thể chia các ngôn ngữ hàm làm hai loại tùy vào việc chúng sử dụng cách tính toán biểu thức chặt (tham lam) hay không chặt (lười biếng), là những khái niệm chỉ cách xử lý thông số của hàm khi tính toán một biểu thức. Sự khác biệt về các cách tính toán này xuất hiện ở ngữ nghĩa biểu thị của biểu thức khi chúng có chứa phép toán lỗi hoặc có vấn đề. Khi tính toán chặt, việc tính toán số hạng có chứa lỗi cũng sẽ dẫn đến lỗi. Ví dụ, biểu thức: :print length([2+1, 3*2, 1/0, 5-4]) sẽ không tính được theo tính toán chặt vì phép chia không tại phần tử thứ ba của danh sách. Còn với tính toán không chặt, hàm length sẽ trả về giá trị 4, vì khi tính toán hàm, nó không cố gắng tính toán các phần tử trong danh sách. Nói một cách ngắn gọn, tính toán chặt luôn luôn tính toán tất cả cấc số hạng của hàm trước khi xử lý hàm. Tính toán không chặt không tính toán tham số của hàm trừ khi nó cần giá trị đó để tính toán hàm.

Cách hiện thực thông thường của tính toán không chặt trong ngôn ngữ hàm là thu giảm đồ thị. Cách tính toán không chặt được dùng mặc định trong vài ngôn ngữ lập trình hàm thuần túy, như Miranda, Clean và Haskell.

Hughes vào năm 1984 đã phản bác việc dùng tính toán không chặt làm cơ chế để tăng tính module hóa của chương trình thông qua quá trình chia nhỏ bài toán, bằng cách làm cho việc hiện thực độc lập giữa nhà sản xuất và khách hàng dễ dàng hơn. Launchbury 1993 mô tả một số khó khăn mà đánh giá lười biếng tạo ra, cụ thể trong việc phân tích yêu cầu lưu trữ của chương trình, và đề xuất ngữ nghĩa hoạt động để hỗ trợ cho việc phân tích này. Harper 2009 đề xuất đưa cả tính toán chặt lẫn không chặt vào một ngôn ngữ, bằng cách dùng hệ thống kiểu của ngôn ngữ để phân biệt chúng.

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.