Hazel
- Hazel là một môi trường lập trình hàm trực tiếp cho phép kiểm tra kiểu, thao tác và thực thi các chương trình chưa hoàn chỉnh có chứa type hole
- Không tồn tại trạng thái trình soạn thảo vô nghĩa
Động lực
- Khi lập trình, chúng ta dành nhiều thời gian làm việc với văn bản chương trình chưa hoàn chỉnh về mặt hình thức do chỗ trống, lỗi kiểu, xung đột hợp nhất, v.v.
- Các định nghĩa ngôn ngữ lập trình hiện có không gán ý nghĩa hình thức chính thức cho những cấu trúc như vậy
- Trình soạn thảo chương trình và các công cụ phải dựa vào những giải pháp tạm thời phức tạp
- Hazel mô hình hóa các chương trình chưa hoàn chỉnh dựa trên lý thuyết kiểu
Đặc điểm của Hazel
- Là một ngôn ngữ lập trình hàm tương tự Elm/ML, được triển khai trong môi trường web
- Ngay cả các chương trình chưa hoàn chỉnh cũng được xác định rõ ràng cả về tĩnh và động
- Có thể được sử dụng như một nền tảng nghiên cứu và giáo dục
Tin tức và ấn phẩm
- Tháng 1 năm 2025: Bài báo Grove được chấp thuận có điều kiện tại POPL 2025
- Tháng 10 năm 2024: Công bố nghiên cứu kết hợp mô hình ngôn ngữ lớn và type hole tại OOPSLA 2024
- Tháng 10 năm 2024: Cyrus dự kiến có bài phát biểu khai mạc tại HATRA 2024
- Tháng 9 năm 2024: Nhận tài trợ nghiên cứu từ NSF để phát triển công cụ hỗ trợ chứng minh dùng trong giảng dạy
- Tháng 1 năm 2024: Công bố bài báo về định vị lỗi và phục hồi tại POPL 2024
- Tháng 10 năm 2023: Công bố nghiên cứu về pattern matching tại OOPSLA 2023
- Tháng 1 năm 2023: Nhận giải NSF CAREER
Nhóm Hazel
- Hazel là một dự án nghiên cứu mã nguồn mở do Future of Programming Lab tại Đại học Michigan dẫn dắt
- Nếu bạn có câu hỏi hoặc muốn đóng góp, có thể liên hệ trưởng nhóm Cyrus Omar
Tóm tắt của GN⁺
- Hazel đề xuất một cách tiếp cận mới để xử lý các chương trình chưa hoàn chỉnh và là một nền tảng hữu ích cho giáo dục và nghiên cứu lập trình
- Bằng việc dựa trên lý thuyết kiểu để khiến cả các chương trình chưa hoàn chỉnh cũng có thể thực thi, Hazel góp phần khám phá tương lai của lập trình
- Các dự án có chức năng tương tự gồm Elm, ML và nhiều công cụ giáo dục lập trình khác
1 bình luận
Ý kiến trên Hacker News
Một trong những đặc điểm của Eclipse là khả năng chạy cả mã chưa hoàn chỉnh hoặc bị hỏng. Điều này có được vì Eclipse Compiler của Java có thể tạo bytecode cho gần như mọi tệp. Đây là một môi trường rất hiệu quả, và thật đáng tiếc khi tính năng này không được triển khai trong các hệ thống lớn khác.
Haskell có type hole, và có plugin cung cấp các code action để hoàn thiện chúng hoặc tách case. Agda cũng có type hole và cung cấp các tính năng mạnh hơn.
Tôi sẵn sàng trả lời câu hỏi về Hazel, và đã làm việc với Hazel trong 4 năm qua với vai trò nghiên cứu sinh tiến sĩ của Cyrus. Hiện tôi đang phát triển một giao diện projectional có thể uốn nắn cho lập trình trực tiếp trong Hazel.
Hazel là một môi trường lập trình hàm trực tiếp với đặc trưng là type hole. Thông tin liên quan: liên kết Hacker News
Tylr là bản demo của biên tập dựa trên tile, một cách tiếp cận mới cho chỉnh sửa có cấu trúc. Thông tin liên quan: liên kết Hacker News
Tôi thích các ví dụ mã của Hazel, và thích trình biên tập trực tiếp cùng phần tài liệu xuất hiện bên phải. Nhưng tôi thắc mắc liệu nó có cung cấp nhiều hơn một trình biên tập trực tiếp và bộ kiểm tra kiểu hay không, và liệu có thể thực sự viết chương trình bằng nó không.
UI của trình biên tập rất đẹp và cũng hoạt động tốt trên di động. Rất ấn tượng.
Cú pháp
letbinding kết thúc bằnginkhá thú vị. Ví dụ:Có ai biết lý do của từ khóa
inkhông?Không thấy nhắc đến Idris, nhưng nơi đầu tiên tôi thấy kiểu phát triển này là ở Idris. Video liên quan: liên kết YouTube
Tôi đã thử playground trên điện thoại Android, nhưng thao tác gõ không được phản ánh vào mã nguồn. Tôi có thể chạm để đặt con trỏ và bàn phím ảo xuất hiện, nhưng không thể nhập được. Không rõ đây là bug hay là vấn đề UX.
Tôi luôn thích Hazel, và có lẽ đây sẽ là một công cụ tuyệt vời cho giáo dục. Tôi tò mò không biết đã có gì được xây dựng bằng Hazel.