View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        Generic programming with ornaments and dependent types

        Thumbnail
        View/Open
        thesis_greyscale.pdf (437.9Kb)
        thesis_color.pdf (426.3Kb)
        Publication date
        2016
        Author
        Sijsling, Y.
        Metadata
        Show full item record
        Summary
        Modern dependently typed functional programming languages like Agda allow very specific restrictions to be built into datatypes by using indices and dependent types. Properly restricted types can help programmers to write correct-by-construction software. However, code duplication will occur because the language does not recognise that similarly-structured datatypes with slightly different program-specific restrictions can be related. Some functions will be copy-pasted for lists, vectors, sorted lists and bounded lists. Ornaments specify the exact relation between of different datatypes and may be a path towards a solution. It is a first step in structuring the design space of datatypes in dependently typed languages. Literature has shown how ornaments can produce conversion functions between types, and how they can help to recover code reuse by transporting functions across ornaments. This thesis presents an Agda library for experimentation with ornaments. We have implemented a generic programming framework where datatypes are represented as descriptions. A description can be generated from a real datatype and patched with an ornament to create new description, which in turn can be converted back to a new datatype. Our descriptions are carefully designed to always be convertible to actual datatypes, resulting in an unconventional design. They pass along a context internally to support dependent types and they can be used with multiple parameters and multiple indices.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/23661
        Collections
        • Theses
        Utrecht university logo