Datatype Laws Without Signatures
Fokkinga, Maarten M. (1996) Datatype Laws Without Signatures. Mathematical Structures in Computer Science, 6 (1). pp. 132. ISSN 09601295

PDF
262kB 
Abstract:  Using the wellknown categorical notion of `functor' one may define the concept of datatype (algebra) without being forced to introduce a signature, that is, names and typings for the individual sorts (types) and operations involved. This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra. The categorical notion of `transformer' developed in this paper allows the same approach to laws: without using signatures one can define the concept of law for datatypes (lawful algebras), and investigate the equational specification of datatypes in a syntaxfree way. A transformer is a special kind of functor and also a natural transformation on the level of dialgebras. Transformers are quite expressive, satisfy several closure properties, and are related to naturality and Wadler's Theorems For Free. In fact, any colimit is an initial lawful algebra. 
Item Type:  Article 
Additional information:  Imported from EWI/DB PMS [dbutwente:arti:0000003409] 
Copyright:  © 1996 Cambridge University Press 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Research Group:  
Link to this item:  http://purl.utwente.nl/publications/66234 
Official URL:  http://dx.doi.org/10.1017/S0960129500000852 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page
Metis ID: 118493