Type-Driven Development để lập trình an toàn bằng cách tận dụng kiểu

• Kiểu là một hợp đồng nghiêm ngặt mà hàm và dữ liệu phải tuân thủ
• Kiểu là tập hợp mà một giá trị có thể thuộc về
• Kiểu có thể được biến đổi thông qua hàm, và nhờ đó phạm vi có thể thay đổi
  • Hàm đơn ánh - chuyển đổi từ kiểu có phạm vi nhỏ sang kiểu có phạm vi lớn
  • Hàm toàn ánh - chuyển đổi từ kiểu có phạm vi lớn sang kiểu có phạm vi nhỏ
  • Hàm song ánh - tương ứng một-một
• Có thể biểu diễn đầu vào và đầu ra của logic bằng kiểu
  • Điều này có nghĩa là có thể trừu tượng hóa logic thông qua kiểu
  • Có thể biểu diễn đầu vào và đầu ra bằng kiểu, rồi từ đó thiết kế logic
• Có thể đặt tên cho kiểu dữ liệu cơ bản để phân biệt thành các kiểu khác nhau
• Có thể giải quyết nhiều vấn đề bằng cách tận dụng hệ thống kiểu
  • Khái quát hóa bằng generic
  • Giới hạn phạm vi bằng phantom type
  • Giới hạn hành vi bằng union type (hoặc sum type)
  • Xử lý TODO bằng minimal type
  • Triển khai máy trạng thái hữu hạn bằng kiểu
  • Xác thực bằng dependent type
• Type-driven development là phương pháp luận định nghĩa kiểu trước, rồi viết mã dựa trên đó
• Type-driven development có thể được áp dụng ở bất cứ đâu nếu muốn, và bắt đầu bằng việc định nghĩa kết quả của từng bước dưới dạng kiểu
• Khi phân tích yêu cầu, hãy thử trừu tượng hóa chúng bằng kiểu
• Ngay cả khi cùng là một kiểu dữ liệu cơ bản, nếu ý nghĩa khác nhau thì nên định nghĩa thành các kiểu khác nhau để phân biệt
• Nếu đã phân tích yêu cầu và nghĩ về kiểu, hãy thử trừu tượng hóa logic bằng kiểu
  • Có thể trừu tượng hóa theo kiểu như (String) -> List<Token>
• Type-driven development rất phù hợp với test-driven development
  • Type-driven development và test-driven development giống nhau ở chỗ đều định nghĩa trước đầu vào và đầu ra rồi mới viết mã
  • Nếu type-driven development có thể dùng hệ thống kiểu để kiểm tra trước tính an toàn tại thời điểm biên dịch, thì test-driven development có thể dùng mã kiểm thử để bắt các lỗi hoặc tình huống ngoại lệ mà chỉ riêng kiểu không thể phát hiện
• Từ góc nhìn của người thiết kế, việc tận dụng hệ thống kiểu cũng giống như tạo ra các quy tắc mã dành cho các lập trình viên khác
• Tuy nhiên, nếu định nghĩa kiểu quá chi tiết khiến số lượng kiểu tăng quá nhiều hoặc việc định nghĩa kiểu trở nên quá phức tạp, thì ngược lại có thể làm cho việc viết mã khó hơn hoặc làm giảm tính dễ đọc, vì vậy điều quan trọng là luôn duy trì ở mức độ phù hợp

[chabulhwi]

> Hàm đơn ánh là trường hợp tập hợp các giá trị được ánh xạ có đối miền và ảnh không trùng nhau. Nói đơn giản hơn một chút, đó là việc chuyển đổi từ kiểu có phạm vi nhỏ sang kiểu có phạm vi lớn.

Hàm đơn ánh là hàm mà ảnh của hai biến bất kỳ khác nhau thì cũng khác nhau. Tức là, với mọi phần tử a và b thuộc miền xác định X của hàm đơn ánh f, nếu a ≠ b thì f(a) ≠ f(b). Trong chương trình toán trung học phổ thông ở Hàn Quốc, đây là điều được gọi là 'hàm một-một'.

[kciter1]

Cảm ơn vì phần giải thích chi tiết. :) Hóa ra là tôi đã hiểu sai. Đây cũng là chỗ tôi đã được góp ý vài lần, nên tôi sẽ học thêm một chút rồi sắp xếp lại nội dung.