一句话:通过研究揭示 LiquidHaskell 开发者面临的九类可用性障碍,为液体类型系统设计提供依据。
液体类型(liquid types)能够表达比简单类型系统更丰富的验证性质,但至今仍未获得广泛采用。为理解其中原因,本文对开发者使用液体类型时所遇挑战进行了研究,重点关注 LiquidHaskell。研究识别出九项关键障碍,可归为三类:开发者体验、面对复杂与大型代码库时的可扩展性挑战,以及对验证过程的理解困难。这些发现综合呈现了阻碍液体类型更广泛采用的可用性问题,并为当前及未来液体类型系统的设计与实现提供启示。
Liquid types can express richer verification properties than simple type systems. However, despite their advantages, liquid types have yet to achieve widespread adoption. To understand why, we conducted a study analyzing developers’ challenges with liquid types, focusing on LiquidHaskell. Our findings reveal nine key barriers that span three categories, including developer experience, scalability challenges with complex and large codebases, and understanding the verification process. Together, these obstacles provide a comprehensive view of the usability challenges to the broader adoption of liquid types and offer insights that can inform the current and future design and implementation of liquid type systems.
@article{paperbot3145,
title = {Usability Barriers for Liquid Types},
author = {Catarina Gamboa and Abigail Reese and Alcides Fonseca and Jonathan Aldrich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729327}
}