CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Proving Type Class Laws for Haskell

Andreas Arvidsson (Institutionen för data- och informationsteknik (Chalmers)) ; Moa Johansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Robin Touche (Institutionen för data- och informationsteknik (Chalmers))

Type classes in Haskell are used to implement ad-hoc poly- morphism, i.e. a way to ensure both to the programmer and the compiler that a set of functions are defined for a specific data type. All instances of such type classes are expected to behave in a certain way and satisfy laws associated with the respective class. These are however typically just stated in comments and as such, there is no real way to enforce that they hold. In this paper we describe an extension to the inductive theorem prover HipSpec, which allows the user to write down type class laws which are then automatically instantiated and sent to the theorem prover when declaring a new instance of a type class.

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-12-15.
CPL Pubid: 246147