< Terug naar vorige pagina
Publicatie
Type invariants for Haskell
Boekbijdrage - Boekhoofdstuk Conferentiebijdrage
Multi-parameter type classes, functional dependencies, and recently GADTs
and open type families open up opportunities to use complex type-level
programming to let GHC's type checker verify various properties of your
programs. But type-level code is special in that its correctness is crucial
to the safety of the program; so except in those cases simple enough for the
type checker to see trivially that the code is correct (or harmless),
type-level programs need to come with a specification of their properties
together with their proof.
In this article, we propose an extension to Haskell that allows the
specification of invariants for type classes and open type families,
together with accompanying evidence that those invariants hold.
To accommodate the open nature of type classes and type families, the
evidence itself needs to be open and every subcase of the proof can be
provided independently from the others.
Boek: Proceedings of the 3rd workshop on Programming languages meets program verification
Pagina's: 39 - 48
ISBN:9781605583303
Jaar van publicatie:2009
Toegankelijkheid:Open