DOC PREVIEW
paper

This preview shows page 1-2-3-4 out of 12 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 12 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Submitted to POPL ’08An Extensible Theory of Indexed TypesDaniel R. Licata Robert HarperCarnegie Mellon University{drl,rwh}@cs.cmu.eduAbstractIndexed families of types are a way of associating run-time datawith compile-time abstractions that can be used to reason aboutthem. We propose an extensible theory of indexed types, in whichprogrammers can define the index data appropriate to their pro-grams and use them to track properties of run-time code. The es-sential ingredients in our proposal are (1) a logical framework,which is used to define index data, constraints, and proofs, and(2) computation with indices, both at the static and dynamic levelsof the programming language. Computation with indices supportsa variety of mechanisms necessary for programming with exten-sible indexed types, including the definition and implementationof indexed types, meta-theoretic reasoning about indices, proof-producing run-time checks, computed index expressions, and run-time actions of index constraints.Programmer-defined index propositions and their proofs can berepresented naturally in a logical framework such as LF, wherevariable binding is used to model the consequence relation of thelogic. Consequently, the central technical challenge in our designis that computing with indices requires computing with the higher-order terms of a logical framework. The technical contributions ofthis paper are a novel method for computing with the higher-orderdata of a simple logical framework and the integration of such com-putation into the static and dynamic levels of a programming lan-guage. Further, we present examples showing how this computationsupports indexed programming.1. IntroductionOne way to enrich the expressiveness of a type system is to providethe programmer with a rich language of data that can be used,at compile-time, to state and verify properties of run-time code.Compile-time data can be associated with run-time values usingan indexed family of types whose indices vary with the classifiedvalues. For example, a programmer might define a family of typeslist[n:nat], indexed by a natural number representing thelength of the list, and varying with the list constructors:nil : list[0]cons : ∀n:nat.elt -> list[n] -> list[n+1]Examples of indexing include dependent types, where the indicesare the drawn from the run-time programming language (Augusts-son, 1998; Coquand and Huet, 1988; Flanagan, 2006; McBride andMcKinna, 2004), and generalized algebraic datatypes, where the in-[Copyright notice will appear here once ’preprint’ option is removed.]dices are other types (Cheney and Hinze, 2003; Peyton Jones et al.,2006; Sheard, 2004; Xi et al., 2003), as well as types indexed bystatic constraint domains (Chen and Xi, 2005; Dunfield and Pfen-ning, 2004; Fogarty et al., 2007; Licata and Harper, 2005; Sarkar,2005; Xi and Pfenning, 1998), by propositions (Nanevski et al.,2006), and by proofs.Indices serve as modelling types in the sense of Leino andM¨uller (2004), in that they define an abstraction of program val-ues which may be used for reasoning. With dependent types, theavailable modelling types are the same as the values they model,and data is often used as its own model. Using more general index-ing, one can model a value with abstractions other than the valueitself, and the model need not be drawn from the run-time language.For example, static array bounds checking, as in Xi and Pfen-ning (1998), is possible using a family of types array[i:nat],which does not track the contents of the array but only its lengthi. Another example is Sarkar’s use of the types term[e:tm]and typ[t:tp], which index run-time datatypes representing thetypes and terms of a programming language by their LF (Harperet al., 1993) representations. The key application of indexing isthat index information may be used to state properties of an abstractdata type in its interface. For example, Sarkar writes a certified typechecker, employing the LF representation of the language’s typingjudgement as an index constraint:check : ∀e.∀t.term[e] -> typ[t]-> (∃d::of e t.unit) + unitWhen this function returns true, it also returns a certificate, rep-resented as an LF derivation of the judgement of e t, that theprogram is well-typed. Indexed types enable richer interfaces atmodule boundaries, serve as machine-checked documentation, andobviate some run-time checks. Proving that a program possessesa more precise type can be harder, but in return the type tellsmore about the program’s behavior. Pragmatically, the programmercan use indexing inasmuch as it seems worthwhile to capture suchstrong invariants.An Extensible Theory of Indexing. We wish to provide an ex-tensible theory of indexing, in which programmers can define theirown index domains and use them to give stronger interfaces. Anextensible framework must at least provide the ability to define in-dex domains, index expressions inhabiting them, constraints on in-dices, proofs of constraints, indexed families of types computed byanalysis of indices, and inhabitants of such families computed bysuch analysis. This can be achieved by equipping a functional lan-guage with a logical framework that is sufficiently powerful to rep-resent index domains, index expressions, constraints, and proofs.Representing constraints and proofs necessitates a framework suchas LF (Harper et al., 1993) that involves binding and scope, whichare used to model the consequence relation of a logic. Then in-dexed families of types can be defined and implemented by provid-ing structural induction, modulo α-renaming, over the terms of theframework.To illustrate these ideas, we define a type of queues whose con-tents are tracked by the type system. For tracking the contents of1 2007/7/19signature FIN SET THY = sigfam ind : Type % elements of setsfam set : Type % finite setsobj void : set.obj sing : ind → set.objs union, diff : set → set → set.fam prop : Type % propositionsobjs eq, neq : set → set → prop.fam pf : prop → Type % proofs...endFigure 1. LF Signature for Finite Set Theorysignature QUEUE = sigimport Sets : FIN SET THY% elements indexed by indtyp elt : ind ⇒ type% queues indexed by setstyp queue : set ⇒ typeval empty : queue[void]val enq :∀ i:ind ∀ s:set elt[i] → queue[s] →∃ t:set ∃ :pf(eq(t,union(s,sing(i))))queue[t]val deq :∀ s:set ∀:pf(neq(s,void)) queue[s] →∃ i:ind ∃ t:set∃ :pf(eq(t,diff(s,sing(i))))elt[i] × queue[t]endFigure 2. Signature for


paper

Download paper
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view paper and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view paper 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?