Đẩy If Lên, Đẩy For Xuống: Nguyên Lý, Đại Số và Giới Hạn

Trong bài viết này, tác giả Debasish Ghosh phân tích nguyên lý "đẩy if lên, đẩy for xuống" — một kinh nghiệm lập trình được TigerBeetle đề xuất trong tài liệu Tiger Style. Ý tưởng cốt lõi là tập trung logic rẽ nhánh vào hàm gọi, trong khi đẩy các vòng lặp xuống xử lý theo lô để giảm chi phí và tận dụng tối ưu hóa phần cứng. Bài viết mở rộng nguyên lý này sang tối ưu truy vấn cơ sở dữ liệu, lập trình hàm và lý thuyết phạm trù, rồi chỉ ra những giới hạn cụ thể.

Nguyên lý cơ bản

Theo Tiger Style, một trong những khuyến nghị quan trọng là tập trung hóa luồng điều khiển. Khi tách một hàm lớn, hãy cố giữ toàn bộ câu lệnh switch/if ở hàm "cha", và chuyển các đoạn logic không rẽ nhánh sang hàm phụ trợ. Nói cách khác: mọi luồng điều khiển nên do một hàm duy nhất đảm nhiệm, phần còn lại không cần bận tâm đến nó.

Cụ thể, nguyên lý này đề xuất hai thao tác bổ trợ cho nhau:

• Đẩy if lên: Nếu một hàm rẽ nhánh dựa trên đầu vào, hãy chuyển nhánh đó lên hàm gọi. Ví dụ, thay vì để hàm tự bóc tách Option, hàm gọi xử lý trường hợp None và hàm nhận thẳng giá trị đã bóc tách. Kiểu dữ liệu của hàm giờ đã thể hiện điều kiện tiên quyết của nó.
• Đẩy for xuống: Trì hoãn vòng lặp cho đến sau khi đã lọc hoặc thu gọn tập dữ liệu. Thay vì gọi hàm trong một vòng lặp, hãy cung cấp một phiên bản xử lý theo lô và để vòng lặp nằm bên trong. Nhờ đó vòng lặp "nóng" chạy không có nhánh rẽ và có thể được vector hóa.

Hai thao tác này kết hợp với nhau. Với một tập các giá trị Option, hàm gọi loại bỏ các None, bóc tách phần còn lại thành một mảng, rồi chuyển cho hàm xử lý theo lô — hàm này không bao giờ phải xét đến trường hợp None.

Tương đồng trong truy vấn cơ sở dữ liệu

Nguyên lý tương tự cũng xuất hiện trong tối ưu hóa truy vấn SQL. Điều đã được biết rõ là nên thực hiện chiếu (projection) và chọn (selection) càng sớm càng tốt, đồng thời trì hoãn các phép kết nối (join) cho đến sau.

Điểm thú vị là thuật ngữ ở đây có vẻ ngược với cách gọi thông thường. Một kế hoạch truy vấn là một cây mà lá là các phép quét bảng và gốc tạo ra kết quả. Dữ liệu chảy từ lá lên gốc, nên "xuống cây" nghĩa là "sớm hơn trong quá trình thực thi". Khi bộ tối ưu nói về "đẩy vị từ xuống" (push predicate down), nghĩa là đánh giá nó càng sớm càng tốt.

• Chiếu và chọn sớm: Phép chiếu chỉ chọn các cột cần thiết, giảm chiều rộng dữ liệu. Phép chọn (mệnh đề WHERE) đóng vai trò bộ lọc. Cả hai được đẩy xuống cây kế hoạch để thực thi sớm, loại bỏ dữ liệu không liên quan trước khi chuyển sang các bước sau.
• Trì hoãn phép kết nối: Phép join rất tốn kém tính toán. Bộ tối ưu đẩy phép chọn và chiếu xuống dưới phép join, để phép join chạy trên đầu vào nhỏ hơn.
• Thực thi vector hóa: Kiểu thực thi Volcano xử lý từng hàng một, mỗi toán tử được gọi một lần cho mỗi bộ dữ liệu. Kiểu thực thi vector hóa gọi mỗi toán tử một lần cho cả lô khoảng một nghìn bộ dữ liệu và chạy vòng lặp bên trong. Chi phí thiết lập và quyết định chỉ trả một lần cho mỗi lô, còn vòng lặp bên trong ít nhánh và thân thiện với bộ nhớ đệm.

Tương đồng trong lập trình hàm và lý thuyết phạm trù

Đẩy if lên như việc giới hạn về một đối tượng con

Trong lý thuyết phạm trù, khi nói về phạm trù các tập hợp, ta có thể có một vị từ p : A -> Bool. Các phần tử hoặc thỏa mãn vị từ, hoặc không. Xét tập con các phần tử thỏa mãn: {a ∈ A | p a}, kèm theo một phép nhúng {a | p a} ↪ A. Tập con cùng phép nhúng này xác định một đối tượng con (subobject).

Liên hệ lại với matklad: trước đây hàm nhận mọi A và chạy if p(a) bên trong. Sau khi đẩy if lên, hàm gọi thực hiện kiểm tra, còn kiểu đầu vào của hàm nhận chỉ là tập con đó. Hàm không còn cần if nữa, vì mọi đầu vào nó có thể nhận đều đã vượt qua kiểm tra. Trong code, tập con này được biểu diễn bằng kiểu dữ liệu — ví dụ Walrus thay vì Option.

Về mặt phạm trù, Option chính là đồng tích (coproduct) 1 + Walrus: hoặc không có gì, hoặc có một con walrus. Đẩy if lên tách đôi cặp hàm đó: hàm gọi xử lý thành phần 1, còn hàm lõi chỉ xử lý thành phần Walrus.

Lọc, ánh xạ và định luật liên hệ chúng

Lời khuyên "lọc trước khi ánh xạ" (filter before map) cũng phản ánh nguyên lý này. Tuy nhiên hai biểu thức sau không tương đương:

filter p (map f xs)   -- p kiểm tra *đầu ra* của f
map f (filter p xs)   -- p kiểm tra *đầu vào* của f

Định luật thực sự liên hệ chúng là:

filter p . map f  ==  map f . filter (p . f)

Định luật này suy ra từ tính tham số (parametricity), dễ thấy nhất khi phân tích hàm lọc qua Maybe:

keep :: (a -> Bool) -> a -> Maybe a
keep p x = if p x then Just x else Nothing
filter p = catMaybes . map (keep p)

Ở đây filter p không phải là phép biến đổi tự nhiên (natural transformation), nhưng catMaybes :: [Maybe a] -> [a] thì đúng là vậy — và tính tự nhiên nằm ở đó. Nhờ đó, định luật trên là một phép tính ngắn gọn, dựa vào việc keep p . f == fmap f . keep (p . f).

Điểm cần lưu ý: vế phải không tự động rẻ hơn. filter (p . f) vẫn phải tính f cho mọi phần tử để kiểm tra. Phép viết lại chỉ có lợi khi p . f rút gọn thành một vị từ rẻ q trên đầu vào — thường là vì p chỉ kiểm tra một phần giá trị mà f giữ nguyên. Khi đó f chỉ chạy trên các phần tử sống sót. Cả hai vế vẫn là một lượt O(n), thứ tiết kiệm được là các lời gọi f trên những phần tử lẽ ra sẽ bị bỏ.

Tổng kết về giới hạn của nguyên lý

Điểm mấu chốt là ta có thể có những nguyên lý chung dẫn dắt tới một "đại số" tốt hơn cho codebase hay toàn hệ thống. Nhưng tất cả đều chỉ đúng khi thỏa mãn một số ràng buộc:

• Đưa if ra khỏi vòng lặp chỉ hợp lệ khi điều kiện là bất biến theo vòng lặp (loop-invariant). Điều kiện phụ thuộc từng phần tử không thể rời khỏi vòng lặp — nó chỉ có thể chuyển ra biên và được ghi lại bằng kiểu dữ liệu, như Walrus thay vì Option.
• Đẩy phép chọn xuống dưới phép join chỉ hợp lệ khi vị từ chỉ tham chiếu các cột từ một phía của phép join.
• Lọc trước khi ánh xạ hợp lệ nhờ định luật filter p . map f == map f . filter (p . f), và chỉ tiết kiệm công sức khi p . f rút gọn thành vị từ rẻ trên đầu vào.

Với phần "đẩy for xuống", vấn đề nằm ở chi phí chứ không phải tính tương đương. Ta thay đổi hình dạng của mũi tên từ A -> B thành [A] -> [B] để chi phí thiết lập chỉ phải trả một lần cho mỗi lô.

Chính đại số mới nói cho ta biết phép viết lại nào là hợp lệ. Trong trường hợp filter/map, tính tự nhiên của catMaybes là thứ dẫn dắt tính hợp lệ và giúp ta lý giải cấu trúc tổng thể của code.