Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

Fibrational induction meets effects

Atkey, Robert and Ghani, Neil and Jacobs, Bart and Johann, Patricia (2012) Fibrational induction meets effects. [Proceedings Paper]

[img]
Preview
PDF - Submitted Version
Download (240Kb) | Preview

    Abstract

    This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.

    Item type: Proceedings Paper
    ID code: 37131
    Keywords: fibrational induction, polynomial data types, Electronic computers. Computer science
    Subjects: Science > Mathematics > Electronic computers. Computer science
    Department: Faculty of Science > Computer and Information Sciences
    Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 26 Jan 2012 16:00
    Last modified: 27 Mar 2014 21:17
    URI: http://strathprints.strath.ac.uk/id/eprint/37131

    Actions (login required)

    View Item

    Fulltext Downloads: