Giải bài toán "Passport Application" của Anh bằng Haskell

• Xem quy trình xin hộ chiếu ở Anh như một trò chơi giải đố, và kể lại trải nghiệm lập trình hóa quy trình xin đầy phức tạp này bằng Haskell để biến nó thành các quy tắc
• Việc xin hộ chiếu trực tuyến có điểm hấp dẫn cốt lõi là thu thập tài liệu đa dạng, diễn giải các quy tắc phức tạp, cùng những nhiệm vụ phụ bất ngờ
• Liên hệ logic của quá trình nộp đơn với 'Constructive Logic', nhấn mạnh rằng tài liệu gốc là điều bắt buộc để làm cơ sở cho từng chứng minh
• Tận dụng LogicT monad và quản lý trạng thái (State) của Haskell để theo dõi danh sách tài liệu cần thiết và lộ trình logic nhằm chứng minh quốc tịch Anh
• HMPO trên thực tế có xu hướng yêu cầu lộ trình chứng minh phức tạp nhất trước, còn các công cụ tự động hóa vẫn được áp dụng chậm do giới hạn trong việc diễn giải luật pháp phức tạp

---

Mở đầu: Xem việc xin hộ chiếu như một trò chơi

• Gần đây, xu hướng dùng lập trình để giải các trò chơi trực tuyến hay câu đố ngày càng tăng, và Passport Application của Anh cũng được tiếp cận theo cách như vậy
• Passport Application là một kiểu "trò chơi phiêu lưu giải đố thu thập tài liệu" mà người Anh chơi 10 năm một lần, với chi phí khoảng £100 và thiết kế tối giản nghiêm ngặt theo phong cách văn bản
• Mục tiêu của trò chơi này là thu thập nhiều giấy tờ chứng minh (artefacts) thông qua nhiều cơ quan công quyền để chứng minh rằng "đương đơn này là người Anh" theo các tiêu chuẩn pháp lý phức tạp
• Phần thưởng của trò chơi là một cuốn hộ chiếu và "ngày có thể chơi lần tiếp theo"

Cấu trúc và độ khó của trò chơi

• Phiên bản ngoại tuyến trên giấy được thực hiện qua thư bảo đảm và quy trình xác thực, với các tài liệu cần thu thập ở từng bước được hướng dẫn dưới dạng chỉ dẫn hoặc bảng biểu
• Giai đoạn đầu tương đối dễ, nhưng khi trò chơi tiến triển sẽ xuất hiện nhiều "nhiệm vụ phụ" và chướng ngại vật khác nhau
  • Ví dụ: nhờ người quen có nghề nghiệp nhất định xác minh danh tính, xin bản dịch công chứng của giấy tờ bằng tiếng nước ngoài, phối hợp với gia đình, hoặc khám phá quy trình hành chính riêng của từng cơ quan

Trải nghiệm thực tế: thử sức ở độ khó 'đứa con đầu tiên sinh ở nước ngoài'

• Tác giả thay mặt mình thử thách ở độ khó 'đứa trẻ đầu tiên sinh ở nước ngoài' cho cô con gái nhỏ, và do đã có nhiều kinh nghiệm trước đó nên dự đoán đây sẽ là một thử thách khá nặng
• Về sau mới xác nhận rằng một nửa số giấy tờ được yêu cầu ở giai đoạn đầu là không cần thiết, và các yêu cầu cũng như hướng dẫn về hồ sơ được thiết kế khá mơ hồ và dễ gây nhầm lẫn
• Không thể liên lạc trực tiếp với người thẩm định phụ trách (examiner), và chỉ có thể nhận hỗ trợ không chính thức thông qua đại lý trung gian tư vấn
• Các yêu cầu giấy tờ liên tục phát sinh lặp đi lặp lại, đôi khi còn yêu cầu cả những giấy tờ không tồn tại, và độ khó tăng dần với những yêu cầu như nộp giấy khai sinh/giấy đăng ký kết hôn của các tổ tiên xa trong gia đình

Logic của HMPO: Bureaucratic Logic

• Logic của việc xin hộ chiếu có thể được xem là Bureaucratic Logic bắt nguồn từ Constructive Logic
• Thay vì chỉ chứng minh đơn giản kiểu "đúng/sai", người nộp đơn phải trực tiếp nộp chứng cứ là tài liệu gốc tương ứng với từng quy tắc
• Vì không chấp nhận nguyên lý bài trung (Excluded Middle), nên không thể chứng minh theo kiểu "một trong các kịch bản chắc chắn đúng"; bắt buộc phải chọn đúng một lộ trình và nộp giấy tờ theo lộ trình đó
• Đặc biệt, "Britishness" phụ thuộc vào quốc tịch của cha mẹ, nên yêu cầu giấy tờ được triển khai đệ quy theo dạng cây gia đình
  • Trường hợp cơ sở: sinh tại Anh trước năm 1983, nhập tịch, v.v. là những trường hợp không cần giấy tờ chứng minh của cha mẹ

Mô hình hóa quy tắc bằng mã Haskell

• Với mục tiêu mô-đun hóa các quy tắc và tự động hóa suy luận, tác giả đã tạo nguyên mẫu logic nộp đơn bằng Haskell, đặc biệt tận dụng LogicT monad
• Khai báo các kiểu như Person/Document/Proof để mô hình hóa nhiều lộ trình tài liệu chứng minh khác nhau theo từng điều kiện
• Hàm chứng minh Britishness sẽ, cùng với input (thông tin của từng person), khám phá nhiều lộ trình chứng minh khả thi (Set of Proofs)
• Từ cây Proof, hệ thống suy ra tổ hợp tài liệu tối thiểu cần thiết (Set of Set Document)
• Kết hợp StateT và LogicT IO để đặt câu hỏi tương tác và chia sẻ trạng thái, rẽ nhánh & backtracking tùy theo "thông tin đã biết"
• Logic phân tích cấu trúc quốc tịch Anh:
  • Lộ trình đơn cho bằng chứng nhập tịch
  • Lộ trình cơ sở có điều kiện nếu sinh tại Anh trước năm 1983
  • Chứng minh đệ quy thông qua cha mẹ (kèm các điều kiện bổ sung như hôn nhân hợp pháp)
  • Bổ sung lộ trình ngoại lệ tùy theo việc cha mẹ có phải BOTBD (British Otherwise Than By Descent) hay không
  • Các quy định ngoại lệ như Crown Service cũng được xử lý trong mã

Ví dụ chạy thử và các lộ trình chứng minh

• Thông qua ghci, hệ thống tự động rút ra tổng cộng 3 lộ trình chứng minh (Proof) dựa trên dữ liệu nhập thực tế (nơi sinh của người nộp đơn, quốc tịch của cha mẹ, v.v.)
• Với mỗi lộ trình chứng minh, hệ thống xuất ra danh sách tài liệu được yêu cầu (tổ hợp các loại giấy chứng nhận, giấy đăng ký kết hôn, v.v.)
• Ở lộ trình phức tạp nhất, có thể thấy cần đến chứng minh đệ quy và xác nhận quan hệ hôn nhân ngược lên đến cả thế hệ tổ tiên

Thảo luận và kết luận

• Trong thực tế, HMPO có vẻ như cố tình yêu cầu lộ trình chứng minh phức tạp nhất trước; còn các mâu thuẫn pháp lý thực tế hay các quy định tinh vi thì được xử lý theo hướng dẫn riêng hoặc nguyên tắc "balance of probabilities"
• Nếu các công cụ tự động hóa được phổ biến, người nộp đơn sẽ có thể hiểu lộ trình chứng minh của mình và các tài liệu cần thiết dễ dàng hơn nhiều
• Tuy vậy, luật pháp quá tinh vi và dễ thay đổi, nên việc tự động hóa đơn giản kiểu "máy tính đưa ra verdict yes/no" là điều tiềm ẩn rủi ro
• Hiện tại tác giả đang thử chứng minh theo lộ trình thứ hai và thứ ba

---

Tóm tắt mã tham khảo và cấu trúc tài liệu

• Toàn bộ mã Haskell có thể xem trên GitHub
• Có thể xem chi tiết phần triển khai logic Haskell như các kiểu dữ liệu khác nhau, lộ trình chứng minh, cấu trúc module và các hàm truy vấn

[GN⁺]

Ý kiến trên Hacker News

• Chia sẻ trải nghiệm từng làm việc trên nhiều hệ thống lớn của chính phủ Anh trong 10 năm qua; phát triển phần mềm cho chính phủ Anh được mô tả là quá trình mã hóa hàng trăm năm luật của quốc hội. Có khó khăn là khi luật thay đổi, như với hệ thống hộ chiếu HMPO, phải tìm và sửa mọi phần trong từng hệ thống bị luật đó ảnh hưởng. Chính phủ giao việc này cho các công ty tư vấn đắt đỏ, nhưng họ lại có động lực kéo dài hợp đồng tối đa và rút lợi nhuận nhiều nhất từ khách hàng. Trong quá trình đó, chất lượng và độ linh hoạt của hệ thống rất khác nhau, và khi luật lại thay đổi thì toàn bộ thủ tục phức tạp này lặp lại. Dịch vụ chính phủ trở nên đắt đỏ vì thiếu một cơ quan đủ năng lực điều phối vấn đề này bằng các quyết định tập trung
  • Thắc mắc không biết đã từng có trường hợp nào thuê ngoài cho chính phủ thực sự hoạt động tốt hay chưa; chưa từng nghe câu chuyện nào về việc chính phủ giao thầu thứ gì đó mà thành công cả
  • Có câu hỏi về lý do dường như các nhà thầu không có nghĩa vụ theo hợp đồng đối với một “hệ thống hoạt động được”; tò mò vì sao lại có hiện tượng tính phí quá mức cho những hệ thống trông có vẻ ổn nhưng thực tế không vận hành đúng
  • Chia sẻ trải nghiệm gần đây khi gia hạn hộ chiếu ở Pháp: có một nền tảng mới cho mọi loại giấy tờ, chỉ cần điền một biểu mẫu online, chỉ phải đến trực tiếp một lần, hoàn tất trong 10 phút, và hộ chiếu cũng được giao rất nhanh. Anh không đến mức tuyệt vọng, và có suy nghĩ rằng nên tuyển lập trình viên thật sự làm nhân viên chính thức để tự phát triển nội bộ
• Gợi nhớ đến một trường hợp dùng DSL để tự động hóa và mã hóa luật thuế Hà Lan; đề xuất tài liệu liên quan là bài trình bày case DSL của Jetbrains
• Về “base case” trong cấu trúc xác định quyền công dân, có ví dụ rằng người sinh tại Anh trước năm 1983 thì đủ tư cách công dân bất kể cha mẹ là ai. Người bình luận nói mình đến từ một nước mà chuyện quốc tịch chỉ cần một câu SELECT trên bảng SQL là xong, nên cấu trúc như vậy thật khó tin
• Về nhận xét rằng cú pháp của Haskell là trực quan: có ý kiến cho rằng sau khi được ai đó giải thích thì nó có vẻ trực quan, nhưng trước đó thì không. Haskell có quá nhiều toán tử, và có ví dụ rằng nhìn vào code cũng khó hiểu ngay; kèm link hướng dẫn toán tử Haskell
  • Có người nói thử đếm sơ số lượng toán tử thực tế dùng trong Haskell thì gần tương đương hoặc nhiều gấp đôi JavaScript. Haskell có rào cản nhập môn ban đầu, nhưng những ngôn ngữ đầu tiên như Java, Python cũng phức tạp theo cách riêng; chỉ là khi đã học và quen tay thì thấy dễ hơn. Ngay cả cú pháp cơ bản của Python như : và = cũng là điểm dễ gây nhầm lẫn cho người mới, nên tính trực quan là kết quả của sự quen thuộc
  • Tranh luận rằng nếu sau khi được ai đó giải thích mà nó trở nên trực quan, thì điều đó rốt cuộc cũng khá gần với khái niệm “trực quan”
  • Có nhắc rằng Larry Wall từng nói điều tương tự về Perl; thực ra vấn đề không phải là cú pháp mà là nếu không biết các khái niệm đặc trưng của Haskell như monad, lens, v.v. thì dù cú pháp đơn giản đến đâu cũng khó mà hiểu được
  • Chỉ ra rằng phần lớn các toán tử trong link đó là điều khá bình thường với người mới học lập trình; nhìn một chương trình Java hay công thức toán học mà không có ngữ cảnh thì cũng sẽ không hiểu tương tự. Tiêu chí nên là sau khi học kiến thức cơ bản và làm vài tutorial, người ta có thể hiểu được đến mức nào
• Nội dung này lúc đầu giống như một màn nhại, nhưng dần phát triển thành một lời giải nghiêm túc và thanh lịch; đến cuối thì tôi cũng muốn thật sự thử chơi “trò chơi” này
  • Bình luận rằng thực ra cũng chơi được, nhưng phần kết ở đoạn cuối khó hơn nhiều
• Chia sẻ trải nghiệm thực tế nộp giấy tờ liên quan đến hộ chiếu Anh tại Nhật; tùy tình huống mà giấy tờ cần nộp có thể khác nhau, và người này phải chuẩn bị rất nhiều tài liệu như giấy khai sinh của bản thân và con, bản gốc sổ hộ khẩu gia đình Nhật, bản dịch, giấy chứng nhận đã tiếp nhận khai sinh, v.v. Mỗi trang đều phải photo màu, thậm chí còn bị yêu cầu cả bản sao hộ chiếu của người khác. Quy trình rất mơ hồ, và về bản chất là cứ phải tiếp tục nộp giấy tờ cho đến khi họ thấy đã đủ
  • Giải thích rằng cha của người bình luận sinh ở Anh, nhưng ông nội lại sinh ở nước ngoài nên tình huống trở nên phức tạp hơn
  • Ở Nhật thì không bị yêu cầu giấy khai sinh của bố mẹ. Người này mang quốc tịch Hungary và Anh, đang sống ở Hungary, nhưng bị yêu cầu giấy khai sinh của cả hai bên cha mẹ và bốn ông bà. Vì vợ và họ hàng không thân thiết nên đã đính kèm thư giải trình và được chấp nhận; dù trong quốc tịch của mình, quốc tịch/xuất thân bên mẹ thực chất gần như không quan trọng. Cũng có chia sẻ rằng đã phải nhờ một người bạn của gia đình làm luật sư kiểm tra online giúp
  • Thắc mắc vì sao phải nộp bản photo màu tất cả các trang trong hộ chiếu Nhật của đứa trẻ
• Việc xin hộ chiếu Anh có thể làm hoàn toàn online, và ngay cả đơn xin mới cho công dân mới (nhận nuôi, nhập tịch, huyết thống) cũng có thể thực hiện chỉ bằng thiết bị di động, kể cả chụp ảnh mà không cần ứng dụng riêng. Theo trải nghiệm của người bình luận, đây là một quy trình hiệu quả, nhanh và trực quan
  • Có người đánh giá hệ thống gia hạn hộ chiếu online gần đây là website tốt nhất họ từng dùng trong nhiều năm; chạy hoàn hảo cả trên máy tính cũ và trình duyệt cũ, UI rất đơn giản và dễ tiếp cận với mọi người, điều hướng từng bước rất thân thiện. Mong kiểu thiết kế này được áp dụng rộng hơn trong lĩnh vực kinh doanh; khen ngợi HMPO
  • Có người lần đầu dùng hệ thống online gần đây và nhận hộ chiếu rất nhanh chỉ trong 2 tuần ngay cả khi đang ở California, Mỹ. Trải nghiệm gia hạn hộ chiếu Canada thì mất tới 4 tháng, thủ tục rắc rối và cần nhiều giấy tờ. Hy vọng chương trình thí điểm gia hạn số bằng smartphone sẽ được mở rộng
• Chia sẻ rằng khi chuẩn bị hộ chiếu cho con gái ở Nhật đã rất vất vả vì các vấn đề như họ của cha mẹ trên giấy khai sinh không khớp. Cuối cùng đã thuyết phục được rằng vì mình sinh ở Anh và có quốc tịch Anh (hộ chiếu), nên con ruột cũng có thể kế thừa điều đó. Dù không khớp với bộ giấy tờ tiêu chuẩn yêu cầu, nhưng vẫn được xem là trường hợp đỡ vất vả hơn
• Kể lại trải nghiệm như từng chơi hộ chiếu ứng dụng “Passport Application” ngoài đời; quy tắc “mutable history” rất thú vị. Có những trường hợp thông tin thực tế của một giấy tờ có thể thay đổi chỉ trong thời gian ngắn, nên ngay cả tài liệu đã scan rồi cũng phải nộp và scan lại. Có câu đùa rằng quá trình này cho thấy các quan chức xét duyệt đang ngầm công nhận sự tồn tại của đa vũ trụ multiverse. Việc giao tiếp giữa các tư vấn viên và nhân viên xử lý đóng vai trò “NPC” mang cảm giác như cầu nguyện một chiều, không truyền đạt được mấy. Có suy đoán OP là fan của trò Mornington Crescent, vì quy tắc của nó giống với việc xin hộ chiếu
  • Trong hệ thống Anh, người ta có thể đổi tên khá tự do, đến mức ngay cả mẹ tôi cũng có thể đăng ký khai sinh cho tôi bằng họ của cuộc hôn nhân thứ ba của bà. Giấy khai sinh cũng chỉ có một số mục là bất biến, nên không phải hoàn toàn cố định. Văn phòng hộ chiếu đôi khi còn quên cả lịch sử trước đó, nên việc họ của tôi trên hộ chiếu không khớp đã từng được giải thích rồi mà sau này vẫn lại thành vấn đề. Mỗi lần gọi điện, gửi email hay gửi câu hỏi cho các tư vấn viên “NPC” thì chỉ nhận được các câu trả lời khác nhau. Nó thiếu nhất quán như GPT vậy. Thậm chí cùng một bộ giấy tờ, một cô con gái thì bị yêu cầu bổ sung, còn cô kia lại được cấp không vấn đề gì; cuối cùng mẹ tôi phải khiếu nại với nghị sĩ quốc hội thì chỉ một ngày sau là xong
• Chia sẻ trải nghiệm đã từng chơi “game” Passport Application vài năm trước. Người này sinh ở Anh, có cha là người Anh, nhưng vì cha mẹ không kết hôn và bản thân sinh sau năm 1983 nhưng trước khi quy định năm 2006 được sửa, nên ban đầu không phải công dân. Khoảng những năm 2010, luật năm 2006 được áp dụng hồi tố nên mới được công nhận là công dân. “Nhiệm vụ” chính là phải nộp bản gốc giấy khai sinh của cha, và đến cuối còn bị bắt buộc tham dự cả “lễ tuyên thệ trung thành với Nữ hoàng”, nghe rất kỳ quặc
  • Ít nhất thì cũng có phần credit cuối phim, như một câu đùa