Translating Type Class Laws from Agda2hs to QuickCheck
G. Grandi (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
N. Burke – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Panichella – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This research aims to explore using property based testing to find counterexamples for proving statements about programs in Agda2hs. I have created an extension to Agda2hs to translate type class laws into QuickCheck properties and evaluated on real-world Haskell code to evaluate its effectiveness. I found that having relatively cheap to run tests compared to formalizing helped save time ensuring definitions were correct before formalizing statements.