Container (type theory) (original) (raw)
In type theory, containers are abstractions which permit various "collection types", such as lists and trees, to be represented in a uniform way. A (unary) container is defined by a type of shapes S and a type family of positions P, indexed by S. The extension of a container is a family of dependent pairs consisting of a shape (of type S) and a function from positions of that shape to the element type. Containers can be seen as canonical forms for collection types.
| Property | Value |
|---|---|
| dbo:abstract | In type theory, containers are abstractions which permit various "collection types", such as lists and trees, to be represented in a uniform way. A (unary) container is defined by a type of shapes S and a type family of positions P, indexed by S. The extension of a container is a family of dependent pairs consisting of a shape (of type S) and a function from positions of that shape to the element type. Containers can be seen as canonical forms for collection types. For lists, the shape type is the natural numbers (including zero). The corresponding position types are the types of natural numbers less than the shape, for each shape. For trees, the shape type is the type of trees of units (that is, trees with no information in them, just structure). The corresponding position types are isomorphic to the types of valid paths from the root to particular nodes on the shape, for each shape. Note that the natural numbers are isomorphic to lists of units. In general the shape type will always be isomorphic to the original non-generic container type family (list, tree etc.) applied to unit. One of the main motivations for introducing the notion of containers is to support generic programming in a dependently typed setting. (en) |
| dbo:wikiPageExternalLink | https://web.archive.org/web/20160428024201/http:/sneezy.cs.nott.ac.uk/containers/blog/ |
| dbo:wikiPageID | 19999420 (xsd:integer) |
| dbo:wikiPageLength | 3094 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 969896881 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Dependent_type dbr:Unary_operation dbr:Generic_programming dbr:Container_(abstract_data_type) dbr:Tree_(data_structure) dbr:Type_theory dbc:Type_theory dbr:Endofunctor dbr:Natural_number dbr:Canonical_form dbr:Polynomial_functor_(type_theory) dbr:List_(computing) |
| dbp:wikiPageUsesTemplate | dbt:Expand_section dbt:Reflist dbt:Type-theory-stub |
| dcterms:subject | dbc:Type_theory |
| gold:hypernym | dbr:Abstractions |
| rdfs:comment | In type theory, containers are abstractions which permit various "collection types", such as lists and trees, to be represented in a uniform way. A (unary) container is defined by a type of shapes S and a type family of positions P, indexed by S. The extension of a container is a family of dependent pairs consisting of a shape (of type S) and a function from positions of that shape to the element type. Containers can be seen as canonical forms for collection types. (en) |
| rdfs:label | Container (type theory) (en) |
| owl:sameAs | freebase:Container (type theory) wikidata:Container (type theory) https://global.dbpedia.org/id/4iNNS |
| prov:wasDerivedFrom | wikipedia-en:Container_(type_theory)?oldid=969896881&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Container_(type_theory) |
| is dbo:wikiPageDisambiguates of | dbr:Container_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Container_(Type_theory) dbr:Indexed_container dbr:Dependent_polynomial_functor |
| is dbo:wikiPageWikiLink of | dbr:Glossary_of_computer_science dbr:Combinatorial_species dbr:Collection_(abstract_data_type) dbr:PikeOS dbr:Container_(Type_theory) dbr:Container_(disambiguation) dbr:Thorsten_Altenkirch dbr:Indexed_container dbr:Dependent_polynomial_functor |
| is foaf:primaryTopic of | wikipedia-en:Container_(type_theory) |