- Hazel là một môi trường lập trình hàm live trên web, đặt typed holes làm trung tâm, cho phép kiểm tra kiểu, thao tác và chạy cả những chương trình chưa hoàn thiện
- Điểm cốt lõi là mô hình hóa các trạng thái chưa hoàn chỉnh như chỗ trống, lỗi kiểu và xung đột merge thành holes, qua đó giảm những đoạn mà editor đánh mất ngữ nghĩa
- Các chương trình chưa hoàn chỉnh có thể tạo trong Hazel được định nghĩa cả tĩnh lẫn động, và có thể có kiểu chưa hoàn chỉnh cũng như kết quả thực thi chưa hoàn chỉnh
- Đối tượng triển khai là ngôn ngữ hàm thuộc họ Elm/ML, và được dùng làm nền tảng cho giáo dục lập trình, biên tập cộng tác, học chứng minh và nghiên cứu hoàn thành mã bằng AI
- Đây là dự án nghiên cứu mã nguồn mở do Future of Programming Lab của University of Michigan dẫn dắt; bản build web để trải nghiệm và mã nguồn trên GitHub đã được công khai
Ý tưởng cốt lõi của Hazel
- Hazel là một môi trường lập trình hàm live, được xây dựng xoay quanh typed holes
- Ngay cả chương trình chưa hoàn thiện cũng có thể tiếp tục các thao tác sau
- Kiểm tra kiểu
- Thao tác
- Thực thi
- Mục tiêu là tạo ra một môi trường vẫn duy trì phản hồi có ý nghĩa ngay cả khi mã đang được chỉnh sửa ở trạng thái bị hỏng
Cách xử lý chương trình chưa hoàn chỉnh
- Trong quá trình lập trình thông thường, văn bản chương trình thường xuyên rơi vào trạng thái chưa hoàn chỉnh về mặt hình thức
- Chỗ trống
- Lỗi kiểu
- Xung đột merge
- Các định nghĩa ngôn ngữ lập trình hiện có không gán ngữ nghĩa hình thức cho những cấu trúc này, nên ngay cả hành vi của phần mã đã hoàn chỉnh cũng khó được xử lý dưới dạng phản hồi live
- Editor và công cụ buộc phải dựa vào các heuristic phức tạp để cung cấp liền mạch hoàn thành mã, kiểm tra kiểu và điều hướng mã
- Hazel mô hình hóa chương trình chưa hoàn chỉnh thành chương trình có holes
- Hole biểu thị phần chương trình còn thiếu
- Nó hoạt động như một lớp màng bao lấy phần có lỗi hoặc phần xung đột trong môi trường cộng tác
- Cách tiếp cận này dựa trên lý thuyết kiểu modal theo ngữ cảnh và lý thuyết kiểu dần dần
Môi trường Hazel và mô hình thực thi
- Hazel đang được triển khai như một môi trường lập trình trên web cho ngôn ngữ hàm tương tự Elm/ML
- Mọi chương trình chưa hoàn chỉnh có thể tạo ra bằng ngôn ngữ thao tác chỉnh sửa của Hazel đều được định nghĩa cả tĩnh lẫn động
- Có thể có kiểu chưa hoàn chỉnh
- Khi thực thi, có thể tạo ra kết quả chưa hoàn chỉnh
- Nhờ đặc tính này, Hazel được dùng làm nền tảng cho nghiên cứu về môi trường lập trình tương lai và giáo dục lập trình
Tầm nhìn nghiên cứu và tài liệu liên quan
- Toward Semantic Foundations for Program Editors: tầm nhìn nghiên cứu về nền tảng ngữ nghĩa cho program editor
- Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine: tầm nhìn về môi trường tính toán live, có thể tổ hợp và cộng tác cho khoa học tính toán quy mô lớn
- Các bài trình bày liên quan đến Hazel được tập hợp trong YouTube playlist of Hazel-related talks
- Có thể xem demo gần đây trong bài trình bày tại Topos Institute
Nghiên cứu gần đây và dòng xuất bản
- Năm 2025, nhiều nghiên cứu xoay quanh Hazel được trình bày tại các hội nghị
- Incremental Bidirectional Typing via Order Maintenance: nghiên cứu biến kiểm tra kiểu hai chiều thành dạng tăng dần bằng cách mượn kỹ thuật từ hệ thống layout của trình duyệt; nhận OOPSLA 2025 Distinguished Paper Award
- Syntactic Completions with Material Obligations: lý thuyết và triển khai sửa lỗi cú pháp bằng cách tận dụng các nghĩa vụ được cụ thể hóa trực quan trong hệ thống Tylr
- A FAIR Case for a Live Computational Commons: đề xuất tái cấu trúc công việc khoa học xoay quanh môi trường lập trình live quy mô lớn
- Decomposable Type Highlighting for Bidirectional Type and Cast Systems: nghiên cứu UI để debug lỗi kiểu tĩnh và động trong Hazel
- Hazel Deriver: A Live Editor for Constructing Rule-Based Derivations: công cụ giáo dục để xây dựng quá trình suy dẫn theo phong cách diễn dịch tự nhiên
- Năm 2024, phục hồi lỗi kiểu, kết hợp LLM, học chứng minh và môi trường tính toán cho khoa học khí hậu tiếp tục là các chủ đề chính
- Total Type Error Localization and Recovery with Holes xử lý việc định vị và phục hồi lỗi trong chương trình bị gán kiểu sai, và nhận POPL 2024 Distinguished Paper Award
- Statically Contextualizing Large Language Models with Typed Holes là công trình kết hợp language server với mô hình ngôn ngữ lớn để cải thiện đáng kể hiệu năng hoàn thành mã bằng AI
- NSF tài trợ cho một đề tài nghiên cứu nhằm chuyển Hazel thành công cụ trợ giúp chứng minh dùng trong lớp học
- Các nghiên cứu từ 2017 đến 2023 đã phát triển từng bước nền tảng tính toán, chỉnh sửa có cấu trúc, đánh giá live và chức năng hỗ trợ giáo dục của Hazel
- Hazelnut: A Bidirectionally Typed Structure Editor Calculus định nghĩa phép tính cho thao tác chỉnh sửa tự động chèn typed holes
- Live Functional Programming with Typed Holes phát triển ngữ nghĩa vận hành phong phú cho biểu thức có typed holes
- Program Sketching with Live Bidirectional Evaluation nói về Smyth, thành phần nền tảng của Hazel Assistant
- Live Pattern Matching with Typed Holes xử lý suy luận chương trình có pattern holes và nhận OOPSLA 2023 Distinguished Paper Award
Sử dụng và đóng góp
- Hazel cung cấp bản build web để có thể trải nghiệm trực tiếp
- Mã nguồn được công khai trên GitHub
- Hazel là dự án nghiên cứu mã nguồn mở do Future of Programming Lab (FP Lab) của University of Michigan dẫn dắt
- Nếu muốn đóng góp hoặc có câu hỏi, có thể liên hệ trưởng nhóm Cyrus Omar
Chưa có bình luận nào.