Mọi thứ đều là hàm: Cảm nhận sau khóa học SICP với David Beazley
(ezzeriesa.notion.site)Cảm nhận sau khóa học SICP với David Beazley: trải nghiệm trong 1 tuần
Chia sẻ trải nghiệm tham gia khóa học SICP của David Beazley vào cuối năm 2022. Dù có nhiều tài liệu miễn phí, khóa học của Dave đặc biệt hiệu quả nhờ chọn lọc các chủ đề cụ thể và giải thích chúng một cách sâu sắc.
Điểm khởi đầu
Khóa học SICP được giảng dạy bằng ngôn ngữ Scheme, và tại đây người học triển khai một trình thông dịch Scheme đơn giản bằng Python để giải thích mô hình thế (substitution), một khái niệm nền tảng.
Cơ bản về ngôn ngữ Scheme
- Primitive: các giá trị cơ bản (ví dụ: số nguyên)
- Toán tử: dùng các phép toán cơ bản như
+,-,*,/dưới dạng ký pháp tiền tố - define: định nghĩa biến
> (define x 2)
> (+ x 3) ; kết quả: 5
- if: câu lệnh điều kiện
- lambda: định nghĩa hàm ẩn danh
> ((lambda (x) (* x x)) 3) ; kết quả: 9
Trình thông dịch Scheme trong Python
Triển khai một trình thông dịch đơn giản để đánh giá mã Scheme bằng Python. Các phép toán cơ bản được định nghĩa bằng hàm Python.
definitions = {
"+": lambda x, y: x + y,
"*": lambda x, y: x * y,
}
Ví dụ:
> evaluate(("+", 2, 3)) # kết quả: 5
Ngoài ra còn bao gồm việc hiện thực define, lambda, và cả xử lý câu điều kiện if.
Mô hình thế (Substitution Model)
Mô hình thế là cách diễn giải chương trình đơn giản, trong đó chương trình được đánh giá bằng cách thay biến bằng giá trị. Tuy nhiên, khi có gán giá trị (assignment) thì mô hình này không còn đúng nữa.
Trạng thái (State)
Một ví dụ cho việc mô hình thế bị phá vỡ là gán giá trị (assignment). Chẳng hạn, khi mô hình hóa số dư tài khoản ngân hàng, ta cập nhật biến bằng set!.
(define balance 100)
(define (withdraw amount)
(set! balance (- balance amount))
balance)
Trong trường hợp này, mô hình thế không thể phân biệt được trạng thái số dư trước và sau đó.
Khi ấy cần đến mô hình môi trường (Environment). Biến được định nghĩa trong môi trường, và mỗi thủ tục có môi trường riêng của nó.
Stream
Một cách khác để mô hình hóa trạng thái là dùng stream. Stream có thể mô hình hóa cả các giá trị trong tương lai thông qua đánh giá trì hoãn (lazy evaluation).
Vòng lặp vô hạn và thứ tự đánh giá
Sự khác biệt về thứ tự đánh giá: hầu hết ngôn ngữ dùng applicative-order evaluation, tức là đánh giá đối số trước.
> (square (+ 1 2)) ; kết quả: 9
Tuy nhiên, normal-order evaluation trì hoãn việc đánh giá cho đến khi đối số thực sự cần thiết. Nhờ đó có thể tránh được vòng lặp vô hạn.
> (define (p) (p))
> (define (test x y) (if (= x 0) 0 y))
> (test 0 (p)) ; với normal-order trả về 0, với applicative-order thì lặp vô hạn
Lambda calculus và số Church
Thông qua Church encoding, có thể biểu diễn số dưới dạng thủ tục (procedure). Đây là một khái niệm quan trọng trong lập trình hàm.
(define (zero f) (lambda (x) x))
(define (increment n) (lambda (f) (lambda (x) (f ((n f) x)))))
zerolà hàm trả nguyên đối số (identityfunction).incrementáp dụng thêm một lần gọi hàm.
Ví dụ
> ((zero (lambda (x) (+ x 1))) 0) ; kết quả: 0
> (((increment zero) (lambda (x) (+ x 1))) 0) ; kết quả: 1
Lặp vs đệ quy
Scheme dùng đệ quy thay cho vòng lặp for để thực hiện các tác vụ lặp lại.
Ví dụ đệ quy: giai thừa
(define (factorial n)
(if (= n 1)
1
(* n (factorial (- n 1)))))
Lời gọi đệ quy này có thể dùng stack và tiêu tốn khá nhiều bộ nhớ.
Tối ưu tail-call
Scheme giảm mức sử dụng bộ nhớ thông qua tối ưu tail-call. Nhờ vậy, nó hoạt động giống một tiến trình lặp (iterative) hơn.
(define (factorial n)
(define (iter product counter)
(if (> counter n)
product
(iter (* product counter) (+ counter 1))))
(iter 1 1))
Kết luận
Khóa học của David Beazley chọn ra các khái niệm cốt lõi của SICP và đào sâu chúng. Đặc biệt, nó giúp hiểu rõ hơn nhiều mô hình lập trình khác nhau như lập trình hàm, lambda calculus và thứ tự đánh giá.
Trích dẫn của Knuth
Nếu chỉ học lý thuyết, điều đó có nghĩa là đã đến lúc tập trung vào phần thực hành; còn nếu chỉ làm thực hành, điều đó có nghĩa là đã đến lúc tập trung vào phần lý thuyết.
1 bình luận
Ý kiến trên Hacker News
Xin cảnh báo rằng nếu đi sâu vào SICP/Lisp/Scheme, cách bạn nghĩ về lập trình có thể thay đổi, và kiểu kích thích trí tuệ như vậy luôn đáng hoan nghênh
Nhưng nếu áp dụng nguyên xi những ý tưởng đó vào một codebase hướng đối tượng, thường sẽ phản tác dụng hoặc khiến đồng đội phản đối
Ví dụ, sau khi học Lisp, bạn có thể muốn đổi mọi vòng lặp
forthànhforEach, hoặc biến mọi thứ thành chuỗimap/reduce; nhưng nếu ngôn ngữ không thực sự ôm trọn lập trình hàm, điều đó có thể làm hại cả khả năng đọc lẫn hiệu năngRốt cuộc, việc nhớ rằng bộ nhớ khả biến và CPU mới là thứ xử lý mã sẽ giúp ta giữ được nền tảng; ngày nay, tôi cho rằng thiết kế hướng dữ liệu và “sự đồng cảm cơ học” phù hợp với thực tế phần cứng thường thực dụng hơn trong công việc hằng ngày so với các khái niệm trừu tượng như số Church
Càng ít tác dụng phụ thì càng dễ dự đoán hơn, còn hướng đối tượng thường được dùng cả ở những nơi chỉ cần hàm là đủ
Trong phát triển game, vì có nhiều phép tính và mã nguy hiểm nên hướng đối tượng khá phù hợp, nhưng trong phát triển web thì lập trình hàm tự nhiên hơn nhiều; với SaaS, các ngôn ngữ như Elixir giúp viết mã đáng tin cậy hơn, ít lỗi hơn và dễ kiểm thử hơn
Hơn nữa, những thứ như
forEach,map/reduceđã có trong các collection của Smalltalk, và dù không phải cú pháp hạng nhất, chúng cũng đã được sao chép sang Object Pascal, C++Vì bộ nhớ bên dưới là khả biến, nên khi thật sự cần, các ngôn ngữ họ ML cũng có cơ chế để xử lý biến đổi
goto, nhưnggotocòn kém được ưa chuộng hơn cả LispĐiều kỳ lạ hơn là trên CPU hiện đại, muốn có hiệu năng thì cache là thiết yếu, vậy mà vẫn chưa có ngôn ngữ nào coi phân cấp bộ nhớ là công dân hạng nhất
Thứ gần nhất có lẽ là kiểu C của Linux, nơi dấu gạch dưới tràn ngập như biển
Cung cấp một phần nhập môn tốt về cách mã hóa trạng thái bằng hàm thuần
Trên thực tế, có rất nhiều cách mã hóa thuần hàm cho đủ loại dữ liệu như cây, số nguyên, kiểu tổng/tích, hình ảnh, monad, v.v.
Cách mã hóa có thể hơi gây bối rối, nhưng đồng thời cũng thanh nhã và nhỏ gọn
Ví dụ, nếu triển khai Maybe monad theo kiểu hàm trong JavaScript thì sẽ như sau:
Nothing = nothing => just => nothingJust = v => nothing => just => just(v)pure = Justbind = mx => f => mx(mx)(f)evalMaybe = maybe => maybe("Nothing")(v => "Just " + v)console.log(evalMaybe(bind(Nothing)(n => pure(n + 1)))) // Nothingconsole.log(evalMaybe(bind(Just(42))(n => pure(n + 1)))) // Just 43data Maybe a = Nothing | Just afoldMaybe :: (Unit -> r) -> (a -> r) -> Maybe a -> rHai hàm bậc cao truyền vào
foldMaybelần lượt tương ứng vớiNothingvàJustTuy nhiên, phía
Nothingđược thêm tham sốUnitđể chính xác hơn một chútTrong lý thuyết kiểu thì khá thú vị, nhưng trong lập trình thực tế thì không tốt lắm
Trước đây tôi đã xem bài giảng SICP thật sự, tức bản ghi hình năm 1986 của MIT OCW
Nó thường được khen là có mật độ thông tin cao, nhưng thực tế khá nhiều thời gian bị lãng phí vào phần hỏi đáp của sinh viên, thời gian giảng viên thu hút sự chú ý khi thử trình bày “đa phương tiện” trong lớp, và những chỗ do kế hoạch tổng thể của buổi học chưa được sắp xếp hoàn toàn từ trước nên không thể chủ động chặn các câu hỏi đáp
Thời gian viết lên bảng nếu cộng dồn lại cũng đáng kể
Tất nhiên thứ tự tài liệu có thể được tranh luận và sắp xếp lại tùy ý, và một ngày nào đó tôi cũng định tự làm một loạt video giải thích nội dung này theo cảm nhận của mình
Tôi vui vì bài giảng này có vẻ vẫn giữ được gốc rễ trong khi dùng một ngôn ngữ hiện đại hơn như Python, và tôi nghĩ vì Python là một ngôn ngữ đa mô hình thực dụng, nên dù không hoàn toàn thuần khiết, mọi người vẫn chưa đánh giá đủ sức biểu đạt của nó thông qua các thành ngữ lập trình hàm
Tôi nghĩ Python có thể và nên được bỏ khỏi bài giảng này
Python hỗ trợ lập trình hàm rất yếu
List không dựa trên cons, lambda có nhiều hạn chế, pattern matching thì tệ và cũng không dựa trên biểu thức, namespace cũng kỳ lạ
Python cũng khó có thể gọi là ngôn ngữ hiện đại, nó vẫn mắc kẹt ở thập niên 1990, và đáng tiếc là chỉ nhờ có C-API khá ổn mà nó đã phát triển bằng cách hy sinh các ngôn ngữ tốt hơn
Vì không có tối ưu hóa lời gọi đuôi, một số bài tập code cần lời giải hoàn toàn khác với Scheme
Nếu đoạn code dịch 1:1 bị lỗi, không biết giảng viên nên bảo sinh viên cứ tin như vậy vì ngôn ngữ được chọn hoạt động như thế, hay nên xem toàn bộ là bài toán đưa stack ra bên ngoài và giải theo cách đó
Việc cố nhét SICP vào Python trông khá ngớ ngẩn
Trang web hiện đã offline, nhưng có thể xem bài giảng trên archive.org
https://en.m.wikipedia.org/wiki/ArsDigita#ArsDigita_Foundati...
https://archive.org/details/arsdigita_01_sicp/
Họ từng bán USB chứa toàn bộ chương trình học, sẽ rất tuyệt nếu ai đó tải ISO lên
https://web.archive.org/web/20190222145553/aduni.org/drives/
Những thứ diễn đạt đơn giản bằng Scheme lại trở thành các bài tập phức tạp trong ngôn ngữ khác
Thay vì tập trung vào khái niệm nền tảng, sinh viên lại phải tập trung vào các chi tiết của ngôn ngữ triển khai mà trong Scheme không cần bận tâm
Khi lần đầu thấy
cons/car/cdrđược triển khai bằng lambda, tôi thấy như ma thuậtNhưng rốt cuộc tôi cho rằng đó là việc cho thấy runtime của ngôn ngữ đang triển khai từ điển key/value, và ta có thể mượn triển khai đó để tạo các cấu trúc dữ liệu khác
Trong Elixir, bạn có thể lấy ra từ phía trước bao nhiêu tùy ý
Một closure không có hành vi chỉ là con trỏ tới các biến đã được đóng, và một closure có 2 con trỏ là một cặp từ đó có thể lấy
carvàcdrRuntime phải làm cho đối tượng được trỏ tới vẫn có thể dùng được bên ngoài phạm vi định nghĩa, nên cần escape analysis, garbage collection, v.v., nhưng không cần từ điển
Gần đây tôi bắt gặp khái niệm rằng để chứng minh những điều như
0 != 1trong chứng minh định lý thì chỉ Church encoding là không đủ, mà cần kiểu dữ liệu quy nạpTôi đã đăng tạm nội dung liên quan ở đây, kèm một phê bình riêng về SICP: https://intellec7.notion.site/Drinking-SICP-hatorade-and-why...
Tôi muốn hiểu rõ hơn giới hạn của quan điểm “mọi thứ chỉ là hàm”
0 ≠ 1Từ định lý
f = g -> f x = g x, có thể suy luận để tạo ra sự kiện bất đẳng thức ở vế phải, rồi lấy phản đảo của nóNói rằng không thể chứng minh trực tiếp bất đẳng thức giữa các Church numeral nếu không có sự kiện khác về bất đẳng thức thì có vẻ đúng
Ngược lại, trong kiểu dữ liệu quy nạp, hệ thống chứng minh có thể trực tiếp “quan sát” tính bằng nhau hoặc không bằng nhau bằng cách đệ quy loại bỏ áp dụng constructor ngoài cùng ở hai instance cụ thể của cùng một kiểu quy nạp
Tôi tò mò liệu có thể đạt được điều đó bằng Scott encoding hay Church encoding không
Bản thân cuốn sách đã đang được thảo luận ở đây: https://news.ycombinator.com/item?id=42157558
Tôi thắc mắc liệu có lý do gì mà liên kết lại dẫn tới phần thảo luận phía dưới thay vì đầu trang đó không
Có lẽ có thể gộp bài này vào cuộc thảo luận hiện có
David Beazley là một nhân vật khá huyền thoại trong thế giới Python, và lúc đầu khóa học này trông như một ý tưởng đáng kinh ngạc, nhưng nghĩ khoảng 2 giây thì thấy đây là một sự kết hợp hoàn hảo nên tôi đã đăng ký buổi học tiếp theo
Điểm cốt lõi là hình thức như thế này có vẻ sẽ là diện mạo tương lai của giáo dục thường xuyên cho kỹ sư phần mềm
Có lỗi gõ trong mã ở phần “the substitution model”
("+", ("fib", ("-", "n", 2)), ("fib", ("-", "n", 1))),Phần được định nghĩa là
fibonacci, cònfibthì chưa được định nghĩa, nên hai lời gọifibrõ ràng phải làfibonacciMã trong kho GitHub thực tế thì đúng: https://github.com/savarin/pyscheme/blob/0f47292c8e5112425b5...
Tôi nghĩ SICP rất xuất sắc
Tuy nhiên, càng học thêm và nghiên cứu toán nhiều hơn, tôi càng tiến gần tới kết luận rằng quan hệ là khái niệm nguyên thủy nền tảng hơn
Mọi hàm đều có thể biểu diễn như một dạng quan hệ bị giới hạn, nhưng chiều ngược lại thì không đúng nếu không thêm vào khá nhiều cơ chế bổ sung
Cơ sở dữ liệu quan hệ và SQL tuy là ví dụ nổi tiếng và thành công nhất của lập trình quan hệ, nhưng tôi cho rằng lĩnh vực này vẫn còn phần lớn chưa được khai phá
Hiện mối quan tâm của tôi nghiêng về việc dạy nền tảng toán học cho trẻ rất nhỏ hơn là thiết kế ngôn ngữ lập trình
Lạ là dạy các vị từ như “lớn” dưới dạng quan hệ một ngôi, và “lớn hơn” dưới dạng quan hệ hai ngôi, lại dễ hơn rất nhiều so với cố gắng nắm bắt cùng khái niệm đó bằng hàm
Tôi không thích lắm quan điểm “mọi thứ đều là hàm” vì nó bị đơn giản hóa quá mức và thường không hữu ích
Ví dụ có những hàm không vừa trong cache, RAM, đĩa, v.v.; có những hàm mà độ phức tạp Big-O bùng nổ như
JOINN chiều hoặc tìm kiếm/khớp mẫu; và có cả các hàm có hiệu ứng phụ, bao gồm cả tính không lũy đẳngHầu như chẳng ai nghĩ đến tấn công kênh bên đối với hàm
Cũng có các hàm bất định phụ thuộc vào ngày, giờ, khoảng thời gian, v.v.; hàm có thể thất bại giữa chừng hoặc không thất bại một cách nhã nhặn
Cũng khó giả định rằng chúng không tiêu thụ tài nguyên gây ảnh hưởng đến các “hàm” khác dùng chung một nhóm tài nguyên
Đối số của hàm có thể lớn hoặc phức tạp tùy ý, nhưng thực tế thì có giới hạn; khi đó cần đến con trỏ, rồi lại cần tham chiếu từ xa như web hay đĩa
Cứ bảo tôi lúc nào nên dừng, tôi có thể nói tiếp mãi
Trong trường hợp này, mô hình phép tính lambda là nền tảng của cách tiếp cận “mọi thứ chỉ là hàm”; nó rất đơn giản nhưng vẫn dễ xử lý và suy luận hơn so với máy Turing, nên là một mô hình tính toán tốt
Vì vậy nó nằm ở nền tảng của phần lớn logic máy tính và các hệ thống chứng minh
Nếu một hàm cần tài nguyên thì hãy khiến nó yêu cầu tài nguyên đó; nếu phụ thuộc vào ngày/giờ thì hãy khiến nó phụ thuộc vào ngày/giờ; nếu trả về giá trị bất định thì hãy khiến nó trả về giá trị bất định
Một trong những lý do cách tiếp cận lập trình hàm tỏa sáng là vì nó buộc ta phải xử lý nghiêm túc những điều này
Nếu muốn dùng tài nguyên được chia sẻ ngầm, bạn phải mô hình hóa nó; và “hàm” phụ thuộc vào tài nguyên chia sẻ ngầm sẽ được phân biệt rõ ràng với hàm thực sự
Chúng gần với thủ tục hơn
Hàm là thủ tục, nhưng không phải thủ tục nào cũng là hàm