A pattern for almost compositional functions

2008 ◽  
Vol 18 (5-6) ◽  
pp. 567-598 ◽  
Author(s):  
BJÖRN BRINGERT ◽  
AARNE RANTA

AbstractThis paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here “almost compositional” means that for all of the constructors in the type(s), except a limited number of them, the result of the function depends only on the constructor and the results of calling the function on the constructor's arguments. The pattern consists of a generic part constructed once for each data type or family of data types, and a task-specific part. The generic part contains the code for the predictable compositional cases, leaving the interesting work to the task-specific part. Examples of the pattern are given, implemented in dependent type theory with inductive families, in Haskell with generalized algebraic data types and rank-2 polymorphism, and in Java using a variant of the Visitor design pattern. The relationships to the “Scrap Your Boilerplate” approach to generic programming, and to general tree types in dependent type theory, are investigated by reimplementing our operations using those frameworks.

2014 ◽  
Vol 49 (1) ◽  
pp. 503-515 ◽  
Author(s):  
Robert Atkey ◽  
Neil Ghani ◽  
Patricia Johann

2019 ◽  
Vol 3 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Daniel Gratzer ◽  
Jonathan Sterling ◽  
Lars Birkedal

Author(s):  
Aleš Bizjak ◽  
Hans Bugge Grathwohl ◽  
Ranald Clouston ◽  
Rasmus E. Møgelberg ◽  
Lars Birkedal

2017 ◽  
Vol 1 (ICFP) ◽  
pp. 1-29 ◽  
Author(s):  
Andreas Nuyts ◽  
Andrea Vezzosi ◽  
Dominique Devriese

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.


2015 ◽  
Vol 25 (5) ◽  
pp. 1010-1039 ◽  
Author(s):  
BENEDIKT AHRENS ◽  
KRZYSZTOF KAPULKIN ◽  
MICHAEL SHULMAN

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.


10.29007/vm4p ◽  
2018 ◽  
Author(s):  
Giuseppe Primiero

In the present paper we explore the use of a newly formulated polymorphic modal type theory for a computational interpretation of programs in the context of distributed processing. The initial language define judgemental modalities with a the standard constructor for necessity interpreted as the presentation of instructions for a program terminating at runtime and an independent constructor for the possibility judgement as a representation of a process of partial evaluation. In order to interpret distributed and localised computing, we propose an extension in terms of multi-modalities, to express programs equipped with locations and data accessibility. Besides localised accessibility formalised by the different signed modalities, we develop further the language by prioritising these modalities, which implement seriality or staging annotations in the program structure.


Sign in / Sign up

Export Citation Format

Share Document