Showing 1–18 of 18 results for author: Scherer, G

Unboxed data constructors -- or, how cpp decides a halting problem

Authors: Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop

Abstract: We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusions, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxin… ▽ More We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusions, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes. Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order lambda-calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our termination-monitoring algorithm turns out to be closely related to the normalization strategy for macro expansion in the `cpp` preprocessor. △ Less

Submitted 9 May, 2024; v1 submitted 13 November, 2023; originally announced November 2023.

Coqlex: Generating Formally Verified Lexers

Authors: Wendlasida Ouedraogo, Gabriel Scherer, Lutz Strassburger

Abstract: A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components. However, some com… ▽ More A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of each component of the tool-chain. An example is the CompCert project, a formally verified C compiler, that comes with associated tools and proofs that allow to formally verify most of those components. However, some components, in particular the lexer, remain unverified. In fact, the lexer of Compcert is generated using OCamllex, a lex-like OCaml lexer generator that produces lexers from a set of regular expressions with associated semantic actions. Even though there exist various approaches, like CakeML or Verbatim++, to write verified lexers, they all have only limited practical applicability. In order to contribute to the end-to-end verification of compilers, we implemented a generator of verified lexers whose usage is similar to OCamllex. Our software, called Coqlex, reads a lexer specification and generates a lexer equipped with a Coq proof of its correctness. It provides a formally verified implementation of most features of standard, unverified lexer generators. The conclusions of our work are two-fold: Firstly, verified lexers gain to follow a user experience similar to lex/flex or OCamllex, with a domain-specific syntax to write lexers comfortably. This introduces a small gap between the written artifact and the verified lexer, but our design minimizes this gap and makes it practical to review the generated lexer. The user remains able to prove further properties of their lexer. Secondly, it is possible to combine simplicity and decent performance. Our implementation approach that uses Brzozowski derivatives is noticeably simpler than the previous work in Verbatim++ that tries to generate a deterministic finite automaton (DFA) ahead of time, and it is also noticeably faster thanks to careful design choices. We wrote several example lexers that suggest that the convenience of using Coqlex is close to that of standard verified generators, in particular, OCamllex. We used Coqlex in an industrial project to implement a verified lexer of Ada. This lexer is part of a tool to optimize safety-critical programs, some of which are very large. This experience confirmed that Coqlex is usable in practice, and in particular that its performance is good enough. Finally, we performed detailed performance comparisons between Coqlex, OCamllex, and Verbatim++. Verbatim++ is the state-of-the-art tool for verified lexers in Coq, and the performance of its lexer was carefully optimized in previous work by Egolf and al. (2022). Our results suggest that Coqlex is two orders of magnitude slower than OCamllex, but two orders of magnitude faster than Verbatim++. Verified compilers and other language-processing tools are becoming important tools for safety-critical or security-critical applications. They provide trust and replace more costly approaches to certification, such as manually reading the generated code. Verified lexers are a missing piece in several Coq-based verified compilers today. Coqlex comes with safety guarantees, and thus shows that it is possible to build formally verified front-ends. △ Less

Submitted 21 June, 2023; originally announced June 2023.

Journal ref: The Art, Science, and Engineering of Programming, 2024, Vol. 8, Issue 1, Article 3

Debootstrap** without Archeology: Stacked Implementations in Camlboot

Authors: Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer

Abstract: Context: It is common for programming languages that their reference implementation is implemented in the language itself. This requires a "bootstrap": a copy of a previous version of the implementation is provided along with the sources, to be able to run the implementation itself. Those bootstrap files are opaque binaries; they could contain bugs, or even malicious changes that could reproduce t… ▽ More Context: It is common for programming languages that their reference implementation is implemented in the language itself. This requires a "bootstrap": a copy of a previous version of the implementation is provided along with the sources, to be able to run the implementation itself. Those bootstrap files are opaque binaries; they could contain bugs, or even malicious changes that could reproduce themselves when running the source version of the language implementation -- this is called the "trusting trust attack". For this reason, a collective project called Bootstrappable was launched in 2016 to remove those bootstraps, providing alternative build paths that do not rely on opaque binaries. Inquiry: Debootstrap** generally combines a mix of two approaches. The "archaeological" approach works by locating old versions of systems, or legacy alternative implementations, that do not need the bootstrap, and by preserving or restoring the ability to run them. The "tailored" approach re-implements a new, non-bootstrapped implementation of the system to debootstrap. Currently, the "tailored" approach is dominant for low-level system components (C, coreutils), and the "archaeological" approach is dominant among the few higher-level languages that were debootstrapped. Approach: We advocate for the benefits of "tailored" debootstrap** implementations of high-level languages. The new implementation needs not be production-ready, it suffices that it is able to run the reference implementation correctly. We argue that this is feasible with a reasonable development effort, with several side benefits besides debootstrap**. Knowledge: We propose a specific design of composing/stacking several implementations: a reference interpreter for the language of interest, implemented in a small subset of the language, and a compiler for this small subset (in another language). Develo** a reference interpreter is valuable independently of debootstrap**: it may help clarify the language semantics, and can be reused for other purposes such as differential testing of the other implementations. Grounding: We present Camlboot, our project to debootstrap the OCaml compiler, version 4.07. Once we converged on this final design, the last version of Camlboot took about a person-month of implementation effort, demonstrating feasibility. Using diverse double-compilation, we were able to prove the absence of trusting trust attack in the existing bootstrap of the standard OCaml implementation. Importance: To our knowledge, this document is the first scholarly discussion of "tailored" debootstrap** for high-level programming languages. Debootstrap** is an interesting problem which recently grew an active community of free software contributors, but so far the interactions with the programming-language research community have been minimal. We share our experience on Camlboot, trying to highlight aspects that are of interest to other language designers and implementors; we hope to foster stronger ties between the Bootstrappable project and relevant academic communities. In particular, the debootstrap** experience has been an interesting reflection on OCaml design and implementation, and we hope that other language implementors would find it equally valuable. △ Less

Submitted 18 February, 2022; originally announced February 2022.

Journal ref: The Art, Science, and Engineering of Programming, 2022, Vol. 6, Issue 3, Article 13

Tail Modulo Cons

Authors: Frédéric Bour, Basile Clément, Gabriel Scherer

Abstract: OCaml function calls consume space on the system stack. Operating systems set default limits on the stack space which are much lower than the available memory. If a program runs out of stack space, they get the dreaded "Stack Overflow" exception -- they crash. As a result, OCaml programmers have to be careful, when they write recursive functions, to remain in the so-called _tail-recursive_ fragmen… ▽ More OCaml function calls consume space on the system stack. Operating systems set default limits on the stack space which are much lower than the available memory. If a program runs out of stack space, they get the dreaded "Stack Overflow" exception -- they crash. As a result, OCaml programmers have to be careful, when they write recursive functions, to remain in the so-called _tail-recursive_ fragment, using _tail_ calls that do not consume stack space. This discipline is a source of difficulties for both beginners and experts. Beginners have to be taught recursion, and then tail-recursion. Experts disagree on the "right" way to write `List.map`. The direct version is beautiful but not tail-recursive, so it crashes on larger inputs. The naive tail-recursive transformation is (slightly) slower than the direct version, and experts may want to avoid that cost. Some libraries propose horrible implementations, unrolling code by hand, to compensate for this performance loss. In general, tail-recursion requires the programmer to manually perform sophisticated program transformations. In this work we propose an implementation of "Tail Modulo Cons" (TMC) for OCaml. TMC is a program transformation for a fragment of non-tail-recursive functions, that rewrites them in _destination-passing style_. The supported fragment is smaller than other approaches such as continuation-passing-style, but the performance of the transformed code is on par with the direct, non-tail-recursive version. Many useful functions that traverse a recursive datastructure and rebuild another recursive structure are in the TMC fragment, in particular `List.map` (and `List.filter`, `List.append`, etc.). Finally those functions can be written in a way that is beautiful, correct on all inputs, and efficient. △ Less

Submitted 19 February, 2021; originally announced February 2021.

Dependent Pearl: Normalization by realizability

Authors: Pierre-Évariste Dagand, Lionel Rieg, Gabriel Scherer

Abstract: For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness. Why do they work? At which point in the proof is "the real work" done? Ho** to build a programming intuition of these proofs, we implement a normalization a… ▽ More For those of us who generally live in the world of syntax, semantic proof techniques such as reducibility, realizability or logical relations seem somewhat magical despite -- or perhaps due to -- their seemingly unreasonable effectiveness. Why do they work? At which point in the proof is "the real work" done? Ho** to build a programming intuition of these proofs, we implement a normalization argument for the simply-typed lambda-calculus with sums: instead of a proof, it is described as a program in a dependently-typed meta-language. The semantic technique we set out to study is Krivine's classical realizability, which amounts to a proof-relevant presentation of reducibility arguments -- unary logical relations. Reducibility assigns a predicate to each type, realizability assigns a set of realizers, which are abstract machines that extend lambda-terms with a first-class notion of contexts. Normalization is a direct consequence of an adequacy theorem or "fundamental lemma", which states that any well-typed term translates to a realizer of its type. We show that the adequacy theorem, when written as a dependent program, corresponds to an evaluation procedure. In particular, a weak normalization proof precisely computes a series of reduction from the input term to a normal form. Interestingly, the choices that we make when we define the reducibility predicates -- truth and falsity witnesses for each connective -- determine the evaluation order of the proof, with each datatype constructor behaving in a lazy or strict fashion. While most of the ideas in this presentation are folklore among specialists, our dependently-typed functional program provides an accessible presentation to a wider audience. In particular, our work provides a gentle introduction to abstract machine calculi which have recently been used as an effective research vehicle. △ Less

Submitted 27 July, 2020; v1 submitted 24 August, 2019; originally announced August 2019.

Functional programming with lambda-tree syntax

Authors: Ulysse Gérard, Dale Miller, Gabriel Scherer

Abstract: We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly sup… ▽ More We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly support this movement of bindings. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory within a rich logic that includes both *nominal abstraction* and the *nabla-quantifier*: as a result, the natural semantics specification of MLTS can be given a succinct and elegant presentation. We present a ty** discipline that naturally extends the ty** of core ML programs and we illustrate the features of MLTS by presenting several examples. An on-line interpreter for MLTS is briefly described. △ Less

Submitted 9 August, 2019; originally announced August 2019.

Comments: PPDP 2019

Proceedings ML Family / OCaml Users and Developers workshops

Authors: Sam Lindley, Gabriel Scherer

Abstract: This volume contains the joint post-proceedings of the 2017 editions of the ML Family Workshop and the OCaml Users and Developers Workshop which took place in Oxford, UK, September 2017, and which were colocated with the ICFP 2017 conference. This volume contains the joint post-proceedings of the 2017 editions of the ML Family Workshop and the OCaml Users and Developers Workshop which took place in Oxford, UK, September 2017, and which were colocated with the ICFP 2017 conference. △ Less

Submitted 14 May, 2019; originally announced May 2019.

ACM Class: F.3.2; F.3.3; D.3.3; D.3.4

Journal ref: EPTCS 294, 2019

A Practical Mode System for Recursive Definitions

Authors: Alban Reynaud, Gabriel Scherer, Jeremy Yallop

Abstract: In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures. We present a set of declarative inference rules, prove its sound… ▽ More In call-by-value languages, some mutually-recursive value definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures. We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander, Carlsson, and Gill (2008), and show that it can be (right-to-left) directed into an algorithmic check in a surprisingly simple way. Our implementation of this new check replaced the existing check used by the OCaml programming language, a fragile syntactic/grammatical criterion which let several subtle bugs slip through as the language kept evolving. We document some issues that arise when advanced features of a real-world functional language (exceptions in first-class modules, GADTs, etc.) interact with safety checking for recursive definitions. △ Less

Submitted 23 December, 2020; v1 submitted 20 November, 2018; originally announced November 2018.

Comments: Author version of POPL'21 article. 29 pages + Appendices

Unboxing Mutually Recursive Type Definitions in OCaml

Authors: Simon Colin, Rodolphe Lepigre, Gabriel Scherer

Abstract: In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic… ▽ More In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single field) can sometimes be `unboxed'. This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However, in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions. △ Less

Submitted 12 December, 2018; v1 submitted 6 November, 2018; originally announced November 2018.

Comments: accepted at JFLA 2019

Merlin: A Language Server for OCaml (Experience Report)

Authors: Frédéric Bour, Thomas Refis, Gabriel Scherer

Abstract: We report on the experience of develo** Merlin, a language server for the OCaml programming language in development since 2013. Merlin is a daemon that connects to your favourite text editor and provides services that require a fine-grained understanding of the programming language syntax and static semantics: instant feedback on warnings and errors, autocompletion, `type of the code under the c… ▽ More We report on the experience of develo** Merlin, a language server for the OCaml programming language in development since 2013. Merlin is a daemon that connects to your favourite text editor and provides services that require a fine-grained understanding of the programming language syntax and static semantics: instant feedback on warnings and errors, autocompletion, `type of the code under the cursor', `go to definition', etc. Language servers need to handle incomplete and partially-incorrect programs, and try to be incremental to minimize recomputation after small editing actions. Merlin was built by carefully adapting the existing tools (the OCamllex lexer and Menhir parser generators) to better support incrementality, incompleteness and error handling. These extensions are elegant and general, as demonstrated by the interesting, unplanned uses that the OCaml community found for them. They could be adapted to other frontends -- in any language. Besides incrementality, we discuss the way Merlin communicates with editors, describe the design decisions that went into some demanding features and report on some of the non-apparent difficulties in building good editor support, emerging from expressive programming languages or frustrating tooling ecosystems. We expect this experience report to be of interest to authors of interactive language tooling for any programming language; many design choices may be reused, and some hard-won lessons can serve as warnings. △ Less

Submitted 2 October, 2018; v1 submitted 17 July, 2018; originally announced July 2018.

Correctness of Speculative Optimizations with Dynamic Deoptimization

Authors: Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek

Abstract: High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that a… ▽ More High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that are no longer valid. The implementation must then deoptimize the program on-the-fly; this entails finding semantically equivalent code that does not rely on invalid assumptions, translating program state to that expected by the target code, and transferring control. This paper looks at the interaction between optimization and deoptimization, and shows that reasoning about speculation is surprisingly easy when assumptions are made explicit in the program representation. This insight is demonstrated on a compiler intermediate representation, named \sourir, modeled after the high-level representation for a dynamic language. Traditional compiler optimizations such constant folding, dead code elimination, and function inlining are shown to be correct in the presence of assumptions. Furthermore, the paper establishes the correctness of compiler transformations specific to deoptimization: namely unrestricted deoptimization, predicate hoisting, and assume composition. △ Less

Submitted 15 November, 2017; v1 submitted 8 November, 2017; originally announced November 2017.

Journal ref: Proceedings of the ACM on Programming Languages (POPL 2018)

Capturing the Future by Replaying the Past

Authors: James Koppel, Gabriel Scherer, Armando Solar-Lezama

Abstract: Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski's 1994 paper, which showed that delimited continuations can implement any monadic effect, letting the programmer use an effect as easily as if it was built into the language. It's a shame that not many languages have delimited continuations. Luckily, exceptions and state are also the mother of all monad… ▽ More Delimited continuations are the mother of all monads! So goes the slogan inspired by Filinski's 1994 paper, which showed that delimited continuations can implement any monadic effect, letting the programmer use an effect as easily as if it was built into the language. It's a shame that not many languages have delimited continuations. Luckily, exceptions and state are also the mother of all monads! In this Pearl, we show how to implement delimited continuations in terms of exceptions and state, a construction we call $\textit{thermometer continuations}$. While traditional implementations of delimited continuations require some way of "capturing" an intermediate state of the computation, the insight of thermometer continuations is to reach this intermediate state by replaying the entire computation from the start, guiding it using a recording it so that the same thing happens until the captured point. Along the way, we explain delimited continuations and monadic reflection, show how the Filinski construction lets thermometer continuations express any monadic effect, share an elegant special-case for nondeterminism, and discuss why our construction is not prevented by theoretical results that exceptions and state cannot macro-express continuations. △ Less

Submitted 5 July, 2018; v1 submitted 28 October, 2017; originally announced October 2017.

FabULous Interoperability for ML and a Linear Language

Authors: Gabriel Scherer, Max New, Nick Rioux, Amal Ahmed

Abstract: Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users fam… ▽ More Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages. We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system. To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language. △ Less

Submitted 12 April, 2018; v1 submitted 16 July, 2017; originally announced July 2017.

Comments: Published in Fossacs 2018

MSC Class: 68N15; 68N30 ACM Class: F.3.1; F.3.2; F.3.3

Deciding equivalence with sums and the empty type

Authors: Gabriel Scherer

Abstract: The logical technique of focusing can be applied to the $λ$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $βη$-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidab… ▽ More The logical technique of focusing can be applied to the $λ$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $βη$-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidability of $βη$-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property. △ Less

Submitted 8 November, 2016; v1 submitted 4 October, 2016; originally announced October 2016.

MSC Class: 03F03; 68N18 ACM Class: F.3.3; F.4.1

Tracking Data-Flow with Open Closure Types

Authors: Gabriel Scherer, Jan Hoffmann

Abstract: Type systems hide data that is captured by function closures in function types. In most cases this is a beneficial design that favors simplicity and compositionality. However, some applications require explicit information about the data that is captured in closures. This paper introduces open closure types, that is, function types that are decorated with type contexts. They are used to track data… ▽ More Type systems hide data that is captured by function closures in function types. In most cases this is a beneficial design that favors simplicity and compositionality. However, some applications require explicit information about the data that is captured in closures. This paper introduces open closure types, that is, function types that are decorated with type contexts. They are used to track data-flow from the environment into the function closure. A simply-typed lambda calculus is used to study the properties of the type theory of open closure types. A distinctive feature of this type theory is that an open closure type of a function can vary in different type contexts. To present an application of the type theory, it is shown that a type derivation establishes a simple non-interference property in the sense of information-flow theory. A publicly available prototype implementation of the system can be used to experiment with type derivations for example programs. △ Less

Submitted 29 November, 2013; originally announced December 2013.

Comments: Logic for Programming Artificial Intelligence and Reasoning (2013)

GADTs meet subty**

Authors: Gabriel Scherer, Didier Rémy

Abstract: While generalized algebraic datatypes (\GADTs) are now considered well-understood, adding them to a language with a notion of subty** comes with a few surprises. What does it mean for a \GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subty** relation that raise interesting design questions. We allow variance annotations in \G… ▽ More While generalized algebraic datatypes (\GADTs) are now considered well-understood, adding them to a language with a notion of subty** comes with a few surprises. What does it mean for a \GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subty** relation that raise interesting design questions. We allow variance annotations in \GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subty** such as OCaml, or to languages with general subty** constraints. △ Less

Submitted 14 January, 2013; originally announced January 2013.

Comments: arXiv admin note: substantial text overlap with arXiv:1210.5935

Journal ref: 22nd European Symposium on Programming (ESOP), Rome : Italy (2013)

GADT meet Subty**

Authors: Gabriel Scherer, Didier Rémy

Abstract: While generalized abstract datatypes (GADT) are now considered well-understood, adding them to a language with a notion of subty** comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subty** relation that raise interesting design questions. We allow variance annotations in GADT d… ▽ More While generalized abstract datatypes (GADT) are now considered well-understood, adding them to a language with a notion of subty** comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subty** relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subty** such as OCaml, or to languages with general subty** constraints. △ Less

Submitted 22 October, 2012; originally announced October 2012.

Comments: No. RR-8114 (2012)

On Irrelevance and Algorithmic Equality in Predicative Type Theory

Authors: Andreas Abel, Gabriel Scherer

Abstract: Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with irrelevant quantification which is compatible with a type-based notion of equality that respects eta-laws. W… ▽ More Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with irrelevant quantification which is compatible with a type-based notion of equality that respects eta-laws. We extend Pfenning's theory to universes and large eliminations and develop its meta-theory. Subject reduction, normalization and consistency are obtained by a Kripke model over the typed equality judgement. Finally, a type-directed equality algorithm is described whose completeness is proven by a second Kripke model. △ Less

Submitted 23 March, 2012; v1 submitted 21 March, 2012; originally announced March 2012.

Comments: 36 pages, superseds the FoSSaCS 2011 paper of the first author, titled "Irrelevance in Type Theory with a Heterogeneous Equality Judgement"

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 1 (March 27, 2012) lmcs:1045