一句话:提出无需嵌入-投影对的机械化单态化,将多态函数用于自动属性测试,并揭示合适类型计算为对数。
随机属性测试近年来备受关注,但多数框架只支持单态属性,对多态属性止步不前。Bernardy 等人曾提出理论将广泛的多态属性归约到单态属性,但依赖 ad-hoc 的嵌入-投影对(embedding-projection pairs)将类型调整成特定形式。本文跳过嵌入-投影对,为一般类多态函数提出一种机械化单态化方法,从而向多态属性的自动测试迈进一步。作者发现,为单态化计算合适类型的过程可归结为对数运算。这一结果简化了多态属性测试的自动化路径,并揭示了类型计算与对数之间的深刻联系。
Randomized property-based testing has gained much attention recently, but most frameworks stop short at polymorphic properties. Although Bernardy et al. have developed a theory to reduce a wide range of polymorphic properties to monomorphic ones, it relies upon ad-hoc embedding-projection pairs to massage the types into a particular form. This paper skips the embedding-projection pairs and presents a mechanical monomorphization for a general class of polymorphic functions, a step towards automatic testing for polymorphic properties. The calculation of suitable types for monomorphization turns out to be logarithm .