| 1. |
- Abel, Andreas, 1974, et al.
(författare)
-
Interactive programming in Agda - Objects and graphical user interfaces
- 2017
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 27
-
Tidskriftsartikel (refereegranskat)abstract
- We develop a methodology for writing interactive and object-based programs (in the sense of Wegner) in dependently typed functional programming languages. The methodology is implemented in the ooAgda library. ooAgda provides a syntax similar to the one used in object-oriented programming languages, thanks to Agda's copattern matching facility. The library allows for the development of graphical user interfaces (GUIs), including the use of action listeners. Our notion of interactive programs is based on the IO monad defined by Hancock and Setzer, which is a coinductive data type. We use a sized coinductive type which allows us to write corecursive programs in a modular way. Objects are server-side interactive programs that respond to method calls by giving answers and changing their state. We introduce two kinds of objects: simple objects and IO objects. Methods in simple objects are pure, while method calls in IO objects allow for interactions before returning their result. Our approach also allows us to extend interfaces and objects by additional methods. We refine our approach to state-dependent interactive programs and objects through which we can avoid exceptions. For example, with a state-dependent stack object, we can statically disable the pop method for empty stacks. As an example, we develop the implementation of recursive functions using a safe stack. Using a coinductive notion of object bisimilarity, we verify basic correctness properties of stack objects and show the equivalence of different stack implementations. Finally, we give a proof of concept that our interaction model allows to write GUI programs in a natural way: we present a simple drawing program, and a program which allows the users to move a small spaceship using a button.
|
|
| 2. |
- Abel, Andreas, 1974, et al.
(författare)
-
Leibniz equality is isomorphic to Martin-Lof identity, parametrically
- 2020
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 30
-
Tidskriftsartikel (refereegranskat)abstract
- Consider two widely used definitions of equality. That of Leibniz: one value equals another if any predicate that holds of the first holds of the second. And that of Martin-Lof: the type identifying one value with another is occupied if the two values are identical. The former dates back several centuries, while the latter is widely used in proof systems such as Agda and Coq. Here we show that the two definitions are isomorphic: we can convert any proof of Leibniz equality to one of Martin-Lof identity andvice versa, and each conversion followed by the other is the identity. One direction of the isomorphism depends crucially on values of the type corresponding to Leibniz equality satisfying functional extensionality and Reynolds' notion of parametricity. The existence of the conversions is widely known (meaning that if one can prove one equality then one can prove the other), but that the two conversions form an isomorphism (internally) in the presence of parametricity and functional extensionality is, we believe, new. Our result is a special case of a more general relation that holds between inductive families and their Church encodings. Our proofs are given inside type theory, rather than meta-theoretically. Our paper is a literate Agda script.
|
|
| 3. |
- Abel, Andreas, 1974, et al.
(författare)
-
POPLMark reloaded: Mechanizing proofs by logical relations
- 2019
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 29
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks.
|
|
| 4. |
- Abel, Andreas, 1974, et al.
(författare)
-
Well-founded recursion with copatterns and sized types
- 2016
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 0956-7968 .- 1469-7653. ; 26
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper, we study strong normalization of a core language based on System F-omega which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non determinism and does not rely on coverage. Since System F-omega is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.
|
|
| 5. |
- Adams, Robin, 1978
(författare)
-
Pure type systems with judgemental equality
- 2006
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 16:2, s. 219-246
-
Tidskriftsartikel (refereegranskat)abstract
- In a typing system, there are two approaches that may be taken to the notion of equality. One can use some external relation of convertibility defined on the terms of the grammar, such as $\beta$-convertibility or $\beta \eta$-convertibility; or one can introduce a judgement form for equality into the rules of the typing system itself. For quite some time, it has been an open problem whether the two systems produced by these two choices are equivalent. This problem is essentially the problem of proving that the Subject Reduction property holds in the system with judgemental equality. In this paper, we shall prove that the equivalence holds for all functional Pure Type Systems (PTSs). The proof essentially consists of proving the Church-Rosser Theorem for a typed version of parallel one-step reduction. This method should generalise easily to many typing systems which satisfy the Uniqueness of Types property.
|
|
| 6. |
- Barthe, G., et al.
(författare)
-
Remarks on the equational theory of non-normalizing pure type systems
- 2006
-
Ingår i: Journal of Functional Programming. - 0956-7968 .- 1469-7653. ; 16:2, s. 137-155
-
Tidskriftsartikel (refereegranskat)abstract
- Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped λ-abstractions (i.e. of the form λx. M); and domain-free systems with typed λ-abstractions (i.e. of the form λx :A. M). Both flavours of systems are related by an erasure function |.| that removes types from λ-abstractions. Preservation of Equational Theory, which states the equational theories of both systems coincide through the erasure function, is a property of functional and normalizing PTSs. In this paper we establish that Preservation of Equational Theory fails for some non-normalizing PTSs, including the PTS with * : *. The gist of our argument is to exhibit a typable expression YH whose erasure |Y| is a fixpoint combinator, but which is not a fixpoint combinator itself.
|
|
| 7. |
- Barthes, Gilles, et al.
(författare)
-
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming
- 2004
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 14:1, s. 1-2
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- 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.
|
|
| 8. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Efficient Parallel and Incremental Parsing
- 2015
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968.
-
Tidskriftsartikel (refereegranskat)abstract
- We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is O(n^3), it improves to O(\log^2 n) under certain conditions satisfied by many useful inputs that occur in practice, and if one uses a sparse representation of matrices. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms with a polylogarithmic conquer step can be parallelised relatively easily.
|
|
| 9. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Efficient parallel and incremental parsing of practical context-free languages
- 2015
-
Ingår i: Journal of Functional Programming. - : Cambridge University Press (CUP). - 1469-7653 .- 0956-7968. ; 25, s. Article Number: UNSP e10-
-
Tidskriftsartikel (refereegranskat)abstract
- We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975; General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10(2), 308-314), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is O(n(3)), it improves to O(log(2) n) under certain conditions satisfied by many useful inputs that occur in practice, and if one uses a sparse representation of matrices. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms with a polylogarithmic conquer step can be parallelized relatively easily.
|
|
| 10. |
- Bernardy, Jean-Philippe, 1978, et al.
(författare)
-
Generic programming with C++ concepts and Haskell type classes—a comparison
- 2010
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 20:3-4, s. 271-302
-
Tidskriftsartikel (refereegranskat)abstract
- Earlier studies have introduced a list of high-level evaluation criteria to assess how well a language supports generic programming. Languages that meet all criteria include Haskell, because of its type classes, and C++ with the concept feature. We refine these criteria into a taxonomy that captures commonalities and differences between type classes in Haskell and concepts in C++, and discuss which differences are incidental and which ones are due to other language features. The taxonomy allows for an improved understanding of language support for generic programming, and the comparison is useful for the ongoing discussions among language designers and users of both languages.
|
|
