2 คะแนน โดย GN⁺ 2024-11-02 | 1 ความคิดเห็น | แชร์ทาง WhatsApp

Hazel

  • Hazel เป็นสภาพแวดล้อมการเขียนโปรแกรมเชิงฟังก์ชันแบบสดที่สามารถตรวจสอบชนิด จัดการ และรันโปรแกรมที่ยังไม่สมบูรณ์ซึ่งมี type holes ได้
  • ไม่มีสถานะของตัวแก้ไขที่ไร้ความหมาย

แรงจูงใจ

  • ระหว่างการเขียนโปรแกรม เรามักใช้เวลามากกับการทำงานกับข้อความโปรแกรมที่ยังไม่สมบูรณ์ในเชิงรูปแบบ เช่น ช่องว่าง ข้อผิดพลาดของชนิด หรือความขัดแย้งจากการรวมโค้ด
  • นิยามของภาษาโปรแกรมแบบเดิมไม่ได้มอบความหมายอย่างเป็นทางการให้กับโครงสร้างเหล่านี้
  • โปรแกรมแก้ไขโค้ดและเครื่องมือต่าง ๆ จึงต้องพึ่งพาวิธีแก้ชั่วคราวที่ซับซ้อน
  • Hazel สร้างแบบจำลองโปรแกรมที่ไม่สมบูรณ์บนพื้นฐานของทฤษฎีชนิด

คุณลักษณะของ Hazel

  • เป็นภาษาโปรแกรมเชิงฟังก์ชันที่คล้ายกับ Elm/ML และถูกพัฒนาเป็นสภาพแวดล้อมบนเว็บ
  • แม้เป็นโปรแกรมที่ไม่สมบูรณ์ก็ยังมีนิยามที่ชัดเจนทั้งแบบสถิตและแบบไดนามิก
  • สามารถใช้เป็นแพลตฟอร์มเพื่อการวิจัยและการศึกษาได้

ข่าวและสิ่งพิมพ์

  • มกราคม 2025: บทความ Grove ได้รับการตอบรับแบบมีเงื่อนไขที่ POPL 2025
  • ตุลาคม 2024: นำเสนองานวิจัยที่ผสาน large language models กับ type holes ที่ OOPSLA 2024
  • ตุลาคม 2024: มีกำหนดปาฐกถาพิเศษของ Cyrus ที่ HATRA 2024
  • กันยายน 2024: ได้รับทุนวิจัยจาก NSF เพื่อพัฒนาเครื่องมือ proof assistant สำหรับการเรียนการสอน
  • มกราคม 2024: นำเสนอบทความเกี่ยวกับการระบุตำแหน่งข้อผิดพลาดและการกู้คืนที่ POPL 2024
  • ตุลาคม 2023: นำเสนองานวิจัยเกี่ยวกับ pattern matching ที่ OOPSLA 2023
  • มกราคม 2023: ได้รับรางวัล NSF CAREER

ทีม Hazel

  • Hazel เป็นโครงการวิจัยโอเพนซอร์สที่นำโดย Future of Programming Lab แห่งมหาวิทยาลัยมิชิแกน
  • หากมีคำถามหรือสนใจร่วมพัฒนา สามารถติดต่อ Cyrus Omar หัวหน้าทีมได้

สรุปโดย GN⁺

  • Hazel นำเสนอแนวทางใหม่ในการจัดการกับโปรแกรมที่ไม่สมบูรณ์ และเป็นแพลตฟอร์มที่มีประโยชน์สำหรับการศึกษาการเขียนโปรแกรมและการวิจัย
  • ด้วยการอิงกับทฤษฎีชนิด จึงทำให้แม้แต่โปรแกรมที่ไม่สมบูรณ์ก็สามารถรันได้ ช่วยสนับสนุนการสำรวจอนาคตของการเขียนโปรแกรม
  • โครงการที่มีฟังก์ชันคล้ายกัน ได้แก่ Elm, ML และเครื่องมือเพื่อการศึกษาด้านการเขียนโปรแกรมอีกหลากหลายชนิด

1 ความคิดเห็น

 
GN⁺ 2024-11-02
ความคิดเห็นใน Hacker News
  • หนึ่งในจุดเด่นของ Eclipse คือความสามารถในการรันโค้ดที่ยังไม่สมบูรณ์หรือเสียอยู่ได้ เพราะ Eclipse Compiler ของ Java สามารถสร้างไบต์โค้ดสำหรับไฟล์แทบทุกไฟล์ได้ ฟีเจอร์นี้มอบสภาพแวดล้อมที่ช่วยเพิ่มประสิทธิภาพอย่างมาก และน่าเสียดายที่ยังไม่ได้ถูกนำไปใช้ในระบบขนาดใหญ่อื่น ๆ

  • Haskell มี type hole และมีปลั๊กอินที่ให้ code action สำหรับเติมให้สมบูรณ์หรือแยกเคสได้ Agda ก็มี type hole เช่นกัน และให้ความสามารถที่ทรงพลังยิ่งกว่า

  • พร้อมตอบคำถามเกี่ยวกับ Hazel และได้ทำงานกับ Hazel มาในฐานะนักศึกษาปริญญาเอกของ Cyrus ตลอด 4 ปีที่ผ่านมา ตอนนี้กำลังพัฒนาอินเทอร์เฟซแบบ projectional ที่ปรับเปลี่ยนได้สำหรับ live programming ใน Hazel

    • รายการฟีเจอร์ที่เพิ่มเข้าไปใน Hazel: ลิงก์ GitHub
    • วิดีโอบรรยายเกี่ยวกับการใช้ type hole และ Hazel language server เพื่อให้บริบทของโค้ดสำหรับ LLM code completion: ลิงก์ YouTube
  • Hazel เป็นสภาพแวดล้อมการเขียนโปรแกรมเชิงฟังก์ชันแบบ live ที่มี type hole เป็นจุดเด่น ข้อมูลที่เกี่ยวข้อง: ลิงก์ Hacker News

  • Tylr เป็นเดโมของการแก้ไขแบบ tile-based ซึ่งเป็นแนวทางใหม่ของ structure editing ข้อมูลที่เกี่ยวข้อง: ลิงก์ Hacker News

  • ชอบตัวอย่างโค้ดของ Hazel และชอบทั้ง live editor กับเอกสารประกอบที่แสดงทางด้านขวา แต่ก็สงสัยว่ามันให้ความสามารถมากกว่า live editor และ type checker หรือไม่ และสามารถใช้เขียนโปรแกรมจริงได้หรือเปล่า

  • UI ของเอดิเตอร์สวยงามมาก และทำงานบนมือถือได้ดีด้วย น่าประทับใจมาก

  • ไวยากรณ์ที่ให้ "let" binding ลงท้ายด้วย "in" น่าสนใจมาก ตัวอย่าง:

    let comparison =
     (0 == 0, 0 < 1, 1 <= 1, 2 > 1, 1 >= 1) 
    in
    

    มีใครรู้ไหมว่าทำไมถึงใช้คีย์เวิร์ด "in"

  • แม้จะไม่มีการพูดถึง Idris แต่ครั้งแรกที่เคยเห็นสไตล์การพัฒนาแบบนี้ก็คือใน Idris วิดีโอที่เกี่ยวข้อง: ลิงก์ YouTube

  • ลองใช้ playground บนโทรศัพท์ Android แล้ว แต่การกดแป้นพิมพ์ไม่สะท้อนเข้าไปในซอร์สโค้ด แตะเพื่อวางเคอร์เซอร์ได้และคีย์บอร์ดเสมือนก็แสดงขึ้นมา แต่พิมพ์อะไรไม่ได้ ไม่แน่ใจว่านี่เป็นบั๊กหรือปัญหาด้าน UX

  • ชอบ Hazel มาตลอด และคิดว่าน่าจะเป็นเครื่องมือที่ยอดเยี่ยมสำหรับการศึกษา อยากรู้ว่ามีอะไรถูกสร้างขึ้นด้วย Hazel แล้วบ้าง