ZU064-05-FPR

main

23 September 2019

10:36

Under consideration for publication in J. Functional Programming

1

Pure Iso-Type Systems
Yanpeng Yang and Bruno C. d. S. Oliveira
The University of Hong Kong, Pokfulam, Hong Kong(e-mail: {ypyang,bruno}@cs.hku.hk)

Abstract
Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax forterms and types. In contrast, many dependently typed languages use a unified syntax that accounts forboth terms and types. Unified syntax has some interesting advantages over separate syntax, including
less duplication of concepts, and added expressiveness. However, integrating unrestricted generalrecursion in calculi with unified syntax is challenging when some level of type-level computation ispresent, since properties such as decidable type-checking are easily lost.
This paper presents a family of calculi called pure iso-type systems (PITS), which employs unified
syntax, supports general recursion and preserves decidable type-checking. PITS is comparable insimplicity to pure type systems (PTSs), and is useful to serve as a foundation for functional languages
that stand in-between traditional ML-like languages and fully-blown dependently typed languages.
In PITS recursion and recursive types are completely unrestricted and type equality is simply basedon alpha-equality, just like traditional ML-style languages. However, like most dependently typed
languages, PITS uses unified syntax, naturally supporting many advanced type system features.
Instead of implicit type conversion, PITS provides a generalization of iso-recursive types called
iso-types. Iso-types replace the conversion rule typically used in dependently typed calculus, andmake every type-level computation explicit via cast operators. Iso-types avoid the complexity of
explicit equality proofs employed in other approaches with casts. We study three variants of PITS
that differ on the reduction strategy employed by the cast operators: call-by-name, call-by-value
and parallel reduction. One key finding is that while using call-by-value or call-by-name reduction
in casts loses some expressive power, it allows those variants of PITS to have simple and direct
operational semantics and proofs. In contrast the variant of PITS with parallel reduction retains theexpressive power of PTS conversion, at the cost of a more complex metatheory.

1 Introduction
Dependent types are gaining popularity in functional programming language design andresearch in recent years (Augustsson, 1998; Altenkirch et al., 2010; Sjöberg et al., 2012;
Stump et al., 2008; Weirich et al., 2013; Gundry, 2013; Casinghino et al., 2014; Sjöberg& Weirich, 2015; Sjöberg, 2015; Eisenberg, 2016; Weirich et al., 2017). Several new fullspectrum dependently languages, including Agda (Norell, 2007) or Idris (Brady, 2011),
are emerging. These languages are designed to be both programming languages and proof
assistants. As such they support different forms of assurances, such as strong normalizationand logical consistency, not typically present in traditional programming languages such as
Haskell and ML. Nevertheless, traditional designs for functional languages still have somebenefits. While strong normalization and logical consistency are certainly nice properties
to have, and can be valuable to have in many domains, they can also impose restrictions

ZU064-05-FPR

main

2

23 September 2019

10:36

Y. Yang and B. Oliveira

on how programs are written. For example, the termination checking algorithms typically
employed by dependently typed languages such as Agda or Idris can only automaticallyensure termination of programs that follow certain patterns. Incorporating recursion andrecursive types in such languages needs careful checks (e.g. termination and positivity)
for not breaking the logical consistency and strong normalization. In contrast Haskell or
ML programmers can write their programs much more freely and can support generalrecursion and recursive types easily, since they do not need to retain strong normalizationand logical consistency. Thus the design space between ML-style languages and full-blown
dependently typed languages like Agda or Idris is very large.
From an implementation and foundational point-of-view, dependently typed languages
and traditional functional languages also have important differences. Languages like Haskell
or ML have a strong separation between terms and types (and also kinds). This separation
often leads to duplication of constructs. For example, when the type language provides
some sort of type level computation, constructs such as type application (Eisenberg et al.,2016) (mimicking value level application) may be needed. In contrast many dependently
typed languages unify types and terms. There are benefits in unifying types and terms. In
addition to the extra expressiveness afforded, for example, by dependent types, only one
syntactic level is needed. Thus duplication can be avoided. Having less language constructs
simplifies the language, making it easier to study (from the meta-theoretical point of view)
and maintain (from the implementation point of view).
In principle having unified syntax would be beneficial even for more traditional designsof functional languages, which do not have strong normalization or logical consistency andhave only restricted forms of type-level computation. Not surprisingly, researchers havein the past considered options for implementing functional languages based on unified
syntax (Augustsson, 1998; Cardelli, 1986; Peyton Jones & Meijer, 1997), by using somevariant of pure type systems (PTSs) (Barendregt, 1992) (normally extended with generalrecursion). Thus, with a simple and tiny calculus, they showed that powerful and quite
expressive functional languages could be built with unified syntax.
However, having unified syntax for types and terms brings challenges. One pressing
problem is that integrating (unrestricted) general recursion in dependently typed calculi
with unified syntax, while retaining logical consistency, strong normalization and decidable type-checking is difficult. Indeed, many early designs using unified syntax andunrestricted general recursion (Augustsson, 1998; Cardelli, 1986) lose all three properties.
For pragmatic reasons languages like Agda or Idris also allow turning off the termination
checker, which allows for added expressiveness, but loses the three properties as well.
For traditional languages, only the loss of decidable type-checking is problematic. Unlike strong normalization and logical consistency, decidable type-checking is normally one
property that is often desirable in a traditional programming language design. Decidable
type checking implies that an algorithm that checks whether an expression is typeable
or not exists. It is natural to ask the question of whether it is possible to come up with asimpler language design for unified syntax and general recursion, if all we wish to preserve
is decidable type-checking. Surprisingly, there are not so many designs that attempt tosupport unified syntax and general recursion with decidable type-checking. Notable exceptions are Dependently Typed Haskell (Weirich et al., 2017) (DTH) and PTSs with explicit

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

3

convertibility proofs (PTS f ) (van Doorn et al., 2013). However these works are still quite
involved due to the need of a separate language for building equality proof terms.
This paper presents a family of calculi called pure iso-type systems (PITS), which employs unified syntax, supports general recursion and preserves decidable type-checking.
PITS is comparable in simplicity to PTSs by making each type-level computation step
explicit. In essence, each type-level reduction or expansion is controlled by a type-safe
cast. Since single computation steps are trivially terminating, decidability of type checking
is possible even in the presence of non-terminating programs at the type level. At the sametime term-level programs using general recursion work as in any conventional functional
languages, and can be non-terminating. Such design choice is useful to serve as a foundation for functional languages that stand in-between traditional ML-like languages andfully-blown dependently typed languages. In PITS, recursion and recursive types are completely unrestricted and type equality is simply based on alpha-equality, just like traditional
ML-style languages. However, like most dependently typed languages, PITS uses unified
syntax, naturally supporting many advanced type system features (such as higher-kinded
types (Girard, 1972), or kind polymorphism (Yorgey et al., 2012)).
PITS design means that instead of an implicit type conversion (employed by PTS), PITS
provides a generalization of iso-recursive types (Crary et al., 1999; Pierce, 2002) called isotypes. Iso-types replace the conversion rule typically used in dependently typed calculus,
and make every type-level computation explicit via cast operators. While such explicit
casts would make many forms of dependently typed programming inconvenient, they are
sufficient to express the kind of type-level computation required by more traditional language designs. We study three variants of PITS that differ on the choice of the reduction
strategy used by cast operators: call-by-name, call-by-value or parallel reduction. The
different variants give different trade-offs in terms of simplicity and expressiveness, which
we discuss thoroughly in the paper.
One key finding is that while using call-by-value or call-by-name reduction in casts
loses some expressive power for type-level computation, it allows those variants of PITS
to have simple and direct operational semantics and proofs. In contrast the variant of PITS
with parallel reduction retains the expressive power of PTS conversion, at the cost of amore complex metatheory where type-safety proofs must be shown indirectly by showing
soundness/completeness to another variant of PTS. A detailed discussion of the trade-offs
between the variants of PITS, as well as PTS f , is given in Section 7.1.
To demonstrate the application of PITS, we build a simple surface language Fun that
extends PITS with algebraic datatypes by using a Scott encoding of datatypes (Mogensen,
1992). We also implement prototype interpreter and compiler for Fun, which can run all
examples shown in this paper.
In summary, the contributions of this work are:
• PITS: A variant of PTS with general recursion, unified syntax and decidable typechecking.
• Iso-types: A generalization of iso-recursive types, which makes all type-level computation steps explicit via casts operators. The combination of casts and recursion
subsumes iso-recursive types.

ZU064-05-FPR

main

4

23 September 2019

10:36

Y. Yang and B. Oliveira• Studying three different reduction strategies: We study PITS with three different
reduction strategies: call-by-name PITS, call-by-value PITS and PITS with parallel reduction at the type-level. One key conclusion is that call-by-name and callby-value PITS have very simple and direct operational semantics and proofs. The
added expressive power brought by parallel reduction complicates the semantics andmetatheory, and requires a more complex formalization.
• Mechanized proofs: All proofs of PITS in the paper are machine-checked in Coq
theorem prover (The Coq development team, 2016) and available online.
• Prototype implementation: Prototype interpreter and compiler for Fun, a simple
language based on PITS extended with algebraic datatypes, are implemented andavailable online.

This article is a significantly revised and expanded version of a conference paper (Yanget al., 2016). There are three main novelties with respect to the conference version. Firstly,
while the conference version of the paper only deals with a calculus of constructions (Coquand & Huet, 1988) style calculus (with the “type-in-type” axiom), PITS is generalized
to deal with a whole family of calculi in the PTS tradition. Secondly, the study of call-byvalue is new. Finally, for the third variant with parallel reduction, we prove a completenesstheorem that demonstrates that our parallel reduction relation subsumes full beta-reductionused in PTS. All related online materials are available from:https://bitbucket.org/ypyang/pits-jfp

2 Motivation and Overview
In this section, we motivate the design and informally introduce the main features of PITS.
In particular, we show how iso-types can be used to allow general recursion, instead of thetypical conversion rule in PTS. We also give examples to illustrate how features of modern
functional languages can be encoded in PITS. The formal details of PITS are presented in
Sections 4, 5 and 6.
2.1 Implicit Type Conversion in Pure Type Systems
Pure Type Systems (PTS) (Barendregt, 1991) are a generic framework to study a familyof type systems, including the Simply Typed Lambda Calculus (STLC), System F (Girard,1972) and the Calculus of Constructions (Coquand & Huet, 1988). A PTS is determinedby a triple (Sorts, A , R) (Barendregt, 1991) where A ⇢ Sorts ⇥ Sorts is a set of Axioms
to type sorts and R ⇢ Sorts ⇥ Sorts ⇥ Sorts is a set of Rules to type P-types. By specifying
the PTS triple, we can obtain specific type systems. For example, given Sort = {?, 2} andA = {(?, 2)}, if R = {(?, ?, ?)}, we obtain STLC; if R = {(?, ?, ?), (2, ?, ?)}, we obtain
System F.
The typing rules for PTS contain a conversion rule:G`e:A

A =b BG`e:B

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

5This rule allows one to derive e : B from the derivation of e : A with the beta equality of A
and B. This rule is important to automatically allow terms with beta equivalent types to beconsidered type-compatible. For example, consider the following identity function:f = l y : (l x : ?. x) Int. y
The type of y is a type-level identity function applied to Int. Without the conversion rule,
f cannot be applied to 3 for example, since the type of 3 (Int) differs from the type of y((l x : ?. x) Int). Note that the beta equivalence (l x : ?. x) Int =b Int holds. Therefore, theconversion rule allows the application of f to 3 by converting the type of y to Int.
Decidability of Type Checking and Strong Normalization. While the conversion rule in
PTS brings a lot of convenience, an unfortunate consequence is that it couples decidabilityof type checking with strong normalization of the calculus (van Benthem Jutting, 1993).
Therefore adding general recursion to PTS becomes difficult, since strong normalization islost. Due to the conversion rule, any non-terminating term would force the type checker togo into an infinite loop (by constantly applying the conversion rule without termination),thus rendering the type system undecidable. For example, assume a term z that has typeloop, where loop stands for any diverging computation. If we type check (l x : Int. x) z
under the normal typing rules of PTS, the type checker would get stuck as it tries tonormalize and compare two terms: Int and loop, where normalizing the latter is nonterminating.

2.2 Newtypes: A Mechanism for Explicit Type Conversion in Haskell
Early designs of functional languages such as Haskell deliberately forbid implicit typeconversions. However, although not widely appreciated, since the very beginning Haskell(and other functional languages) has supported explicit type-conversions via algebraic
datatypes, or their simpler sibling newtypes. In essence, encapsulated behind algebraic
datatypes and newtypes is a language mechanism that supports explicit type conversions.
Such language mechanism is closely related to iso-recursive types, but also allows forcomputations that are not recursive.
In early versions of Haskell, such as Haskell 98, there is no real type-level computation
as in dependently-typed languages such as Coq (The Coq development team, 2016). In particular, there are no computational type-level lambdas. Indeed Haskell forbids type-level
lambdas to avoid higher-order unification that is required in dependently typed languages
such as Coq or Agda (Jones, 1993). While modern Haskell is half the way in evolving into
a dependently typed language, it still does not support type-level lambdas.
Despite the absence of type-level lambdas, it is still possible to express type-level functions via newtype or data constructs. For example, the type Id defined bynewtype Id a = MkId {runId :: a}can be viewed as a type-level identity function and Id a is isomorphic to type a. To convert
the type back and forth between a and Id a, one needs to explicitly use the constructor
MkId or the destructor runId:

ZU064-05-FPR

main

23 September 2019

6

10:36

Y. Yang and B. Oliveira
MkId :: a ! Id a
runId :: Id a ! a

Iso-recursive Types in Haskell. More generally, it is possible to use newtypes to modelrecursive types in Haskell as well:
newtype Fix f = Fold {unfold :: f (Fix f )}The type Fix is a type-level fixpoint. Its constructor Fold forms a recursive type from function f and destructor unfold forces the computation to obtain the unrolling f (Fix f ). Suchtreatment of recursive types is well-studied, and it is essentially a form of iso-recursive
types.
While the explicit type level computations enabled by newtypes or algebraic datatypes
are very simple, they are essential for many of the characterizing programming styles
employed in Haskell. For example without such simple explicit type conversions it would
not be possible to have monadic programming (Wadler, 1995), or modular interpreters
enabled by approaches such as Datatypes à la Carte (Swierstra, 2008).
2.3 Iso-types: Explicit Type Conversion in PITS
The main source of inspiration for the design of PITS comes from iso-recursive types(Crary et al., 1999; Pierce, 2002). Iso-types offer an alternative to the conversion ruleof PTS, making it explicit as to when and where to convert one type to another. Typeconversions are explicitly controlled by two language constructs: cast# (one-step reduction) and cast" (one-step expansion). In PITS, not only folding/unfolding of recursion at
the type level is explicitly controlled by term level constructs, but also any other typelevel computation (including beta reduction/expansion). There is an analogy to language
designs with equi-recursive types and iso-recursive types, which are normally the two
options for adding recursive types to programming languages. With equi-recursive types,
type-level recursion is implicitly folded/unfolded, which makes establishing decidabilityof type-checking much more difficult. In iso-recursive designs, the idea is to trade someconvenience by a simple way to ensure decidability.
We view the design of traditional dependently typed calculi, such as PTS, as analogous
to systems with equi-recursive types. In PTS, it is the conversion rule that allows type-levelcomputation to by implicitly triggered. However, the proof of decidability of type checking
for PTS is non-trivial, as it depends on strong normalization (van Benthem Jutting, 1993).
Moreover decidability is lost when adding general recursion. In contrast, the cast operators
in PITS have to be used to explicitly trigger each step of type-level computation, but it iseasy to ensure decidable type-checking, even in the presence of general recursion. Anotherpotential benefit of iso-types is that the problem of type-inference may be significantly
simpler in a language with iso-types than in a language with a conversion rule. Jones’ workon type-inference for higher-kinded types in Haskell (Jones, 1993) seems to back up thisidea. We leave for future work exploring type-inference and unification for dependently
typed systems with iso-types.
PITS iso-types also have strong similarities with the explicit conversion mechanism
found in languages like Haskell. Differently from Haskell (and similarly to iso-recursive

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

7

types) iso-types are purely structural, while Haskell datatypes and newtypes are nominal.
Because iso-types are structural they can be directly represented with type-level lambdas(and other constructs). Moreover, since in PITS type equality is just alpha-equality, typelevel lambdas are not problematic, since they do not trigger computation during typechecking.
Reduction. The cast# operator allows a type conversion provided that the resulting type isa reduction of the original type of the term. To explain the use of cast# , assume an identity
function g defined by g = l y : Int. y and a term e such that e : (l x : ?. x) Int. In contrast
to PTS, we cannot directly apply g to e in PITS since the type of e ((l x : ?. x) Int) is notsyntactically equal to Int. However, note that the reduction relation (l x : ?. x) Int ,! Int
holds. Therefore, we can use cast# for the explicit (type-level) reduction:
cast# e : Int
Then the application g (cast# e) type checks.
Expansion. The dual operation of cast# is cast" , which allows a type conversion provided
that the resulting type is an expansion of the original type of the term. To explain the useof cast" , let us revisit the example from Section 2.1:
f = l y : (l x : ?. x) Int. y
We cannot apply f to 3 without the conversion rule. Instead, we can use cast" to expand
the type of 3:(cast" [(l x : ?. x) Int] 3) : (l x : ?. x) Int

Thus, the application f (cast" [(l x : ?. x) Int] 3) becomes well-typed. Intuitively, cast"performs expansion, as the type of 3 is Int, and (l x : ?. x) Int is the expansion of Int
witnessed by (l x : ?. x) Int ,! Int. Notice that for cast" to work, we need to provide theresulting type as argument. This is because for the same term, there may be more than one
choice for expansion. For example, 1 + 2 and 2 + 1 are both the expansions of 3.
One-Step. The cast operators allow only one-step reduction or expansion. If two typelevel terms require more than one step of reductions or expansions for normalization, thenmultiple casts must be used. Consider a variant of the example such that e : (l x : ?. l y :?. x) Int Bool. Given g = l y : Int. y, the expression g (cast# e) is ill-typed because cast# e
has type (l y : ?. Int) Bool, which is not syntactically equal to Int. Thus, we need anothercast# :
cast# (cast# e) : Intto further reduce the type and allow the program g (cast# (cast# e)) to type check.
Analogy to Newtypes in Haskell. By using cast operators, we can model the Haskell
example shown in Section 2.2:
Id = l x : ?. x
cast" [Id a] : a ! Id acast#
: Id a ! aZU064-05-FPR

main

8

23 September 2019

10:36

Y. Yang and B. Oliveiracast" and cast# are analogous to the datatype constructor MkId and destructor runId,
respectively. The difference is that PITS directly supports type-level lambdas without theneed of using newtype, though PITS only has alpha equality without implicit beta conversion. In some sense, type-level lambdas in PITS are non-computational as newtype-style“type functions” in Haskell. Nevertheless, we can still trigger type-level computation by
casts, similarly to newtype constructors and destructors in Haskell.
Decidability without Strong Normalization. With explicit type conversion rules the decidability of type checking no longer depends on the strong normalization property. Thus
the type system remains decidable even in the presence of non-termination at type level.
Consider the same example using the term z from Section 2.1. This time the type checker
will not get stuck when type checking (l x : Int. x) z. This is because in PITS, the typechecker only performs a syntactic comparison between Int and loop, instead of beta equality. Thus, it rejects the above application as ill-typed. By using explicit casts, the typechecker does not need to normalize types and it becomes decidable.
Variants of Casts. A reduction relation is used in cast operators to convert types. We
study three possible reduction relations: call-by-name reduction, call-by-value reduction
and full reduction. Call-by-name and call-by-value reduction cannot reduce sub-terms at
certain positions (e.g., inside l or P binders), while full reduction can reduce sub-terms at
any position. We also create three variants of PITS for each variant of casts. Specifically,full PITS uses a decidable parallel reduction relation with full cast operators cast* andcast+ . All variants reflect the idea of iso-types, but have trade-offs between simplicity
and expressiveness: call-by-name and call-by-value PITS use the same reduction relation
for both casts and evaluation to keep the system and metatheory simple, but lose some
expressiveness, e.g. cannot convert l x : Int. (1 + 1) to l x : Int. 2. Full PITS is more
expressive but results in a more complicated metatheory (see Section 6). Note that whengenerally referring to PITS, we do not specify the reduction strategy, which could be any
variant.

2.4 General Recursion
PITS supports general recursion and allows writing unrestricted recursive programs at theterm level. The recursive construct is also used to model recursive types at the type level.
Recursive terms and types are represented by the same µ primitive.
Recursive Terms. The primitive µx : A. e can be used to define recursive functions. For
example, the factorial function would be written as:fact = µ f : Int ! Int. l x : Int. if x == 0 then 1 else x ⇥ f (x1)

We treat the µ operator as a fixpoint, which evaluates µx : A. e to its recursive unfolding e[x 7! µx : A. e]. Term-level recursion in PITS works as in any standard functional
language, e.g., fact 3 produces 6 as expected (see Section 4.4).

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

9

Recursive Types. The same µ primitive is used at the type level to represent iso-recursive
types (Crary et al., 1999). In the iso-recursive approach a recursive type and its unfolding are different, but isomorphic. The isomorphism is witnessed by two operations, typically called fold and unfold. This is also similar to the previous Haskell example of(iso-)recursive types with Fold and unfold (see Section 2.2). In call-by-name PITS, suchisomorphism is witnessed by cast" and cast# . In fact, cast" and cast# generalize fold andunfold: they can convert any types, not just recursive types, as we shall see in the exampleof encoding parametrized datatypes in Section 3.
To demonstrate the use of casts with recursive types, we show the formation of the“hungry” type (Pierce, 2002) H = µx : ?. Int ! x. A term z of type H will accept one more
integer every time when it is unfolded by a cast# :(cast# z) 3
:H
cast# ((cast# z) 3) 3
:H
cast# (. . . (cast# z) 3 . . .) 3 : H
3 Applications
PITS is a simple core calculus, but expressive enough to encode useful language constructs.
In order to show how features of modern functional languages can be encoded in PITS,
we implemented a simple functional language Fun, a thin layer that is desugared to a
specific PITS with only a single sort ? and “type-in-type” axiom. Thus, Fun is not logicallyconsistent due to the “type-in-type” axiom. We focus on common features available intraditional functional languages and some interesting type-level features, but not the fullpower of dependent types. In this section, we briefly introduce the implementation of Funand present examples.
Encodable Features. Table 1 shows a summary of encodable features in Fun, including
algebraic datatypes (Section 3.1), higher-kinded types (Section 3.2), datatype promotion(Section 3.2), high-order abstract syntax (Section 3.2) and object encodings (Section 3.3).
The encoding of algebraic datatypes in Fun uses Scott encodings (Mogensen, 1992). The
encoding itself uses casts, but the use of casts is completely transparent to programmers. In
other words the elaboration process inserts the casts automatically. Thus in all the examples
in 3.2 the casts are inferred automatically. We illustrate how to encode a simple form ofobjects in Section 3.3, but since we did not develop a source syntax for objects the encoding
is manual and requires programmers to use casts explicitly. All the examples (except thelast one) work in the 3 variants of PITS. We also discuss one final example on dependently
typed vectors (Section 3.4) that only works with parallel reduction. Vectors are an example
of what would be called a GADT (Xi et al., 2003; Cheney & Hinze, 2003; Peyton Joneset al., 2004) in Haskell terminology. All examples can run in the prototype interpreter andcompiler.
3.1 Fun Implementation
Fun uses PITS as its core language and provides surface language constructs for algebraic datatypes and pattern matching. The core language is a specific call-by-name PITS

ZU064-05-FPR

main

23 September 2019

10:36

10

Y. Yang and B. Oliveira
Table 1. Encodable Features of Fun

Encodable Features

Section

Encoding Method

Casts
Inferred

Full Casts
Required?

Algebraic Datatypes
Higher-kinded Types
Datatype Promotion
Higher-order Abstract Syntax
Object Encodings
Vectors and GADTs

3.1
3.2
3.2
3.2
3.3
3.4

Scott Encoding
Directly by Datatypes
Directly by Datatypes
Directly by Datatypes
Existential Types
Leibniz Equality

Yes
Yes
Yes
Yes
No
No

No
No
No
No
No
Yes

called l I (Yang et al., 2016). l I specifies the PITS triple (see Section 2.1) as Sort = {?},
A = {(?, ?)} and R = {(?, ?, ?)}. Algebraic datatypes and pattern matching in Fun are
implemented using Scott encodings (Mogensen, 1992), which can be later desugared into
PITS (l I) terms. For demonstration, we implemented a prototype interpreter and compiler
for Fun, both written in GHC Haskell (Marlow, 2010). Fun terms are firstly desugared intol I terms and then type-checked using PITS typing rules. The type-checked l I terms canbe evaluated directly by the interpreter or compiled to JavaScript or Haskell code.
Inferring Casts. As a surface language, explicit casts are mostly intended to be generated
by the compiler, but not by the programmers. Indeed, some casts in Fun are automatically inferred by elaboration rules. In particular the elaboration of algebraic datatypes
and pattern matching infers casts. Since the focus of this work is to illustrate the design
space of the core language with casts we do have not yet explored the addition of surfacelevel mechanisms for doing more advanced type-level computation built on top of casts.
Languages like Haskell have a similar design to Fun with a very explicit core languagewith casts. In Haskell cast inference is taken to an extreme. Many surface features in
Haskell, e.g., type families (Schrijvers et al., 2008) and associated types (Chakravarty et al.,2005), involve type-level computation where casts are inferred by the compiler. We hope
to explore similar type-level computation mechanisms in Fun in the future.
In this section, most examples written in Fun do not require programmers to write casts
directly as they are automatically inferred. Two exceptions are the encodings of objects andvectors, whose elaboration rules are not implemented in the Fun yet. We demonstrate these
two examples by manually adding casts. Also, to make them runnable in the prototype
implementation, cast operators from the core language are allowed to be called from thesurface programs.
Encoding Parametrized Algebraic Datatypes. We give an example of encoding parametrized algebraic datatypes in PITS via the µ-operator and explicit casts. Note that for
simplicity reasons, we use call-by-name casts to demonstrate the encoding. Call-by-value
casts can similarly be used for encoding, but require a more complex treatment of recursive types, since they become values in call-by-value PITS (will be discussed later in
Section 5.2). Importantly we should note that having iso-recursive types alone (and alphaZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

11

equality) would be insufficient to encode parametrized types: the generalization affordedby iso-types is needed here.
In Fun we can define a polymorphic list as
data List a = Nil | Cons a (List a);This Fun definition is translated into PITS using a Scott encoding (Mogensen, 1992) ofdatatypes:
List = µL : ? ! ?. l a : ?. Pb : ?. b ! (a ! L a ! b) ! b
Nil = l a : ?. cast2" [List a] (l b : ?. l n : b. l c : (a ! List a ! b). n)Cons = l a : ?. l x : a. l (xs : List a).
cast2" [List a] (l b : ?. l n : b. l c : (a ! List a ! b). c x xs)
The type constructor List is encoded as a recursive type1 .The body is a type-level functionthat takes a type parameter a and returns a dependent function type, i.e., P-type. The
body of P-type is universally quantified by a type parameter b, which represents the resulttype instantiated during pattern matching. Following are the types corresponding to data
constructors: b for Nil, and a ! L a ! b for Cons, and the result type b at the end. The
data constructors Nil and Cons are encoded as functions. Each of them selects a different
function from the parameters (n and c). This provides branching in the process flow, basedon the constructors. Note that cast" is used twice here (written as cast2" ): one for onestep expansion from t to (l a : ?. t) a and the other for folding the recursive type from(l a : ?. t) a to List a, where t is the type of cast2" body.
We have two notable remarks from the example above. Firstly, iso-types are critical
for the encoding and cannot be replaced by iso-recursive types. Since type constructors
are parametrized, not only folding/unfolding recursive types, but also type-level reduction/expansion is required, which is only possible with casts. Secondly, although casts
using call-by-value and call-by-name reduction are not as powerful as casts using fullbeta-reduction, they are still capable of encoding many useful constructs, such as algebraic
datatypes and records. Nevertheless full-reduction casts enable other important applications. Some applications of full casts are discussed later (see Section 3.4).
3.2 Combining Algebraic Datatypes with Advanced Features
Languages like Haskell support several advanced type-level features. Such features, whenused in combination with algebraic datatypes, have important applications. Next we discuss
some of these features and their applications. The purpose is to show all these advanced
features are encodable in PITS. For simplicity reasons, we use arrow syntax (x : A) ! B as
syntactic sugar for P-types Px : A.B in the following text.

1

An alternative way of encoding is to flip L and a as List = l a : ?. µL : ?. Pb : ?. b ! (a ! L !
b) ! b. However, L here is not parametric and implicitly has a fixed parameter a. Such encoding
is more limited and does not work with non-uniform types where parameters can vary (e.g. PTree
example in Section 3.2).

ZU064-05-FPR

main

23 September 2019

12

10:36

Y. Yang and B. Oliveira

Higher-kinded Types. Higher-kinded types are type-level functions. To support higherkinded types, languages like Haskell use core languages that account for kind expressions.
The existing core language of Haskell, System FC (Sulzmann et al., 2007), is an extensionof System Fw (Girard, 1972), which natively supports higher-kinded types. We can similarly construct higher-kinded types in PITS. We show an example of encoding the functor“type-class” as a record:
data Functor (f : ? ! ?) =Func {fmap : (a : ?) ! (b : ?) ! (a ! b) ! f a ! f b};
Note that in PITS, records are encoded using algebraic datatypes in a similar way as
Haskell’s record syntax (Marlow, 2010). Here we use a record to represent a functor, whose
only field is a function called fmap. The functor “instance” of the Maybe datatype is:data Maybe (a : ?) = Nothing | Just a;def maybeInst : Functor Maybe =Func Maybe (l a : ?. l b : ?. l f : a ! b. l x : Maybe a.
case x ofNothing ) Nothing b| Just (z : a) ) Just b (f z));After the translation process, the Functor record is desugared into a datatype with only one
data constructor (Func) that has type:(f : ? ! ?) ! (a : ?) ! (b : ?) ! (a ! b) ! f a ! f b
Since Maybe has kind ? ! ?, it is legal to apply Func to Maybe.
Datatype Promotion. Recent versions of Haskell introduced datatype promotion (Yorgey
et al., 2012), in order to allow ordinary datatypes as kinds, and data constructors as types.
With the power of unified syntax, data promotion is made trivial in Fun. We show arepresentation of a labeled binary tree, where each node is labeled with its depth in thetree. Below is the definition:
data Nat = Z | S Nat;data PTree (n : Nat) = Empty | Fork (z : Int) (x : PTree (S n)) (y : PTree (S n));Notice how the datatype Nat is “promoted” to be used at the kind level in the definition of
PTree. Next we can construct a binary tree that keeps track of its depth statically:
Fork Z 1 (Empty (S Z)) (Empty (S Z))
If we accidentally write the wrong depth, for example:
Fork Z 1 (Empty (S Z)) (Empty Z)
The above will fail to pass type checking.
The PTree example can also be viewed as a dependent variant of nested datatypes (Bird& Meertens, 1998). For example, Nest is a non-dependent nested datatype as follows(written in Haskell):

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

13

data Nest a = NilN | ConsN a (Nest (a, a))where ConsN contains a parameter with type Nest (a, a) that varies from Nest a. This issimilar to Fork that contains a parameter of type PTree (S n). Notice that nested datatypes
are supported in Haskell 98. Pattern matching for nested datatypes in Haskell alreadyworked before GADTs were added to Haskell. In other words, such restricted subset of
non-uniform types (i.e. nested datatypes) do not require the use of equality during patternmatching (unlike the more general case of GADTs).
Higher-order Abstract Syntax. Higher-order abstract syntax (Pfenning & Elliott, 1988)(HOAS) is a representation of abstract syntax where the function space of the meta-language
is used to encode the binders of the object language. We show an example of encoding asimple lambda calculus:
data Exp = Num Int| Lam (Exp ! Exp)| App Exp Exp;
Note that in the lambda constructor (Lam), the recursive occurrence of Exp appears in anegative position (i.e. in the left side of a function arrow). Systems like Coq (The Coq
development team, 2016) and Agda (Norell, 2007) would reject such programs since it iswell-known that such datatypes can lead to logical inconsistency. Moreover, such logicalinconsistency can be exploited to write non-terminating computations, and make typechecking undecidable. In contrast, Fun is able to express HOAS in a straightforward way,while preserving decidable type checking.
Using Exp we can write an evaluator for the lambda calculus. As noted by Fegaras andSheard (1996), the evaluation function needs an extra function (reify) to invert the resultof evaluation. The code for the evaluator is shown next (we omit most of the unsurprisingcases; text after “--” are comments):
data Value = VI Int | VF (Value ! Value);data Eval = Ev { eval0 : Exp ! Value, reify0 : Value ! Exp};
defrec ev : Eval =Ev (l e : Exp. case e of ... -- excerpted| Lam fun ) VF (l e0 : Value. eval0 ev (fun (reify0 ev e0 )))(l v : Value. case v of ... -- excerpted| VF fun ) Lam (l e0 : Exp. reify0 ev (fun (eval0 ev e0 )));
def eval : Exp ! Value = eval0 ev;
The definition of the evaluator is mostly straightforward. Here we create a record Eval,
inside which are two name fields eval0 and reify0 . Similarly to the record syntax of Haskell,both eval0 and reify0 are also functions for projections of fields. The eval0 function isconventional, dealing with each possible shape of an expression. The tricky part lies inthe evaluation of a lambda abstraction, where we need a second function, called reify0 , oftype Value ! Exp that lifts values into terms. Thanks to the flexibility of the µ primitive,
mutual recursion can be encoded by using records.
Evaluation of a lambda expression proceeds as follows:

ZU064-05-FPR

main

14

23 September 2019

10:36

Y. Yang and B. Oliveira
def show = l v : Value. case v of VI n ) n;
def expr = App (Lam (l f : Exp. App f (Num 42))) (Lam (l g : Exp. g));show (eval expr) -- returns 42

3.3 Object Encodings
Casts are useful for modeling examples other than algebraic datatypes. For example, we
can model a simple form of object encodings with call-by-name cast operators (Yang &Oliveira, 2017). We present an example of existential object encodings (Pierce & Turner,
1994) in Fun, which originally requires System Fw . First, we encode the existential typeand its constructor in Fun by a standard Church encoding (Pierce, 2002) using the universal
type (i.e. P-type):def Ex = l P : ? ! ?. (z : ?) ! ((x : ?) ! P x ! z) ! z;
def pack = l P : ? ! ?. l e1 : ?. l e2 : P e1 .
cast" [Ex P] (l z : ?. l f : (x : ?) ! P x ! z. f e1 e2 );where pack is the constructor to build an existential package. Thus, we can encode an
existential type 9x. A as Ex (l x : ?. A) in Fun. The object type operator Obj can be encoded
as follows:data Pair (A : ?) (B : ?) = MkPair {fst : A, snd : B};
def Obj = l I : ? ! ?. Ex (l X : ?. Pair X (X ! I X));
where Pair A B encodes the pair type A⇥B. In the definition of Obj, the binder I denotes theinterface. The body is an existential type which packs a pair. The pair consists of a hidden
state (with type X) and methods which are functions depending on the state (with type
X ! I X). For a concrete example of objects, we use the interface of cell objects (Bruce
et al., 1999):
data Cell (X : ?) = MkCell {get : Int, set : Int ! X, bump : X };The interface indicates that a cell object consists of three methods: a getter get to return thecurrent state, a setter set to return a new cell with a given state, and bump to return a newcell with the state increased by one.
We can define a cell object c as follows:data Var = MkVar {getVar : Int };def CellT = l X : ?. Pair X (X ! Cell X);
def pair = MkPair Var (Var ! Cell Var)
(MkVar 0)-- Initial state(l s : Var. MkCell Var -- Methods(getVar s)-- Method get(l n : Int.MkVar n)-- Method set(MkVar (getVar s + 1))); -- Method bump
def p
def c

= pack CellT Var (cast" [CellT Var ] pair);= cast" [Obj Cell] p;

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

15

The body of object c is an existential package p of type 9X.Pair X (X ! Cell X) built
by the pack operator. The first parameter of pack is CellT that represents the body of theexistential type. The second parameter is the integer variable type Var which corresponds
to the existential binder X. The third parameter has type CellT Var which can be reduced
to a pair type Var ⇥ (Var ! Cell Var) which is defined in the definition pair constructedby MkPair. The first component of the pair is the initial hidden state MkVar 0. The second
component is a function containing three methods that are defined in a record by MkCell
and abstracted by the state variable s. The definition of the three methods follows the cellobject interface Cell.
Note that we have two cast" operators here: one over the existential package p andanother over the pair. Due to the lack of a conversion rule in PITS, the desired type of theobject c (i.e. Obj Cell) is an application, which is different from the type of the existential
package (i.e. Ex CellT). Noticing that
Obj Cell ,! Ex (l X : ?. Pair X (X ! Cell X)) = Ex CellT
We can use cast" to do one-step type expansion for the package. Similarly, the second
cast" operator used in the third parameter of pack converts the pair type into CellT Var.
We emphasize that the object encoding example exploits fundamental features of PITS,
namely higher-kinded types, higher-order polymorphism and explicit casts. The absenceof a conversion rule does not prevent the object encoding because the required type-levelcomputation is recovered by explicit casts.
3.4 Fun with Full Reduction
So far all the examples can be encoded in Fun with casts using weak-head reduction.
However for some applications full reduction is needed at the type level. In this subsection
particularly, we show one such application. For brevity, we move types of arguments indef bindings to top-level annotations without repeating them in l -binders, e.g., we change
def f = l x : Int. 1 into
def f : Int ! Int = l x. 1
Leibniz Equality, Kind Polymorphism and Vectors. One interesting type-level featureof GHC Haskell is generalized algebraic datatypes, or GADTs (Xi et al., 2003; Cheney &Hinze, 2003; Peyton Jones et al., 2004). GADTs require a non-trivial form of explicit typeequality, which is built in Haskell’s core language (System FC (Sulzmann et al., 2007)),
called a coercion. PITS does not have such built-in equality. However a form of equality
can be encoded using Leibniz Equality (Cheney & Hinze, 2002):
data Eq (k : ?) (a : k) (b : k) =Proof {subst : (f : k ! ?) ! f a ! f b};
Note that the definition uses kind polymorphism: the kind of types a and b is k, which ispolymorphic and not limited to ?. For brevity, we use a ⌘ b to denote Eq k a b by omitting
the kind k. Then we can encode a GADT, for example, length-indexed list (or vector) as
follows:

ZU064-05-FPR

main

23 September 2019

16

10:36

Y. Yang and B. Oliveiradata Vec (a : ?) (n : Nat) =Nil (Eq Nat n Z)
| Cons (m : Nat) (Eq Nat n (S m)) a (Vec a m);

However, it is difficult to use such encoding approach to express the injectivity of constructors (Cheney & Hinze, 2003), e.g., deducing n ⌘ m from S n ⌘ S m. It would be challenging
to encode the tail function of a vector:
def tail : (a : ?) ! (n : Nat) ! (v : Vec a (S n)) ! Vec a n =l a. l n. l v. case v ofCons m p x xs ) xs; -- ill-typed
The case expression above is ill-typed: xs has the type Vec a m, but the function requires
the case branch to return Vec a n. To convert xs to the correct type, we need to show n ⌘ m.
But the equality proof p has type Eq Nat (S n) (S m), i.e., S n ⌘ S m. Thus, the injectivityof constructor S is needed.
Fun incorporates two full cast operators (cast* and cast+ ) from full PITS. With thepower of full casts, we can “prove” the injectivity of S. We first define a partial function
predNat to destruct S:
def predNat : Nat ! Nat =l n. case n of S m ) m;
Given S n ⌘ S m, by congruence of equality, it is trivial to show predNat (S n) ⌘ predNat (S m).
Noticing the reduction predNat (S n) ,! n holds, we can use a full cast operator cast+ to
reduce both sides of the equality to obtain n ⌘ m:
def injNat : (n : Nat) ! (m : Nat) ! Eq Nat (S n) (S m) ! Eq Nat n m =l n. l m. l p. cast+ (lift Nat Nat (S n) (S m) predNat p);
The auxiliary function “lift”2 lifts the type of equality proof p from S n ⌘ S m to predNat (S n) ⌘predNat (S m). Then cast+ converts it to Eq Nat n m (type annotations are omitted forbrevity):p:S n ⌘ S mlift predNat p: predNat (S n) ⌘ predNat (S m)cast+ (lift predNat p) : n ⌘ m
Now we can write a well-typed version of tail:def castVec : (a : ?) ! (n : Nat) ! (m : Nat) !
Eq Nat n m ! Vec a m ! Vec a n =l a. l n. l m. l p. to (Vec a n) (Vec a m) (lift Nat ? n m (Vec a) p);
def tail : (a : ?) ! (n : Nat) ! (v : Vec a (S n)) ! Vec a n =l a. l n. l v. case v ofCons m p x xs ) castVec a n m (injNat n m p) xs;
2

The definition of lift is omitted and available from online materials.

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

17

We use injNat to obtain a proof n ⌘ m from S n ⌘ S m. Finally, we call an auxiliary
function castVec that uses the proof n ⌘ m to convert xs from Vec a m to Vec a n. The
definition of castVec relies on another auxiliary function “to”3 that unfolds the Leibniz
equality Vec a n ⌘ Vec a m, lifted from n ⌘ m, to a function with type Vec a m ! Vec a n.
Note that Fun is not logically consistent and does not check whether the proof is terminating. Nonetheless, we can manually ensure that the injectivity proof injNat used intail is valid. There are no recursive terms in injNat, which could be bogus proofs. Though
predNat is a partial function, it is always applied to numbers with the form S n and nevergoes to the invalid branch. Finally, while this encoding deals with injectivity, an encodingof equality still has a computational cost. Therefore, a motivation to natively support
equality constraints instead (as done for example in Haskell (Sulzmann et al., 2007)) is
to have equality without any computational costs, since equality constraints can simply beerased.
4 Call-by-name Pure Iso-Type Systems
We formally present the first variant of Pure Iso-Type Systems. PITS is very close to Pure
Type Systems (PTS) (Barendregt, 1992), except for two key differences: the existence of
cast operators and general recursion. In this section, we focus on the call-by-name variantof PITS, which uses a call-by-name weak-head reduction strategy in casts. We show typesafety for any PITS and decidability of type checking for a particular subset, i.e., functional
PITS (see Definition 4.1). One important remark is that the dynamic semantics of callby-name PITS is given by a direct small-step operational semantics, and type-safety isproved using the usual preservation and progress theorems. Full proofs of the metatheory
are mechanized in Coq and can be found in the online repository.
4.1 Syntax
Fig. 1 shows the syntax of PITS, including expressions, values and contexts. Like Pure
Type Systems (PTS), PITS uses a unified representation for different syntactic levels. Thereis no syntactic distinction between terms, types or kinds/sorts. Such unified syntax brings
economy for type checking, since one set of typing rules can cover all syntactic levels. As
in PTS, PITS contains a set of constants called Sorts, e.g., ?, 2, denoted by metavariable s.
By convention, we use metavariables A, B, etc. for an expression on the type-level positionand e for one on the term level. We use A ! B as a syntactic sugar for Px : A. B if x does
not occur free in B.
Cast Operators. We introduce two new primitives cast" and cast# (pronounced as “castup” and “cast down”) to replace the implicit conversion rule of PTS with one-step explicit
type conversions. The cast operators perform two directions of conversion: cast# is for the
one-step reduction of types, and cast" is for the one-step expansion. The cast" constructneeds a type annotation A as the result type of one-step expansion for disambiguation,
3

The definition of to is omitted and available from online materials.

ZU064-05-FPR

main

23 September 2019

18

10:36

Y. Yang and B. Oliveira
Expressionse, A, B ::= x | s | e1 e2 | l x : A. e | Px : A. B
| µx : A. e | cast" [A] e | cast# ev ::= s | l x : A. e | Px : A. B | cast" [A] e
G ::= ? | G, x : A

ValuesContexts
Syntactic Sugar
A!B, Px : A. B
where x 62 FV(B)castn" [A1 ] e , cast" [A1 ](cast" [A2 ](. . . (cast" [An ] e) . . .))where A1 ,! A2 ,! . . . ,! An
castn# e, cast# (cast# (. . . (cast# e) . . .))
|
{z
}
n

Fig. 1. Syntax of call-by-name PITS

while cast# does not, since the result type of one-step reduction can be uniquely determinedas discussed in Section 4.5.
We use syntactic sugar castn" and castn# to denote n consecutive cast operators (see Fig.
1). Alternatively, one can introduce them as built-in operators and treat one-step casts
as syntactic sugar instead. Though using built-in n-step casts can reduce the number ofindividual cast constructs, we do not adopt such alternative design in order to simplify the
discussion of metatheory. Note that castn" is simplified to take just one type parameter, i.e.,
the last type A1 of the n cast operations. Due to the determinacy of one-step reduction (seeLemma 4.2), the intermediate types can be uniquely determined and left out.
General Recursion. We use the µ-operator to uniformly represent recursive terms andtypes. The expression µx : A. e can be used on the type level as a recursive type, or on termlevel as a fixpoint that is possibly non-terminating. For example, A can be a single sort s,as well as a function type such as Int ! Int or s1 ! s2 .
4.2 Operational Semantics
Fig. 2 shows the small-step, call-by-name operational semantics. Three base cases include
rule R-B ETA for beta reduction, rule R-M U for recursion unrolling and rule R-C AST E LIM
for cast canceling. Two inductive cases, rule R-A PP and rule R-C ASTDN, define reduction
at the head position of an application, and the inner expression of cast# terms, respectively.
Note that rule R-C AST E LIM and rule R-C ASTDN do not overlap because in the former
rule, the inner term of cast# is a value (see Fig. 1), i.e., cast" [A] e. In rule R-C ASTDN, theinner term is reducible and cannot be a value.
The reduction rules are called weak-head since only the head term of an application canbe reduced, as indicated by the rule R-A PP. Reduction is also not allowed inside the l term and P-term which are both defined as values. To remove such restrictions, we need
the parallel reduction, as will be discussed in Section 6. Weak-head reduction rules areused for both type conversion and term evaluation. To evaluate the value of a term-level
expression, we apply the one-step (weak-head) reduction multiple times, i.e., multi-step
reduction, the transitive and reflexive closure of the one-step reduction.

ZU064-05-FPR

main

23 September 2019

10:36

19

Pure Iso-Type Systems
e1 ,! e2(Call-by-name Reduction)
R-A PPR-B ETA

R-M U

e1 ,! e01

e1 e2 ,! e01 e2(l x : A. e1 ) e2 ,! e1 [x 7! e2 ]R-C ASTDNµx : A. e ,! e[x 7! µx : A. e]

R-C AST E LIM

e ,! e00

cast# e ,! cast# e

cast# (cast" [A] e) ,! eFig. 2. Operational semantics of call-by-name PITS
G`e:A

(Typing of Call-by-name PITS)
T-A BS

T-A X

`G

T-VAR

`G

(s1 , s2 ) 2 A

G ` s1 : s2

G ` A : s1
G, x : A ` B : s2

x:A 2 G

G`x:A

G, x : A ` e : B(s1 , s2 , s3 ) 2 R

G ` l x : A. e : Px : A. B

T-P ROD
T-A PPG ` e1 : Px : A. B

G ` A : s1
G, x : A ` B : s2
(s1 , s2 , s3 ) 2 R

G ` e2 : A

G ` e1 e2 : B[x 7! e2 ]

T-M U

G`A:s

G, x : A ` e : A

G ` µx : A. e : A`GG ` Px : A. B : s3

T-C ASTUP

G`B:s

G`e:A

B ,! AG ` cast" [B] e : B

T-C ASTDN

G`e:A

A ,! BG ` cast# e : B(Well-formedness)

W-N IL`?

W-C ONSG`A:sx fresh in G

` G, x : A

Fig. 3. Typing rules of call-by-name PITS
4.3 Typing
Fig. 3 gives the syntax-directed typing rules of PITS, including rules of context wellformedness ` G and expression typing G ` e : A. Note that there is only a single set of rules
for expression typing, as there is no distinction of different syntactic levels. Most typing
rules are quite standard. We write ` G if a context G is well-formed. We use G ` A : s tocheck if A is a well-formed type.
PITS is a family of type systems similarly to PTS, parametrized by the axiom set A ⇢(Sorts ⇥ Sorts) for typing sorts and rule set R ⇢ (Sorts ⇥ Sorts ⇥ Sorts) for checking
well-formedness of P-types. Rule T-A X checks whether sort s1 can be typed by sort s2
if (s1 , s2 ) 2 A holds. Rule T-VAR checks the type of variable x from the valid context.
Rule T-A PP and rule T-A BS check the validity of application and abstraction respectively.
Rule T-P ROD checks the type well-formedness of the dependent function type by checking

ZU064-05-FPR

main

23 September 2019

10:36

20

Y. Yang and B. Oliveiraif (s1 , s2 , s3 ) 2 R. Rule T-M U checks the validity of a recursive term. It ensures that therecursion µx : A. e should have the same type A as the binder x and also the inner term e.
The Cast Rules. We focus on the rule T-C ASTUP and rule T-C ASTDN that define thesemantics of cast operators and replace the conversion rule of PTS. The relation between
the original and converted type is defined by one-step call-by-name reduction (see Fig.
2). For example, given a judgment G ` e : A2 and relation A1 ,! A2 ,! A3 , cast" [A1 ] e
expands the type of e from A2 to A1 , while cast# e reduces the type of e from A2 to A3 . We
can formally give the typing derivations of the examples in Section 2.3:
G ` e : (l x : ?. x) Int(l x : ?. x) Int ,! IntG ` 3 : IntG ` (l x : ?. x) Int : ?
(l x : ?. x) Int ,! IntG ` (cast# e) : IntG ` (cast" [(l x : ?. x) Int] 3) : (l x : ?. x) Int

Importantly, in PITS term-level and type-level computation are treated differently. Termlevel computation is dealt in the usual way, by using multi-step reduction until a value isfinally obtained. Type-level computation, on the other hand, is controlled by the program:each step of the computation is induced by a cast. If a type-level program requires n stepsof computation to reach the normal form, then it will require n casts to compute a type-levelvalue.
Syntactic Equality. Finally, the definition of type equality in PITS differs from PTS.
Without the conversion rule, the type of a term in PITS cannot be converted freely against
beta equality, unless using cast operators. Thus, types of expressions are equal only if they
are syntactically equal (up to alpha renaming).
4.4 The Two Faces of Recursion
One key difference from PTS is that PITS supports general recursion for both terms andtypes. We discuss general recursion on two levels and show how iso-types generalize isorecursive types.
Term-level Recursion. In PITS, the µ-operator works as a fixpoint on the term level. By
rule R-M U, evaluating a term µx : A. e will substitute all x’s in e with the whole µ-term
itself, resulting in the unrolling e[x 7! µx : A. e]. The µ-term is equivalent to a recursivefunction that should be allowed to unroll without restriction.
Recall the factorial function example in Section 2.4. By rule T-M U, the type of fact
is Int ! Int. Thus we can apply fact to an integer. Note that by rule R-M U, fact will be
unrolled to a l -term. Assuming the evaluation of if-then-else construct and arithmetic
expressions follows the one-step reduction, we can evaluate the term fact 3 as follows:
,!
,!
,!

fact 3(l x : Int. if x == 0 then 1 else x ⇥ fact (xif 3 == 0 then 1 else 3 ⇥ fact (3 1). . . ,! 61)) 3-- by rule R-A PP-- by rule R-B ETA

Note that we never check if a µ-term can terminate or not, which is an undecidable
problem for general recursive terms. The factorial function example above can stop, while

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

21

there exist some terms that will loop forever. However, term-level non-termination is only aruntime concern and does not block the type checker. In Section 4.5 we show type checking
PITS is still decidable in the presence of general recursion.
Type-level Recursion. On the type level, µx : A. e works as an iso-recursive type (Craryet al., 1999), a kind of recursive type that is not equal but only isomorphic to its unrolling.
Normally, we need to add two more primitives fold and unfold for the iso-recursive typeto map back and forth between the original and unrolled form. Assuming that there exist
expressions e1 and e2 such that e1 : µx : A. B and e2 : B[x 7! µx : A. B], we have thefollowing typing results:: B[x 7! µx : A. B]: µx : A. B

unfold e1
fold [µx : A. B] e2

by applying standard typing rules of iso-recursive types (Pierce, 2002):
G ` e1 : µx : A. B

G ` unfold e1 : B[x 7! µx : A. B]

G ` µx : A. B : s
G ` e2 : B[x 7! µx : A. B]

G ` fold [µx : A. B]e2 : µx : A. B

We have the following relation between types of e1 and e2 witnessed by fold and unfold:µx : A. B )unfold* B[x 7! µx : A. B]

fold [µx:A. B]

In PITS, we do not need to introduce fold and unfold operators, because with the rule RM U, cast" and cast# generalize fold and unfold, respectively. Consider the same expressions e1 and e2 above. The type of e2 is the unrolling of e1 ’s type, which follows theone-step reduction relation by rule R-M U:µx : A. B ,! B[x 7! µx : A. B]
By applying rule T-C AST U P and rule T-C ASTDN, we can obtain the following typing
results:
cast# e1
: B[x 7! µx : A. B]
cast" [µx : A. B] e2 : µx : A. B

Thus, cast" and cast# witness the isomorphism between the original recursive type and its
unrolling, behaving in the same way as fold and unfold in iso-recursive types.
µx : A. B )cast#* B[x 7! µx : A. B]

cast" [µx:A. B]

An important remark is that casts are necessary, not only for controlling the unrolling ofrecursive types, but also for type conversion of other constructs, which is essential for
encoding parametrized algebraic datatypes (see Section 3.1).
4.5 Metatheory of Call-by-name PITS
We now discuss the metatheory of call-by-name PITS. We focus on two properties: thedecidability of type checking and the type safety of the language. Firstly, we show that

ZU064-05-FPR

main

23 September 2019

22

10:36

Y. Yang and B. Oliveira

type checking for a functional subset (Siles & Herbelin, 2012) of PITS is decidable without requiring strong normalization. Secondly, any PITS is type-safe, proven by subject
reduction and progress lemmas (Wright & Felleisen, 1994).
Decidability of Type Checking for Functional PITS. We limit the discussion in thisparagraph to a subclass of PITS, functional PITS:
Definition 4.1
A PITS is functional if:
1. for all s1 , s2 , s02 , if (s1 , s2 ) 2 A and (s1 , s02 ) 2 A , then s2 ⌘ s02 .
2. for all s1 , s2 , s3 , s03 , if (s1 , s2 , s3 ) 2 R and (s1 , s2 , s03 ) 2 R, then s3 ⌘ s03 .
Such definition is similar to the one of functional PTS (Siles & Herbelin, 2012), or singlysorted PTS (Barendregt, 1992). Functional PITS enjoys uniqueness of typing, i.e., typing
result is unique up to alpha equality:
Lemma 4.1 (Uniqueness of Typing for Functional PITS)
In any functional PITS, if G ` e : A and G ` e : B, then A ⌘ B.
For simplicity reasons, we only discuss decidability for functional PITS, where the proof
can be significantly simplified by the uniqueness of typing lemma. For non-functional
PITS, one may follow the proof strategy similarly used in non-functional PTS (van Benthem Jutting, 1993), by proving the “Uniqueness of Domains” lemma instead. We leave
the decidability proof for non-functional PITS as future work.
For functional PITS, the proof for decidability of type checking is by induction on the
structure of e. The non-trivial case is for cast-terms with typing rule T-C AST U P and rule TC ASTDN. Both rules contain a premise that needs to judge if two types A and B follow the
one-step reduction, i.e., if A ,! B holds. We show that B is unique with respect to the onestep reduction, or equivalently, reducing A by one step will get only a sole result B. Suchproperty is given by the following lemma:
Lemma 4.2 (Determinacy of One-step Call-by-name Reduction)
If e ,! e1 and e ,! e2 , then e1 ⌘ e2 .
We use the notation ⌘ to denote the alpha equivalence of e1 and e2 . Note that the presenceof recursion does not affect this lemma: given a recursive term µx : A. e, by rule R-M U,
there always exists a unique term e0 ⌘ e[x 7! µx : A. e] such that µx : A. e ,! e0 . With thisresult, we show that it is decidable to check whether the one-step relation A ,! B holds.
We first reduce A by one step to obtain A0 (which is unique by Lemma 4.2), and compare
if A0 and B are syntactically equal. Thus, we can further show type checking cast-terms is
decidable.
By the definition of functional PITS, checking the type of sorts and well-formedness of
P-types are decidable. For other cases, type checking is decidable by the induction hypothesis and uniqueness of typing (see Lemma 4.1). Thus, we can conclude the decidability oftype checking:
Theorem 4.1 (Decidability of Type Checking for Functional PITS)

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

23

In any functional PITS, given a well-formed context G and a term e, it is decidable todetermine if there exists A such that G ` e : A.
We emphasize that when proving the decidability of type checking, we do not rely onstrong normalization. Intuitively, explicit type conversion rules use one-step call-by-namereduction, which already has a decidable checking algorithm according to Lemma 4.2. We
do not need to further require the normalization of terms. This is different from the proof
for PTS which requires the language to be strongly normalizing (van Benthem Jutting,1993). In PTS the conversion rule needs to examine the beta equivalence of terms, which
is decidable only if every term has a normal form.
Type Safety for all PITS. Type safety holds for any PITS, not just functional PITS. The
proof of the type safety is by showing subject reduction and progress lemmas (Wright &Felleisen, 1994):
Theorem 4.2 (Subject Reduction of Call-by-name PITS)
If G ` e : A and e ,! e0 then G ` e0 : A.
Theorem 4.3 (Progress of Call-by-name PITS)
If ? ` e : A then either e is a value v or there exists e0 such that e ,! e0 .

The proof of subject reduction is straightforward by induction on the derivation of G ` e : A
and inversion of e ,! e0 . Some cases need supporting lemmas: rule R-C AST E LIM requires
Lemma 4.2; rule R-B ETA and rule R-M U require the following substitution lemma:
Lemma 4.3 (Substitution of Call-by-name PITS)
If G1 , x : B, G2 ` e1 : A and G1 ` e2 : B, then G1 , G2 [x 7! e2 ] ` e1 [x 7! e2 ] : A[x 7! e2 ].
The proof of progress is also standard by induction on ? ` e : A. Notice that cast" [A] e
is a value, while cast# e1 is not: by rule R-C ASTDN, e1 will be constantly reduced until it
becomes a value that could only be in the form cast" [A] e by typing rule T-C ASTDN. Thenrule R-C AST E LIM can be further applied and the evaluation does not get stuck. Anothernotable remark is that when proving the case for application e1 e2 , if e1 is a value, it could
only be a l -term but not a cast" -term. Otherwise, suppose e1 has the form cast" [Px :A. B] e01 . By inversion, we have ? ` e01 : A0 and Px : A. B ,! A0 . But such A0 does not exist
because Px : A. B is a value which is not reducible.
5 Call-by-value Pure Iso-Type Systems
Pure Iso-Type Systems enjoy the flexibility of choosing different reduction rules for typeconversion or term evaluation. In this section, we present another variant of PITS whichuses call-by-value reduction, a more commonly used reduction strategy. All metatheory
presented in Section 4, including type safety and decidability of typing, still holds for thisvariant. Call-by-value is interesting because, for applications, the arguments are reduced
before beta reduction. Such reduction is problematic for dependent functions types in asetting with iso-types, since it may endanger type safety. We address this problem by using
a form of value restriction, inspired by previous work (Swamy et al., 2011; Sjöberg et al.,2012). Full proofs are mechanized in Coq and can be found in the online repository.

ZU064-05-FPR

main

23 September 2019

24

10:36

Y. Yang and B. Oliveira
5.1 Value Restriction

Call-by-value reduction (,!v ) requires the argument of beta reduction to be a value (v).
A typical leftmost reduction strategy of an application is that, one first reduces the function part to a value, then further reduces the argument. Such process is witnessed by thefollowing reduction rules:
RV-B ETA

RV-A PP L

RV-A PP Re1 e2 ,!v e01 e2

v e ,!v v e0

e1 ,!v e01(l x : A. e) v ,!v e[x 7! v]

e ,!v e0

A function in PITS can be dependent. That is the function type can depend on theargument. For example, suppose that f is a dependent function generating a length-indexed
list with given length n, with the following type:f : (Pn : Int.Vec n)
By rule RV-A PP R, the reduction f (1 + 1) ,!v f 2 holds. However, the types of two sidesof the reduction are different:f (1 + 1) : Vec (1 + 1)
f2
: Vec 2
Notice that PITS does not contain an implicit conversion rule. Without an explicit typeconversion, subject reduction does not hold. There are at least two possible ways to deal
with this issue: 1) introducing a type cast for reduction; 2) requiring the dependent function
to be applied to a value only. For simplicity reasons, we choose the second method: avalue restriction. The first method entangles types with reduction, which makes the semantics more complicated. The value restriction is also used by several existing call-byvalue calculi to ensure type safety or simplify the design, e.g., by Zombie (Sjöberg et al.,2012; Casinghino et al., 2014) to prevent bogus proofs that are non-terminating, and by
DOT (Amin et al., 2012; Amin et al., 2016), a core language of Scala (Odersky et al.,2004), to simplify the formalization of path-dependent types (Amin et al., 2014).
Typing Rules with Value Restriction. Now we have two typing rules for the function
application:
TV-A PP V

G `v e : Px : A. B

G `v v : A

G `v e v : B[x 7! v]

TV-A PPG `v e1 : A ! B

G `v e2 : A

G `v e1 e2 : B

If a function is dependent the argument must be a value (v). Otherwise, the function is nondependent and there is no restriction on its argument. Recall that the arrow type is syntactic
sugar for the non-dependent P-type (see Fig. 1). Note that these two typing rules overlap:
the P-type of e in rule TV-A PP V could be non-dependent. In such case, B = B[x 7! v] andrule TV-A PP V has the same typing result as rule TV-A PP. Thus, such overlapping does
not cause any determinacy issues.

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

25

Two Sides of Value Restriction. Imposing such value restriction in PITS has both pros
and cons. On one side, type-safety proofs are quite simple (see Section 5.3). We can safely
rule out the case that breaks type preservation when reducing the argument of a dependentfunction application. Recalling the example above, a reduction like f (1 + 1) ,!v f 2 is notpossible since f (1 + 1) will be rejected by the type system in the first place. The argument(1 + 1) of the dependent function f is not a value, so f (1 + 1) is not a well-typed term.
Thus, if a function is applied to a reducible argument it must be a non-dependent functionin order to ensure type preservation.
Though users can easily write f 2 as a workaround to satisfy the type system insteadof f (1 + 1), there is no alternative way to express terms such as f (x + y) where theargument cannot be reduced to a value. Thus, the value restriction makes the type system
more restrictive on dependent function applications — users can only provide values but
not arbitrary arguments to dependent functions. Nonetheless, there is no restriction on
applying non-dependent functions to arguments, e.g., id (x + y) where id = l z : Int. z.
In other words, there is no loss of expressiveness with respect to non-dependently typed
programming. One nice aspect of call-by-value casts is that they can be erased after typechecking (i.e. computational irrelevance, see Section 7.1).
Also, the value restriction does not make call-by-value PITS necessarily less expressive
than call-by-name PITS. Though dependent applications such as f (1 + 1) can be written
in call-by-name PITS, the argument (1 + 1) may never be reduced and is always kept as
is. Thus, one may not be able to prove equality between f (1 + 1) and f 2 in call-by-name
PITS. On the other hand, one can reduce id (1 + 1) to id 2 in call-by-value PITS but not incall-by-name PITS.
Alternative to the Value Restriction. Instead of the value restriction, one could simultaneously add casts when reducing dependent function applications. Supposing we drop thevalue restriction, for the same example of f , noticing that Vec (1 + 1) ,!v Vec 2, we canobtainf2: Vec 2cast" [Vec (1 + 1)]( f 2) : Vec (1 + 1)
Then, f (1 + 1) ,!v cast" [Vec (1 + 1)]( f 2) preserves the type with an extra cast" . However,such reduction relation involves types due to the annotation of casts. Moreover, call-byvalue casts may not be expressive enough for certain type conversions, such as conversions
inside binders. Parallel reduction and full casts may be required, as will be discussed in
Section 6. For simplicity reasons, we leave this extension as future work and stick to value
restriction for a simpler meta-theory.
5.2 Reduction with Open Terms
In call-by-value PITS, cast operators also use one-step call-by-value reduction to perform
type conversions. Open terms that contain free variables may occur during reduction, e.g.,(l x : Int. x) y, where y is a free variable. Using the rule RV-B ETA, the reduction can only be
performed if y is a value. To allow beta reduction of such open terms, we allow variables
as values. Traditional call-by-value calculi do not have such definitions, since reduction

ZU064-05-FPR

main

26

23 September 2019

10:36

Y. Yang and B. Oliveira

is used for term evaluation but not type conversion. Nevertheless, several call-by-value
calculi that involve type conversion allow treating variables as values, such as several open
call-by-value calculi (Accattoli & Guerrieri, 2016) (including Fireball Calculus (Paolini &Della Rocca, 1999)) and Zombie (Sjöberg et al., 2012; Casinghino et al., 2014). To makesuch definition work, we need to ensure that a variable is substituted with a value. The
rule RV-B ETA already ensures such requirement.
Recursion and Recursive Types. For a recursive term µx : A. e, its unrolling has the forme[x 7! µx : A. e] such that the substituted term is the term itself. Thus, we need to treat µterms as values as in traditional call-by-value settings. One consequence is that a µ-term
now is only unrolled when it is placed at the function part of an application, or inside cast# :RV-M U

RV-C ASTDN -M U(µx : A. e) v ,!v (e[x 7! µx : A. e]) v

cast# (µx : A. e) ,!v cast# (e[x 7! µx : A. e])Thus, µ-terms only represents term-level recursive functions, as in most call-by-value
languages. They cannot directly represent recursive types at the same time. This is different
from the call-by-name PITS where µ-terms are both term-level fixpoints and recursive
types, since substituted terms are not necessarily values. Nevertheless, one can still recoverrecursive types in call-by-value PITS by feeding the type-level recursive function a dummy
argument, e.g., the unit value ():PITS Variant Recursive Type
Reduction
Call-by-name f = µy : A. e
f ,! e[y 7! f ]Call-by-value f 0 = µx : Unit ! A. e[y 7! x ()] f 0 () ,!v (e[y 7! x ()][x 7! f 0 ]) ()where x does not occur free in e. The recursive type f in call-by-name PITS can be
simulated by a type-level recursive function f 0 applied to a dummy argument, i.e., f 0 ().
Finally, we show the full definition of call-by-value PITS in Fig. 4. The changes fromthe call-by-name variant are highlighted.
5.3 Metatheory
All the metatheory of call-by-name PITS still holds in the call-by-value variant, including
two key properties: type safety and decidability of type checking. The proofs are almost
the same. The only relevant change is the statement of the substitution lemma:
Lemma 5.1 (Substitution of Call-by-value PITS)
If G1 , x : B, G2 `v e : A and G1 `v v : B, then G1 , G2 [x 7! v] `v e[x 7! v] : A[x 7! v].

We now require substituted terms to be values. With such a change, type preservation of
reducing open terms is possible, as discussed in Section 5.2. Such restricted substitution
lemma is sufficient for proving subject reduction, because all substituted terms are values
in reduction rules (see Fig. 4). The subject reduction and progress lemmas can be provedin a similar way to call-by-name PITS:
Theorem 5.1 (Subject Reduction of Call-by-value PITS)
If G `v e : A and e ,!v e0 then G `v e0 : A.

ZU064-05-FPR

main

23 September 2019

10:36

27

Pure Iso-Type Systems(Syntax)
Expressions
ValuesContexts

e, A, B ::= x | s | e1 e2 | l x : A. e | Px : A. B | µx : A. e | cast" [A] e | cast# ev ::= x | s | l x : A. e | Px : A. B | µx : A. e | cast" [A] v
G ::= ? | G, x : A

e1 ,!v e2(Call-by-value Reduction)
RV-A PP L

RV-B ETA

RV-M U(l x : A. e) v ,!v e[x 7! v ](µx : A. e) v ,!v (e[x 7! µx : A. e]) v

RV-A PP R

RV-C ASTUP

e ,!v e0v e ,!v v e0

e1 ,!v e01
e1 e2 ,!v e01 e2

RV-C ASTDN

e ,!v e0cast" [A] e ,!v cast" [A] e0

e ,!v e0
cast# e ,!v cast# e0

RV-C ASTDN -M U

RV-C AST E LIM

cast# ( µx : A. e ) ,!v cast# ( e[x 7! µx : A. e] )cast# (cast" [A] v ) ,!v v

G `v e : A(Typing of Call-by-value PITS)
TV-A BSTV-A X`v G

G `v A : s1
G, x : A `v e : B
G, x : A `v B : s2
(s1 , s2 , s3 ) 2 R
G `v l x : A. e : Px : A. B

TV-VAR`v G
x:A 2 GG `v x : A(s1 , s2 ) 2 A
G `v s1 : s2
TV-A PPG `v e1 : A ! B

TV-A PP V

G `v e2 : A

G `v e : Px : A. B

G `v v : A

G `v e v : B[x 7! v ]G `v e1 e2 : B

TV-P ROD

G `v A : s1
G, x : A `v B : s2
(s1 , s2 , s3 ) 2 R
G `v Px : A. B : s3
TV-C ASTUP

G `v B : s

G `v e : A

TV-M UG `v A : s
G, x : A `v e : A
G `v µx : A. e : A
TV-C ASTDN

B ,!v AG `v cast" [B] e : B

G `v e : A

A ,!v BG `v cast# e : B`v G(Well-formedness)
WV-N IL`v ?

WV-C ONS

G `v A : sx fresh in G
`v G, x : A

Fig. 4. Call-by-value PITS
Theorem 5.2 (Progress of Call-by-value PITS)
If ? `v e : A then either e is a value v or there exists e0 such that e ,!v e0 .
Like call-by-name reduction, the one-step call-by-value reduction is deterministic:
Lemma 5.2 (Determinacy of One-step Call-by-value Reduction)

ZU064-05-FPR

main

28

23 September 2019

10:36

Y. Yang and B. Oliveira

If e ,!v e1 and e ,!v e2 , then e1 ⌘ e2 .
Similarly, for functional PITS, we have typing uniqueness and decidable type checking:Lemma 5.3 (Uniqueness of Typing for Functional PITS)
In any functional PITS, if G `v e : A and G `v e : B, then A ⌘ B.
Theorem 5.3 (Decidability of Type Checking for Functional PITS)
In any functional PITS, given a well-formed context G and a term e, it is decidable todetermine if there exists A such that G `v e : A.
6 Iso-Types with Full Casts
In Sections 4 and 5, we have introduced two variants of PITS that use one-step call-byname/value reduction for both term evaluation and type conversion. The use of those reduction strategies simplifies the design and metatheory, at the cost of some expressiveness. To
gain extra expressiveness, we take one step further to generalize casts with full reduction. In
this section, we present a third variant of PITS called full PITS, where casts use a decidable
parallel reduction relation for type conversion. The trade-off is some extra complexity inthe metatheory. We show that full PITS has decidable type checking and type safety that
holds up to erasure of casts. The proofs and metatheory design is inspired by approaches
used in Zombie (Sjöberg & Weirich, 2015) and Guru (Stump et al., 2008).
6.1 Full Casts with Parallel Reduction
Cast operators in call-by-name/value PITS use the same one-step reduction as term evaluation for type-level computation. We refer to them as weak casts, because they lack theability to do full type-level computation where reduction can occur at any position ofterms. For example, weak casts cannot convert the type Vec (1 + 1) to Vec 2, because
1) for call-by-name reduction, the desired reduction is at the non-head position; 2) for callby-value reduction, the term is rejected due to the value restriction. Thus, we generalize
weak casts to full casts (cast* and cast+ ) utilizing a one-step decidable parallel reduction(,!p ) relation for type conversion. Fig. 5 shows the definition of ,!p . This relation allows
reducing terms at any position, including non-head positions or inside binders, e.g., l x :Int. 1 + 1 ,!p l x : Int. 2. Thus full type-level computation for casts is enabled.
There are three remarks for parallel reduction worth mentioning. Firstly, parallel reduction is defined up to erasure denoted by |e| (see Fig. 6), a process that removes all
casts from term e. We also extend erasure to context denoted by |G|. It is feasible to define
parallel reduction only for erased terms because casts in full PITS (also call-by-value PITS)
are only used to ensure the decidability of type checking and have no effect on dynamic
semantics, thus are computationally irrelevant (will be discussed in Section 7.1). We use
metavariables r and R to range over erased terms and types, respectively. The only syntacticchange of erased terms is that there is no cast. The type system after erasure is essentiallya variant of PTS with recursion. We call it PTSµ . The syntax and semantics of PTSµ isshown in Fig. 7.

ZU064-05-FPR

main

23 September 2019

10:36

29

Pure Iso-Type Systems
r1 ,!p r2(Decidable Parallel Reduction)

P-R ED

P-VAR

P-S ORT(l x : R. r1 ) r2 ,!p r1 [x 7! r2 ]x ,!p xs ,!p sP-A BSR ,!p R0P-P ROD

r ,!p r00

l x : R. r ,!p l x : R . r

R1 ,!p R01

0

R2 ,!p R02

Px : R1 . R2 ,!p Px : R01 . R02
P-M U

R ,!p R0

P-A PP

r1 ,!p r10

r2 ,!p r20

r1 r2 ,!p r10 r20
P-M U R ED

µx : R. r ,!p r[x 7! µx : R. r]

r ,!p r0

µx : R. r ,!p µx : R0 . r0

Fig. 5. One-step decidable parallel reduction of erased terms(Term Erasure)

|e|
|x|
|s|
|e1 e2 ||l x : A. e||Px : A. B||µx : A. e||cast* [A] e||cast+ [A] e|

=
=
=
=
=
=
=
=

x
s
|e1 | |e2 |l x : |A|. |e|Px : |A|. |B|µx : |A|. |e||e||e|(Context Erasure)|G||?||G, x : A|==?
|G|, x : |A|

Fig. 6. Erasure of casts
Secondly, the definition of parallel reduction in Fig. 5 is slightly different from thestandard one for PTS (Adams, 2006). It is partially parallel: rule P-R ED and rule PM U R ED do not parallel reduce sub-terms, but only do beta reduction and recursion unrolling, respectively. The confluence property for one-step reduction is lost4 . Nevertheless,such definition makes the decidability property (see Lemma 6.5) easier to prove than theconventional fully parallel version, thus it is called decidable parallel reduction. It also
requires fewer reduction steps than the non-parallel version, thus correspondingly needs
fewer casts.
Thirdly, parallel reduction does not have the determinacy property like weak-head reduction (Lemma 4.2). For example, for the term (l x : Int. 1 + 1) 3, we can (parallel) reduce
4

Notice that multi-step reduction ,!
!p is still confluent since it is equivalent to multi-step full beta
reduction !⇤b (see Lemma 6.3) which is confluent.

ZU064-05-FPR

main

23 September 2019

10:36

30

Y. Yang and B. Oliveira(Syntax)
Expressions
ValuesContexts

r, R ::= x | s | r1 r2 | l x : R. r | Px : R1 . R2 | µx : R. r
u ::= s | l x : R. r | Px : R1 . R2
D ::= ? | D, x : R(Weak-head Reduction)

r1 ,! r2
RE-A PPRE-B ETA

RE-M U

r1 ,! r10

r1 r2 ,! r10 r2(l x : R. r1 ) r2 ,! r1 [x 7! r2 ]D`r:R
TE-A X`Dµx : R. r ,! r[x 7! µx : R. r](Typing of PTSµ )TE-A BS

TE-VAR`D(s1 , s2 ) 2 A

D ` s1 : s2

D ` R1 : s1
D, x : R1 ` r : R2
D, x : R1 ` R2 : s2
(s1 , s2 , s3 ) 2 R

x:R 2 DD`x:R

D ` l x : R1 . r : Px : R1 . R2

TE-P ROD
TE-A PPD ` r1 : Px : R1 . R2

D ` r2 : R1

D ` r1 r2 : R2 [x 7! r2 ]TE-M UD`R:s

D, x : R ` r : R

D ` µx : R. r : R`D

D ` R1 : s1
D, x : R1 ` R2 : s2
(s1 , s2 , s3 ) 2 R
D ` Px : R1 . R2 : s3

TE-C ONVD ` r : R1

D ` R2 : s
D ` r : R2

R1 ⌘b R2

(Well-formedness)
WE-N IL`?

WE-C ONSD`R:sx fresh in G

` D, x : R

Fig. 7. PTSµ

it to either (l x : Int. 2) 3 by rule P-A PP and rule P-A BS, or 1 + 1 by rule P-R ED. Thus,
to ensure the decidability, we also need to add the type annotation for cast+ operator toindicate what exact type we want to reduce to. Similarly to cast* , cast+ [A] v is a value,
which is different from the call-by-name/value variant.
Fig. 8 shows the specification of full PITS. Changes from call-by-name/value PITS are
highlighted. Note that we do not define operational semantics directly but up to erasure.
Reduction relations are defined in PTSµ only for terms after erasure. Similarly, syntactic
values are not defined in full PITS but defined for erased terms, ranged over by u in PTSµ
(see Figure 7). This is different from call-by-name/value PITS, where reduction rules
for type casting and term evaluation are the same, i.e., the one-step call-by-name/value
reduction. In full PITS, parallel reduction is only used by casts, while a separate reduction
is used for term evaluation. For simplicity reasons, we choose the call-by-name reduction(,!) for term evaluation for erased terms in PTSµ (see Fig. 7).

ZU064-05-FPR

main

23 September 2019

10:36

31

Pure Iso-Type Systems(Syntax)
Expressionse, A, B ::= x | s | e1 e2 | l x : A. e | Px : A. B
| µx : A. e | cast* [A] e | cast+ [A] e
G ::= ? | G, x : A

Contexts
G `f e : A(Typing of Full PITS)
TF-A BSTF-A X`f G

TF-VAR`f G(s1 , s2 ) 2 A

G ` f s1 : s2

G `f A : s1
G, x : A `f B : s2

x:A 2 GG `f x : A

G, x : A `f e : B(s1 , s2 , s3 ) 2 R

G `f l x : A. e : Px : A. B

TF-P ROD
TF-A PPG `f e1 : Px : A. B

G ` f A : s1
G, x : A `f B : s2
(s1 , s2 , s3 ) 2 R

G `f e2 : A

G `f e1 e2 : B[x 7! e2 ]TF-M UG `f A : s

G `f Px : A. B : s3

TF-C ASTUP

G `f B : s

G, x : A `f e : A

G `f µx : A. e : A

G `f e : A|B| ,!p |A|G `f cast* [B] e : B

TF-C ASTDN

G `f B : s

G `f e : A|A| ,!p |B|G `f cast+ [B] e : B`f G(Well-formedness)
WF-N IL`f ?

WF-C ONS

G `f A : sx fresh in G

`f G, x : A

Fig. 8. Full PITS
6.2 Metatheory
We show that the two key properties, type safety and decidability of type checking, still
hold in full PITS.
Type Safety. Full casts are more expressive but also complicate the metatheory: term
evaluation could get stuck using full casts. For example, the following term,(cast+ [Int ! Int] (l x : ((l y : ?. y) Int). x)) 3
cannot be further reduced because the head position is already a value but not a l -term.
Note that weak casts do not have such problem because only cast" is annotated and it is
not legal to have a P-type in the annotation (see last paragraph of Section 4.5). To avoid
getting stuck by full casts, one could introduce several cast push rules similar to System
FC (Sulzmann et al., 2007). For example, the stuck term above can be further evaluated by

ZU064-05-FPR

main

23 September 2019

32

10:36

Y. Yang and B. Oliveira

r1 !b r2

(Full Reduction)
B-A PP 1

B-R ED(l x : R. r1 ) r2 !b r1 [x 7! r2 ]r1 r2

B-A BS 2

l x : R. r !b l x : R0 . r

l x : R. r !b l x : R. r0

B-P ROD 2

R2 !b R02

Px : R1 . R2 !b Px : R1 . R02

r2 !b r20

!b r10 r2

B-A BS 1

R ! b R0

B-A PP 2

r1 !b r10

r !b r0

r1 r2 !b r1 r20
B-P ROD 1

Px : R1 . R2 !b Px : R01 . R2

B-M U R ED

µx : R. r !b r[x 7! µx : R. r]
B-M U 2

R1 !b R01

B-M U 1

R !b R0µx : R. r !b µx : R0 . r

r !b r 0µx : R. r !b µx : R. r0

Fig. 9. Full beta reduction
pushing cast+ into the l -term:(cast+ [Int ! Int] (l x : ((l y : ?. y) Int). x)) 3 ,! (l x : Int. x) 3
However, adding “push rules” significantly complicates the reduction relations and metatheory. Instead, we adopt the erasure approach inspired by Zombie (Sjöberg & Weirich, 2015)
and Guru (Stump et al., 2008) that removes all casts when proving the type safety. The
typing of erased terms follow the type system PTSµ (see Fig. 7). The typing judgment is
D ` r : R where D ranges over the erased context.
PTSµ is a variant of PTS with recursion. We follow the standard proof steps for PTS (Barendregt, 1992). The substitution and progress lemmas are stated as follows:
Lemma 6.1 (Substitution of PTSµ )If D1 , x : R0 , D2 ` r1 : R and D1 ` r2 : R0 , then D1 , D2 [x 7! r2 ] ` r1 [x 7! r2 ] : R[x 7! r2 ].
Theorem 6.1 (Progress of PTSµ )If ? ` r : R then either r is a value u or there exists r0 such that r ,! r0 .
Notice that term evaluation uses the weak-head reduction ,!. We only need to prove
subject reduction and progress theorems for ,!. But we generalize the result for subject
reduction, which holds up to the parallel reduction ,!p . We first show subject reduction
holds for one-step full beta reduction !b (see Fig. 9) and multi-step full beta reduction!⇤b , i.e., reflexive and transitive closure of !b :Lemma 6.2 (Subject Reduction for Full Beta Reduction)
1. If D ` r : R and r !b r0 then D ` r0 : R.
2. If D ` r : R and r !⇤b r0 then D ` r0 : R.
Then we show !⇤b is equivalent to multi-step parallel reduction ,!
!p , i.e., transitive
closure of ,!p (since it is already reflexive):

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

33

Lemma 6.3 (Equivalence of Parallel Reduction)
Given r1 and r2 , r1 !⇤b r2 holds if and only if r1 ,!
!p r2 holds.
Thus, subject reduction for parallel reduction ,!p is an immediate corollary:
Theorem 6.2 (Subject Reduction for Parallel Reduction)
If D ` r : R and r ,!p r0 then D ` r0 : R.
Finally, given that the PTSµ is type-safe, if we want to show the type-safety of full PITS,
it is sufficient to show the typing is preserved after erasure:Lemma 6.4 (Soundness of Erasure)
If G `f e : A then |G| ` |e| : |A|.
Decidability of Type Checking. The proof of decidability of type checking full PITS issimilar to call-by-name PITS in Section 4.5. We also limit discussion of decidability tofunctional PITS (see Definition 4.1). The only difference is for cast rule TF-C ASTUP andrule TF-C ASTDN, which use parallel reduction |A1 | ,!p |A2 | as a premise. We first show
the decidability of parallel reduction:
Lemma 6.5 (Decidability of Parallel Reduction)
Given r1 and r2 , it is decidable to determine whether r1 ,!p r2 holds.
The proof is by induction on the length of r1 and attempting to construct a parallel reduction
step from r1 to r2 . A checking algorithm can be derived from the proof and runs inlinear time in the size of both terms. Notice that the proof does not rely on the singlestep confluence of ,!p . The confluence of ,!p is lost due to two base reduction rules PR ED and P-M U R ED, which do not simultaneously reduce sub-terms but only do one-stepbeta reduction and recursive unrolling, respectively (see Section 6.1). However, both rules
become deterministic, which makes it easier to determine if ,!p in both cases. We can justcheck if one-step reduction of r1 is equal to r2 , similarly to the proof for call-by-name PITS
(see Section 4.5). For example, consider r1 = (l x : R3 . r3 ) r4 and r2 = r5 r6 . If case P-A PP
applies, i.e., l x : R3 . r3 ,!p r5 and r4 ,!p r6 hold, then r1 ,!p r2 holds trivially. Otherwise,
r1 ,!p r2 holds if and only if P-R ED holds. The latter can be determined by testing theequality of r3 [x 7! r4 ] and r5 r6 . By contrast, the proof will be much complicated for the
standard parallel reduction. To ensure one-step confluence, the rule P-R ED becomes
r1 ,!p r10

r2 ,!p r20(l x : R. r1 ) r2 ,!p r10 [x 7! r20 ]We now need to determine if r3 ,!p r30 holds or not. This is non-trivial since the induction
hypothesis only gives the hint whether l x : R3 . r3 ,!p r5 holds but not directly for r3 .
As cast* and cast+ are annotated, both A1 and A2 can be determined and the welltypedness is checked in the original system. By Lemma 6.4, the erased terms keep thewell-typedness. By Lemma 6.5, it is decidable to check if |A1 | ,!p |A2 |. We conclude thedecidability of type checking by following lemmas:
Lemma 6.6 (Uniqueness of Typing for functional PITS)
In any functional PITS, if G `f e : A1 and G `f e : A2 , then A1 ⌘ A2 .

ZU064-05-FPR

main

23 September 2019

10:36

34

Y. Yang and B. OliveiraD✏r:R(Typing of PTSstep )TS-A BS

TS-A X✏D

TS-VAR✏D(s1 , s2 ) 2 A

D ✏ s1 : s2

D ✏ R1 : s1
D, x : R1 ✏ r : R2
D, x : R1 ✏ R2 : s2
(s1 , s2 , s3 ) 2 R

x:R 2 DD✏x:R

D ✏ l x : R1 . r : Px : R1 . R2

TS-P ROD
TS-A PPD ✏ r1 : Px : R1 . R2

D ✏ R 1 : s1
D, x : R1 ✏ R2 : s2
(s1 , s2 , s3 ) 2 R

D ✏ r2 : R1

D ✏ r1 r2 : R2 [x 7! r2 ]TS- MUD✏R:s

D, x : R ✏ r : R

D ✏ Px : R1 . R2 : s3

TS-B ETAUP

D ✏ r : R1

D ✏ R2 : s

D ✏ µx : R. r : R

D ✏ r : R2

TS-B ETADN

D ✏ r : R1

D ✏ R2 : s
D ✏ r : R2

R2 !b R1

R1 !b R2

✏D

(Well-formedness)
WS-C ONS

WS-N ILD✏R:sx fresh in G

✏ D, x : R✏?

Fig. 10. Typing rules of PTSstep
Theorem 6.3 (Decidability of Type Checking for functional PITS)
In any functional PITS, given a well-formed context G and a term e, it is decidable todetermine if there exists A such that G `f e : A.
6.3 Completeness to Pure Type Systems
We have shown that full PITS is complete to a variant of PTSµ . Such variant uses analternative single-step conversion rule (Geuvers, 1995):
TS-B ETAUP

D ✏ r : R1

D ✏ R2 : s
D ✏ r : R2

TS-B ETADN

D ✏ r : R1

D ✏ R2 : s
D ✏ r : R2

R2 !b R1

R1 !b R2

where !b denotes full beta reduction (see Fig. 9). We call this variant PTSstep (seeFig. 10). Its typing judgment is denoted by D ✏ r : R. PITS can be seen as an annotatedversion of PTSstep . We first show that full PITS is complete to PTSstep by the following
lemma:

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

35

Lemma 6.7 (Completeness of Full PITS to PTSstep )If D ✏ r : R, then there exists G,e and A such that G `f e : A where |G| = D, |e| = r and|A| = R.
Furthermore, Siles and Herbelin have proved that single-step conversion rule is equivalent to the original conversion rule using beta conversion in PTS (see Corollary 2.9 in (Siles& Herbelin, 2012)). We have the following relation between PTSstep and PTSµ :Lemma 6.8 (Completeness of One-step PTS to PTS)
If D ` r : R, then D ✏ r : R holds.
Thus, we can conclude the full PITS is complete to PTSµ :Theorem 6.4 (Completeness of Full PITS to PTSµ )If D ` r : R, then there exists G, e, A such that G `f e : A where |G| = D, |e| = r and |A| = R.
7 Discussion and Related WorkIn this work we have developed three variants of PITS. The three variants differ on the
reduction rules used in the cast operators. As it turns out the specific choice of reduction
has quite a bit of impact on the formalization and the metatheory. In this section we startby presenting an extensive comparison between the three variants of PITS, as well as PTS f(which is a closely related variant of PTS). Then we discuss other closely related work.
7.1 Comparing the three variants of PITS and PTS f
We have developed PITS with the aim of using such family of calculi as foundations to programming languages supporting unified syntax and recursion. PITS trades the convenienceof implicit type conversion that is afforded in most dependently typed calculi by a simple
meta-theory that allows for decidable type-checking. Closely related to our work is PTS
with explicit convertibility proofs (PTS f ) (van Doorn et al., 2013), which is a variant of
PTS. PTS f replaces the conversion rule by embedding explicit conversion steps into terms.
PTS f has strong connections to PITS in the sense that both systems are based on Pure
Type Systems and require explicit type conversions — PTS f uses proof-annotated terms,
while PITS uses cast operators. Nevertheless the design of PTS f is still quite complex, as
it requires a separate sub-language for building convertibility (equality) proofs.
Although PTS f was motivated by applications to theorem proving, PTS f (like PTS) canbe instantiated to form inconsistent calculi, which can encode fixpoints and general recursion. Therefore PTS f could also, in principle, be used as a foundation for programming
languages. However, the underlying mechanisms and foundations of PTS f and PITS are
different. Generally speaking, when dealing with programming languages with generalrecursion it is important to study not only the static semantics, but also the dynamic
semantics. Unlike strongly normalizing languages where any choice of reduction leads
to termination, in languages that are not strongly normalizing this is not usually the caseand the choice of reduction is important. Furthermore the choice of the style of reduction
in casts has a profound impact on the properties and metatheory of the language. Our

ZU064-05-FPR

main

23 September 2019

36

10:36

Y. Yang and B. Oliveira
Table 2. Comparison between PTS f and PITS

Features

PTS f

Direct Dynamic Semantics
Direct Proofs
No Mutually Dependent Judgments
Implicit Proofs by Reduction
Full Type-Level Computation
Consistency of Reduction
Decidability with Recursion
Erasability of Casts
Equality
No Value Restriction

#
#
#
#

SLOC of Coq proofs
Lemmas of Coq proofs

7318
319

—
G
#2

Call-by-name Call-by-value Full PITS
PITS
PITS
#
#
G1
#
#
#
G3
1217
62

#

#

G
#3
#

3

1477
66

3796
221

1 Proofs for typing decidability are direct, but not for type-safety.

2 We believe that decidability should hold, but no there is no discussion or proofs in theformalization of PTS f (van Doorn et al., 2013).
3 Encoding via Leibniz equality.

work on PITS puts great emphasis on the study of the dynamic semantics and the tradeoffs between different choices, while in PTS f only the static semantics is studied. Next
we give a detailed comparison on features between PTS f and the three variants of PITS,
summarized in Table 2.
Direct Dynamic Semantics. One important difference between call-by-value and call-byname PITS and the variant with full reduction is that the former two calculi have a direct
small-step operational semantics, while the semantics of the later calculus is indirectly
given by elaboration. A direct operational semantics has the advantage that the reduction
rules can be used to directly reason about expressions in the calculus. This reasoning canbe used to perform, for example, equational reasoning steps or to justify the correctness ofsome optimizations. In an elaboration-based semantics the lack of reduction rules meansthat one must first translate the source expression into a corresponding expression in thetarget calculus, and then do all reasoning there. This is a much more involved process.
As discussed in Section 6.2, it is difficult to directly define a type-preserving operationalsemantics for full PITS. The problem is not intrinsic to PITS, but rather it is a general
problem whenever full reduction is used in cast-like operators. Indeed this problem has
been identified previously in the literature (Sjöberg et al., 2012; Sulzmann et al., 2007),and two major approaches have been used to address it. One approach is not to use a directsemantics but instead to use an elaboration semantics, which is precisely the approach that
we used in our variant of PITS with full reduction. This approach is quite common and
it is also the approach used in PTS f as well as several other calculi (Sjöberg et al., 2012;

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

37

Sjöberg & Weirich, 2015; Stump et al., 2008). Another approach that has been presented
in the literature is to use push rules as in System FC (Sulzmann et al., 2007; Yorgey et al.,2012; Weirich et al., 2013) and System DC (Weirich et al., 2017). However push rules
significantly complicate the reduction rules (see Section 6.2).
In this work we show a third approach to achieve a simple type-preserving direct dynamic semantics: we can use alternative weaker reduction relations (call-by-value or callby-name) for type conversion. The weaker reduction relations are straightforward and do
not have the extra complication of the push rules (although some expressiveness is lost).
There is no discussion on how to achieve direct dynamic semantics using the proof term
approach by PTS f , since they use an elaboration approach. Furthermore this is unlikely to
be trivial. We expect that it may be possible to give a direct operational semantics to full
PITS or PTS f using push rules similar to the ones employed in System DC (Weirich et al.,2017), but this would come at the cost of a much more involved set of reduction rules (aswell as the corresponding meta-theory).
Direct Proofs. Because of the direct dynamic semantics it is possible to do direct proofs ofpreservation and progress in call-by-value and call-by-name PITS. The meta-theory of Full
PITS is significantly more involved because we need a target calculus and to prove several
lemmas in both the target and the source, as well as showing the correspondence between
the two systems. To give a rough idea of the complexity of the different developments,
Table 2 shows the total number of lines of Coq code used and lemmas used to formalize
the three variants of PITS. Roughly speaking the development of full PITS requires twice
as many SLOC and nearly four times more lemmas than the other two variants, since wealso need to formalize PTSµ along with full PITS.
PTS f is shown to be equivalent to plain PTS and its type-safety then can be guaranteedby showing the correspondence to plain PTS (Barendregt, 1991). However the proof forsoundness and completeness between PTS f and PTS is highly non-trivial (van Doorn et al.,2013; Siles & Herbelin, 2012). In PTS f there is no discussion on proving subject reduction
directly in PTS f . The type-safety of PTS f is indirectly shown by erasure of explicit proofs
to generate valid plain PTS terms. This is similar to the proof strategy for type-safetyof full PITS, which is shown up to erasure of casts (see Section 6.2). The formalizationof PTS f requires about 7000 SLOC and 300 lemmas (see Table 2), including auxiliary
systems such as plain PTS and PTSe . These numbers cannot be directly compared to thenumbers of the PITS formalizations, since different approaches and libraries are employed
to deal with binding and the formalization of PTS f does not include proofs of decidabilityof type-checking. Nevertheless the numbers are useful to give an idea of the effort in the
PTS f formalization.
Ultimately we believe that direct proofs and a direct operational semantics of the callby-name and call-by-value PITS are quite simple. Furthermore such simplicity is helpfulwhen trying to extend calculi to study additional features. One non-trivial extension that wehave already studied, based on a particular instance of the call-by-name PITS, is subtyping (Yang & Oliveira, 2017). Integrating subtyping and some form of dependent types
is a widely acknowledged difficult problem (Aspinall & Compagnoni, 1996; Castagna& Chen, 2001; Hutchins, 2010). Nevertheless, using our call-by-name instance of PITS
extension with subtyping we have managed to develop a calculus that subsumes System

ZU064-05-FPR

main

23 September 2019

38

10:36

Y. Yang and B. OliveiraF<: (Cardelli et al., 1994) and has several interesting properties, including subject reduction
and transitivity of subtyping. We believe this development would be a lot harder to do byextending full PITS or PTS f .
No Mutually Dependent Judgments. PTS f requires more language mechanisms for typeconversions, including proof terms (H) and their typing rules (G ` f H : A = B) to ensure
coercions (A = B) are well-typed. However, the well-formedness checking of coercions
depends on typing judgments (G ` f e : A), which causes mutual dependency of judgments
and complicates proofs. Casts in PITS use reduction relations (A ,! B), which are untyped
and do not depend on typing rules. The well-formedness of types is checked separately intyping rules of cast operators, e.g. TF-C ASTUP and TF-C ASTDN in full PITS. The factthat PITS does not require such mutually dependent judgments means that many proofs
can be proved using simple inductions. In PTS f the mutually dependent judgments leads
to several lemmas that need to be mutually proved.
Implicit Proofs by Reduction. PTS f uses coercions (i.e. equivalence relations) to explicitly write equality proofs, while PITS uses reduction relations that implicitly construct suchproofs. Equality proofs in PTS f are constructed by proof terms. Each language constructrequires a corresponding proof term to reason about equality of sub-terms, which adds tothe number of language constructs. On the contrary, PITS does not require proof terms but
two extra cast operators, thus has fewer language constructs.
Type conversions in PTS f are more “explicit” than in PITS. One needs to specify which
proof terms to be used exactly in PTS f , while he/she just needs casts without specifying
which underlying reduction rule to use. This makes it easier to do explicit type conversions
in PITS. Assume that we have integer literals and use beta reduction to evaluate addition(1 + 1 ,! 2). Recall the example from Section 1:
e : Px : Int. Vec (1 + 1)
e0 : Px : Int. Vec 2
To obtain e0 from e, in PTS f , e0 = eH where H is a proof term such thatH = {Int, [x : Int](Vec b (1 + 1))}
In full PITS, e0 = cast

+ [Px : Int. Vec 2] e, which implicitly uses the reduction rules P-

P ROD, P-A PP and P-R ED in the cast operator. In call-by-name/value PITS, due to thedeterminacy of reduction used in casts, the cast# operator even does not require a type
annotation. For example, consider a simpler type conversion (l x : ?. x) Int ,! Int from
Section 2.3:
e : (l x : ?. x) Int
e0 : Int
where e0 can simply be cast# e without any annotation.
Generally speaking we believe that for programming, and especially more traditional
forms of programming that do not involve complex forms of type-level reasoning, havingsuch implicit proofs of conversion is good. We believe that for a practical language design
to be based directly on PTS f it would require some degree of inference of the equality
proof terms. In some sense full PITS can be thought of a system that implicitly generates

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

39

proof terms and in principle could be translated to PTS f , but it is one step closer to asource language that infers equality proof terms. Of course if the goal is to do theorem
proving and/or heavy uses of type level computation then having explicit control over theequality proof terms can be an advantage. However for PITS our focus is on programming
languages with general recursion.
Full Type-Level Computation. PTS f has full type-level computation since type conversion uses equivalence relations which are congruent. It has the same expressive power as
Pure Type Systems. Full PITS similarly has full type-level computation, while call-byname/value PITS do not. Full type-level computation is useful for theorem proving andfull-spectrum dependently typed programming as in Coq and Agda, but not necessarily
required for traditional programming. As the examples presented in Section 3 show, isotypes that just use weak-head call-by-name reductions in casts can encode many advanced
type-level features. The extra expressiveness of PTS f and full PITS also comes at the costof additional complexity in the metatheory and makes it non-trivial to achieve features likedirect dynamic semantics and direct type-safety proofs.
Consistency of Reduction. In many strongly normalizing languages a basic assumption isthat the order of reduction does not matter. This justifies reasoning that can be done in any
order of reduction. Reduction strategies such as parallel reduction embody this principle
and enable reductions in terms to occur in multiple orders. However, in languages withgeneral recursion this assumption is broken: i.e. reduction order does matter. For example,
given term (l x : Int. 1) ?, where ? is any diverging computation, such term evaluates
to 1 with call-by-name semantics, but diverges with call-by-value semantics. If we wantto conduct precise reasoning about programs and their behavior we cannot ignore theorder of reduction. In particular, if we want the type-level reduction to respect the runtime semantics/reduction then we need to ensure that the two reductions are in some sense
consistent.
We study three different variants of PITS that differ on term evaluation strategy, as wellas the reduction strategy employed by the cast operators. They have different trade-offs interms of simplicity and expressiveness. Call-by-name PITS uses weak-head call-by-namereduction, while call-by-value PITS enables standard call-by-value reduction by employing
a value restriction (Swamy et al., 2011; Sjöberg et al., 2012). In both designs the key idea
is that the same reduction strategy is used for both term evaluation and type casts, ensuring
a consistent behavior of reduction at both type and term level. In call-by-name/value PITS,
we can trivially guarantee that no invalid reasoning steps can happen due to mismatcheswith the evaluation strategy.
In full PITS, the use of parallel reduction breaks consistency because type-level reduction allows some reductions that are not allowed at the term-level. For example, Int !
Vec (1 + 1) can be reduced to Int ! Vec 2 by type-level parallel reduction but not termlevel reduction. We believe that it may be possible to have a variant of PITS that uses
call-by-name or call-by-value and has a consistent form of full reduction that respects the
reduction order. However we leave this for future work.
PTS f has no discussion on reduction rules for term evaluation, since its dynamic semantics is given by elaboration into PTS. Since the focus of PTS f is primarily on the

ZU064-05-FPR

main

40

23 September 2019

10:36

Y. Yang and B. Oliveira

applications to theorem proving the issues of consistency between term and type-level
reduction are not relevant, because such for theorem proving calculi are normally strongly
normalizing and reduction order does not affect the semantics.
Decidability in the Presence of Recursion. There is no formal discussion or direct proof
on decidability of the type system for PTS f , though this seems to be a plausible property
since the typing rules of PTS f are syntax-directed. Only uniqueness of typing is formally
discussed and proved for functional PTS f . This is similar to functional PITS which haveuniqueness of typing up to only alpha equality due to the absence of implicit beta conversion (see Lemma 4.1). Uniqueness of typing is used in the decidability proof of functional
PITS (see Section 4.5), and we believe that it should be useful to prove decidability of
PTS f as well.
Alternatively, note that an indirect proof for decidability of typing can be derived fromthe plain metatheory of PTS through the equivalence of PTS f and PTS. However, the original decidability proof for PTS relies on the normalization property (van Benthem Jutting,1993). Thus, non-normalizing PTS f cannot use such indirect approach to prove decidability for variants of PTS f with recursion/fixpoints.
For all three variants of PITS, decidability of type checking has been proved directlyin the presence of general recursion without relying on normalization, though the proof isdone only for functional PITS for simplicity reasons. We expect that a similar proof would
work for PTS f as well, and this would be interesting to prove in future work.
Erasability of Casts. Type casts are usually erased after type checking to avoid run-timecost. Erasure of casts is only valid if they are computationally irrelevant, meaning thatthe operational semantics of expressions does not change after erasure. As mentioned in
Section 6.1, casts in call-by-value and full PITS are erasable. In full (call-by-value) PITS,
cast* [A] v (cast" [A] v) is a value and becomes v after erasure, which is still a value anddoes not change the computational behavior. Similarly, equality proofs in PTS f are also
computationally irrelevant and erasable. In contrast, casts in call-by-name PITS do nothave this property, as we define cast" [A] e to be a value. If we erase the cast operator, ecan be further reducible, which changes the dynamic semantics. Nonetheless, it is easy togain erasability of casts in call-by-name PITS by partially adopting the call-by-value rules
for cast" specifically. For example, we can define cast" [A] v as a value and further reduce
inner terms of a cast" by rule RV-C ASTUP (see Fig. 4). We did not adopt this approachin call-by-name PITS, since such operational semantics requires additional reduction rules
and complicates the metatheory.
Equality. PTS f has built-in support for propositional equality, while PITS needs to encode
equality types using Leibniz equality. In Section 3.4, we show the encoding of Leibniz
equality, which works for all three variants of PITS. But full PITS is required for complete
reasoning on equality types. In call-by-name/value PITS, equality reasoning is limited
since type conversions are not congruent. The reasoning required for vectors (e.g., tailfunction in Section 3.4) is not encodable.

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

41

No Value Restriction. We employ a value restriction in call-by-value PITS to retain
subject reduction with a simple proof. As discussed in Section 5.1, we will consider analternative approach by adding cast operators during dynamic semantics for future work.
In contrast, call-by-name and full PITS, as well as PTS f , do not rely on the value restriction
to prove subject reduction.

7.2 Other Related Work
Core calculus for functional languages. Girard’s System Fw (Girard, 1972) is a typed
lambda calculus with higher-kinded polymorphism. For the well-formedness of type expressions, an extra level of kinds is added to the system. In comparison, because of unified syntax, PITS is considerably simpler than System Fw , both in terms of language
constructs and complexity of proofs. As for type-level computation, System Fw differsfrom PITS in that it uses a conversion rule, while PITS uses explicit casts. PITS is also
inspired by the treatment of datatype constructors in Haskell (Jones, 1993). Iso-types have
similarities to newtypes and datatypes which involve explicit type-level computations.
The current core language for GHC Haskell, System FC (Sulzmann et al., 2007) is asignificant extension of System F, which supports GADTs (Peyton Jones et al., 2004),
functional dependencies (Jones, 2000), type families (Eisenberg et al., 2014), and kindequality (Weirich et al., 2013). System DC (Weirich et al., 2017) is a further extension to
FC and foundation of Dependently Typed Haskell (DTH) that extends Haskell with fullspectrum dependent types. System DC is not logically consistent and can support recursion
as well as decidable type-checking. However System DC is still quite ambitious in that itcomes with a rich notion of type equality aimed at supporting more sophisticated formsof type-level computation. While such rich notion of type equality adds expressive power,
the details of type equality are quite involved and System DC is still significantly more
complex than classic pure type systems or older Haskell/ML-style language designs basedon System F (Reynolds, 1974; Girard, 1972).
System FC and its extensions require a non-trivial form of type equality, which is currently missing from PITS. One possible direction for future work is to investigate theaddition of such forms of non-trivial type-equality. On the other hand, PITS uses unified
syntax and has only 8 language constructs, whereas the original System FC uses multiple
levels of syntax and currently has over 30 language constructs, making it significantly more
complex. The simplicity of PITS makes it suitable to be combined with other language
features, such as subtyping, which seems hard to support in FC and its extensions. For
example, we proposed l I6 (Yang & Oliveira, 2017), in a separate article, which extends avariant of PITS called l I with bounded quantification and subtyping and supports object
encodings (Pierce & Turner, 1994).
Unified syntax with decidable type-checking. Pure Type Systems (Barendregt, 1991)
show how a whole family of type systems can be implemented using just a single syntactic
form. PTSs are an obvious source of inspiration for our work. An early attempt of using a
PTS-like syntax for an intermediate language for functional programming was Henk (Peyton Jones & Meijer, 1997). The Henk proposal was to use the lambda cube as a typed

ZU064-05-FPR

main

42

23 September 2019

10:36

Y. Yang and B. Oliveiraintermediate language, unifying all three levels. However the authors have not studied the
addition of general recursion, full dependent types or the meta-theory.
Zombie (Casinghino et al., 2014) is a dependently typed language using a single syntactic category. It is composed of two fragments: a logical fragment where every expression is
known to terminate, and a programmatic fragment that allows general recursion. Though
Zombie has one syntactic category, it is still fairly complicated (with around 24 language
constructs) as it tries to be both consistent as a logic and pragmatic as a programming
language. Even if one is only interested in modeling a programmatic fragment, additional
mechanisms are required to ensure the validity of proofs (Sjöberg et al., 2012; Sjöberg &Weirich, 2015). In contrast to Zombie, PITS takes another point of the design space, giving
up logical consistency and reasoning about proofs for simplicity in the language design.
Unified syntax with general recursion and undecidable type checking. Cayenne (Augustsson, 1998) integrates the full power of dependent types with general recursion, whichbears some similarities with PITS. It uses one syntactic form for both terms and types,
allows arbitrary computation at type level and is logically inconsistent because of thepresence of unrestricted recursion. Moreover, the most crucial difference from PITS isthat type checking in Cayenne is undecidable. From a pragmatic point of view, this design
choice simplifies the implementation, but the desirable property of decidable type checking
is lost. Cardelli’s Type:Type language (Cardelli, 1986) also features general recursion to
implement equi-recursive types. Recursion and recursive types are unified in a single construct. However, both equi-recursive types and the Type:Type axiom make the type system
undecidable. PS (Altenkirch et al., 2010) is another example of a language that uses one
recursion mechanism for both types and functions. The type-level recursion is controlled
by lifted types and boxes since definitions are not unfolded inside boxes. However, PS does
not have decidable type checking due to the “type-in-type” axiom. And its metatheory is
not formally developed.
Casts for managed type-level computation. Type-level computation in PITS is controlled by explicit casts. Several studies (Stump et al., 2008; Sjöberg et al., 2012; Kimmell
et al., 2012; Sjöberg & Weirich, 2015; Sulzmann et al., 2007; Gundry, 2013; Weirich et al.,2017) also attempt to use explicit casts for managed type-level computation. However,casts in those approaches are not inspired by iso-recursive types. Instead they require
equality proof terms, while casts in PITS do not. The need for equality proof terms complicates the language design because: 1) building equality proofs requires various otherlanguage constructs, adding to the complexity of the language design and metatheory; 2) It
is desirable to ensure that the equality proofs are valid. Otherwise, one can easily build bogus equality proofs with non-termination, which could endanger type safety. Guru (Stumpet al., 2008) and Sep3 (Kimmell et al., 2012) make syntactic separation between proofs
and programs to prevent certain programmatic terms turning into invalid proofs. System
DC (Weirich et al., 2017) and other FC variants (Sulzmann et al., 2007; Yorgey et al.,2012) similarly distinguish coercions (i.e. equality proofs) and programs syntactically. The
programmatic part of Zombie (Sjöberg et al., 2012; Sjöberg & Weirich, 2015), which has
no such separation, employs value restriction that restricts proofs to be syntactic values toavoid non-terminating terms. Gundry’s evidence language (Gundry, 2013) also unifies all

ZU064-05-FPR

main

23 September 2019

10:36

Pure Iso-Type Systems

43

syntactic levels including coercions, but uses different phases for separating programs andproofs. The typing rules contain an access policy relation to determine the conversion ofphases. Such mechanism is finer-grained yet more complicated. Note that our treatment offull casts in full PITS, using a separate erased system for developing metatheory, is similar
to the approach of Zombie or Guru which uses an unannotated system.
Restricted recursion with termination checking. As proof assistants, dependently typed
languages such as Coq (The Coq development team, 2016) and Adga (Norell, 2007) areconservative as to what kind of computation is allowed. They require all programs to terminate by means of a termination checker, ensuring that recursive calls are decreasing. Decidable type checking and logical consistency are preserved. But the conservative, syntactic
criteria is insufficient to support a variety of important programming styles. Agda offers an
option to disable the termination checker to allow writing arbitrary functions. However,this may endanger both decidable type checking and logical consistency. Idris (Brady,2011) is a dependently typed language that allows writing unrestricted functions. However,to achieve decidable type checking, it also requires termination checker to ensure only
terminating functions are evaluated by the type checker. While logical consistency is anappealing property, it is not a goal of PITS. Instead PITS aims at retaining (term-level)
general recursion as found in languages like Haskell or ML, while benefiting from a unified
syntax to simplify the implementation and the meta-theory of the core language.
8 Conclusion and Future Work
This work proposes PITS: a family of minimal dependently typed core languages thatallow the same syntax for terms and types, support type-level computation, and preserve
decidable type checking under the presence of general recursion. The key idea is to control
type-level computation using iso-types via casts. Because each cast can only account for
one-step of type-level computation, type checking becomes decidable without requiringstrong normalization of the calculus. At the same time one-step casts together with recursion provide a generalization of iso-recursive types. Different variants of PITS show
trade-offs of employing different reduction strategies in casts.
In future work, we hope to investigate more applications of iso-types. Two possible
directions are discussed next:
Type-level computation and subtyping. One possible direction is to implement more
surface language mechanisms, so as to express intensive type-level computation in a moreconvenient way. For example, we can add lightweight (but not full) type inference forcasts, or multi-step casts with step limits. Another direction is to combine iso-types withmore language features, e.g., subtyping and strong dependent sums, which are useful tomodel object-oriented programming constructs and to model module systems. Thanks tothe simplicity of PITS, we can extend PITS without complicating the metatheory too much,as our previous work on l I6 (Yang & Oliveira, 2017) illustrates. Such extensions of PITS
could also be used as underlying theories of feature-rich languages, similarly to Dependent
Object Types (DOT) of Scala (Amin et al., 2012). We plan to develop a language based on
iso-types and unified subtyping (Yang & Oliveira, 2017), which will have similar features

ZU064-05-FPR

main

44

23 September 2019

10:36

Y. Yang and B. Oliveira

to DOT and be able to model Scala-like programming idioms, e.g., type members andpath-dependent types.
Traditional language designs and type-inference. It will be also interesting to use PITS
to model traditional functional languages like (older versions of) Haskell and ML withsome extra features that come “for free” from the use of dependent types and unified
syntax. We believe PITS should easily allow the development of functional languages
that stand somewhere in-between older designs of functional languages (such as Haskell
98 and the original ML) and dependently typed languages like Idris (Brady, 2011) andAgda (Norell, 2007) or dependently typed Haskell (Weirich et al., 2017). One short term
goal for the future is to study a version of the Fun language with type-inference.
We believe that the absence of a conversion rule makes the problem of type-inference
and unification considerably easier than for dependently typed languages with a conversion
rule. Type-inference is still a major difference between ML-like languages (and Haskell)and existing dependently typed languages. ML-like languages follow the Hindley-Milner(Hindley, 1969; Milner, 1978; Damas & Milner, 1982) tradition and support global typeinference requiring very few or no type-annotations at all. Part of the reason why typeinference works so well in those languages is that only first-order unification is necessary.
In contrast dependently typed languages, like Agda or Idris, typically employ local type
inference algorithms that require a considerable number of type annotations. This is needed
because the unification problem in such dependently typed languages is very hard. Essentially the presence of type level functions and a conversion rule means that a lot of types ofdifferent syntactic forms are equivalent. In the general case this would require higher-orderunification, which is undecidable (Huet, 1973). Because there is no conversion rule in PITS
the unification problem should be considerably simpler as two types are only equivalent if
they have the same syntactic form. If the unification problem for PITS (or representative
subsystems of PITS) is solved, this should enable forms of type-inference closer to Haskell
or ML.

Acknowledgements
We would like to thank the anonymous reviewers for their insightful and useful comments.
This work has been sponsored by the Hong Kong Research Grant Council projects number
17210617 and 17258816.

References
Accattoli, Beniamino, & Guerrieri, Giulio. (2016). Open call-by-value. Pages 206–226 of: Igarashi,
Atsushi (ed), Programming Languages and Systems. Cham: Springer International Publishing.
Adams, Robin. (2006). Pure type systems with judgemental equality. Journal of functional
programming, 16(02), 219–246.
Altenkirch, Thorsten, Danielsson, Nils Anders, Löh, Andres, & Oury, Nicolas. (2010). ps :Dependent types without the sugar. Pages 40–55 of: Blume, Matthias, Kobayashi, Naoki, &Vidal, Germán (eds), Functional and Logic Programming. Berlin, Heidelberg: Springer Berlin
Heidelberg.

ZU064-05-FPR

main

23 September 2019

10:36

45

Pure Iso-Type Systems

Amin, Nada, Moors, Adriaan, & Odersky, Martin. (2012). Dependent object types. 19th International
Workshop on Foundations of Object-Oriented Languages. FOOL ’12.
Amin, Nada, Rompf, Tiark, & Odersky, Martin. (2014). Foundations of path-dependent types. Pages
233–249 of: OOPSLA ’14. ACM.
Amin, Nada, Grütter, Samuel, Odersky, Martin, Rompf, Tiark, & Stucki, Sandro. (2016). The essenceof dependent object types. Pages 249–272 of: A List of Successes That Can Change the World.
Springer.
Aspinall, David, & Compagnoni, Adriana. (1996). Subtyping dependent types. Pages 86–97 of:
LICS ’96.
Augustsson, Lennart. (1998). Cayenne — a language with dependent types. Pages 239–250 of:Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming.
ICFP ’98. New York, NY, USA: ACM.
Barendregt, Henk. (1991). Introduction to generalized type systems.
programming, 1(2), 125–154.

Journal of functional

Barendregt, Henk. (1992). Lambda calculi with types. Pages 117–309 of: Handbook of Logic in
Computer Science, vol. 2.
Bird, Richard, & Meertens, Lambert. (1998). Nested datatypes. Pages 52–67 of: International
Conference on Mathematics of Program Construction. Springer.
Brady, Edwin C. (2011). Idris — systems programming meets full dependent types. Pages 43–54 of:Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification.
PLPV ’11. New York, NY, USA: ACM.
Bruce, Kim B., Cardelli, Luca, & Pierce, Benjamin C. (1999).
Information and computation, 155(1-2), 108–133.

Comparing object encodings.

Cardelli, Luca. (1986). A polymorphic lambda-calculus with type: Type. Digital Systems ResearchCenter.
Cardelli, Luca, Martini, Simone, Mitchell, John C., & Scedrov, Andre. (1994). An extension ofsystem f with subtyping. Information and computation, 109(1-2), 4–56.
Casinghino, Chris, Sjöberg, Vilhelm, & Weirich, Stephanie. (2014). Combining proofs and programsin a dependently typed language. Pages 33–45 of: Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages. POPL ’14. New York, NY, USA:
ACM.
Castagna, Giuseppe, & Chen, Gang. (2001). Dependent types with subtyping and late-boundoverloading. Information and computation, 168(1), 1–67.
Chakravarty, Manuel M. T., Keller, Gabriele, & Jones, Simon Peyton. (2005). Associated typesynonyms. Pages 241–253 of: ICFP ’05: Proceedings of the tenth ACM SIGPLAN international
conference on Functional programming. New York, NY, USA: ACM.
Cheney, James, & Hinze, Ralf. (2002). A lightweight implementation of generics and dynamics.
Pages 90–104 of: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell. Haskell ’02.
New York, NY, USA: ACM.
Cheney, James, & Hinze, Ralf. (2003). First-class phantom types. Tech. rept. CUCIS TR2003-1901.
Coquand, Thierry, & Huet, Gérard. (1988).
computation, 76, 95–120.

The calculus of constructions.

Information andCrary, Karl, Harper, Robert, & Puri, Sidd. (1999). What is a recursive module? Pages 50–63 of:Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and
Implementation. PLDI ’99. New York, NY, USA: ACM.
Damas, Luis, & Milner, Robin. (1982). Principal type-schemes for functional programs. Proceedingsof the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL’82.

ZU064-05-FPR

main

23 September 2019

46

10:36

Y. Yang and B. Oliveira

Eisenberg, Richard A. (2016). Dependent types in haskell: Theory and practice. Ph.D. thesis,
University of Pennsylvania.
Eisenberg, Richard A., Vytiniotis, Dimitrios, Peyton Jones, Simon, & Weirich, Stephanie. (2014).
Closed type families with overlapping equations. Pages 671–683 of: Proceedings of the 41st ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’14. New York,NY, USA: ACM.
Eisenberg, Richard A., Weirich, Stephanie, & Ahmed, Hamidhasan G. (2016). Visible typeapplication. Pages 229–254 of: Thiemann, Peter (ed), Programming Languages and Systems.
Berlin, Heidelberg: Springer Berlin Heidelberg.
Fegaras, Leonidas, & Sheard, Tim. (1996). Revisiting catamorphisms over datatypes with embedded
functions (or, programs from outer space). Pages 284–294 of: Proceedings of the 23rd ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’96. New York,NY, USA: ACM.
Geuvers, Herman. (1995). A short and flexible proof of strong normalization for the calculus of
constructions. Pages 14–38 of: Dybjer, Peter, Nordström, Bengt, & Smith, Jan (eds), Types for
Proofs and Programs. Berlin, Heidelberg: Springer Berlin Heidelberg.
Girard, Jean-Yves. (1972). Interprétation fonctionnelle et élimination des coupures de l’arithmétiqued’ordre supérieur. Ph.D. thesis, Université Paris VII.
Gundry, Adam Michael. (2013).
University of Strathclyde.

Type inference, haskell and dependent types.

Ph.D. thesis,

Hindley, Roger. (1969). The principal type-scheme of an object in combinatory logic. Transactionsof the american mathematical society, 146, 29–60.
Huet, Gérard. (1973). The undecidability of unification in third order logic. Information and control,
22(3), 257–267.
Hutchins, DeLesley S. (2010). Pure subtype systems. Pages 287–298 of: Proceedings of the 37th
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL
’10. ACM.
Jones, Mark P. (1993). A system of constructor classes: Overloading and implicit higher-order
polymorphism. Pages 52–61 of: Proceedings of the Conference on Functional Programming
Languages and Computer Architecture. FPCA ’93. New York, NY, USA: ACM.
Jones, Mark P. (2000). Type classes with functional dependencies. Pages 230–244 of: Smolka, Gert(ed), Programming Languages and Systems. Berlin, Heidelberg: Springer Berlin Heidelberg.
Kimmell, Garrin, Stump, Aaron, Eades, III, Harley D., Fu, Peng, Sheard, Tim, Weirich, Stephanie,
Casinghino, Chris, Sjöberg, Vilhelm, Collins, Nathan, & Ahn, Ki Yung. (2012). Equational
reasoning about programs with general recursion and call-by-value semantics. Pages 15–26
of: Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification.
PLPV ’12. New York, NY, USA: ACM.
Marlow, Simon. (2010). Haskell 2010 language report. 2010.
Milner, Robin. (1978). A theory of type polymorphism in programming. Journal of computer andsystem sciences, 17(3), 348–375.
Mogensen, T. Æ. (1992). Theoretical pearls: Efficient self-interpretation in lambda calculus. Journalof functional programming, 2(3), 345–364.
Norell, Ulf. (2007). Towards a practical programming language based on dependent type theory.
Ph.D. thesis, Chalmers University of Technology.
Odersky, Martin, Altherr, Philippe, Cremet, Vincent, Emir, Burak, Maneth, Sebastian, Micheloud,Stéphane, Mihaylov, Nikolay, Schinz, Michel, Stenman, Erik, & Zenger, Matthias. (2004).
An overview of the scala programming language. Tech. rept. IC/2004/64. EPFL Lausanne,
Switzerland.

ZU064-05-FPR

main

23 September 2019

10:36

47

Pure Iso-Type Systems

Paolini, Luca, & Della Rocca, Simona Ronchi. (1999). Call-by-value solvability. Rairo-theoreticalinformatics and applications, 33(6), 507–534.
Peyton Jones, Simon, & Meijer, Erik. (1997). Henk: a Typed Intermediate Language. Types inCompilation Workshop.
Peyton Jones, Simon, Washburn, Geoffrey, & Weirich, Stephanie. 2004 (July). Wobbly types:
type inference for generalised algebraic data types. Tech. rept. MS-CIS-05-26. University ofPennsylvania.
Pfenning, F., & Elliott, C. (1988). Higher-order abstract syntax. Pages 199–208 of: Proceedingsof the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation.
PLDI ’88. New York, NY, USA: ACM.
Pierce, Benjamin C. (2002). Types and programming languages. MIT press.
Pierce, Benjamin C., & Turner, David N. (1994). Simple type-theoretic foundations for objectoriented programming. Journal of functional programming, 4(02), 207–247.
Reynolds, John C. (1974). Towards a theory of type structure. Pages 408–425 of: Proceedings of the‘Colloque sur la Programmation’.
Schrijvers, Tom, Peyton Jones, Simon, Chakravarty, Manuel, & Sulzmann, Martin. (2008). Typechecking with open type functions. Proceedings of the 13th ACM SIGPLAN International
Conference on Functional Programming. ICFP ’08.
Siles, Vincent, & Herbelin, Hugo. (2012). Pure type system conversion is always typable. Journalof functional programming, 22(2), 153–180.
Sjöberg, Vilhelm, & Weirich, Stephanie. (2015). Programming up to congruence. Pages 369–
382 of: Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages. POPL ’15. New York, NY, USA: ACM.
Sjöberg, Vilhelm, Casinghino, Chris, Ahn, Ki Yung, Collins, Nathan, III, Harley D. Eades, Fu,
Peng, Kimmell, Garrin, Sheard, Tim, Stump, Aaron, & Weirich, Stephanie. (2012). Irrelevance,
heterogenous equality, and call-by-value dependent type systems. Pages 112–162 of: Fourthworkshop on Mathematically Structured Functional Programming (MSFP ’12). MSFP ’12.
Sjöberg, Vilhem. (2015). A dependently typed language with nontermination.
University of Pennsylvania.

Ph.D. thesis,

Stump, Aaron, Deters, Morgan, Petcher, Adam, Schiller, Todd, & Simpson, Timothy. (2008). Verified
programming in guru. Pages 49–58 of: Proceedings of the 3rd Workshop on Programming
Languages Meets Program Verification. PLPV ’09. New York, NY, USA: ACM.
Sulzmann, Martin, Chakravarty, Manuel M. T., Peyton Jones, Simon, & Donnelly, Kevin. (2007).
System f with type equality coercions. Pages 53–66 of: Proceedings of the 2007 ACM SIGPLAN
International Workshop on Types in Languages Design and Implementation. TLDI ’07. New York,NY, USA: ACM.
Swamy, Nikhil, Chen, Juan, Fournet, Cédric, Strub, Pierre-Yves, Bhargavan, Karthikeyan, & Yang,
Jean. (2011). Secure distributed programming with value-dependent types. Pages 266–278 of:Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming.
ICFP ’11. New York, NY, USA: ACM.
Swierstra, Wouter. (2008). Data types à la carte. Journal of functional programming, 18(4), 423–436.
The Coq development team. (2016). The coq proof assistant reference manual. Version 8.6.
van Benthem Jutting, L. S. (1993). Typing in pure type systems. Information and computation,105(1), 30–41.
van Doorn, Floris, Geuvers, Herman, & Wiedijk, Freek. (2013). Explicit convertibility proofs in puretype systems. Pages 25–36 of: Proceedings of the Eighth ACM SIGPLAN International Workshop
on Logical Frameworks & Meta-languages: Theory & Practice. LFMTP ’13. New York, NY,
USA: ACM.

ZU064-05-FPR

main

48

23 September 2019

10:36

Y. Yang and B. Oliveira

Wadler, Philip. (1995). Monads for functional programming. Pages 24–52 of: Jeuring, Johan,& Meijer, Erik (eds), Advanced Functional Programming. Berlin, Heidelberg: Springer Berlin
Heidelberg.
Weirich, Stephanie, Hsu, Justin, & Eisenberg, Richard A. (2013). System fc with explicit kindequality. Pages 275–286 of: Proceedings of the 18th ACM SIGPLAN International Conference
on Functional Programming. ICFP ’13. New York, NY, USA: ACM.
Weirich, Stephanie, Voizard, Antoine, de Amorim, Pedro Henrique Azevedo, & Eisenberg,
Richard A. (2017). A specification for dependent types in haskell. Proc. acm program. lang.,
1(ICFP), 31:1–31:29.
Wright, Andrew K., & Felleisen, Matthias. (1994). A syntactic approach to type soundness.
Information and computation, 115(1), 38–94.
Xi, Hongwei, Chen, Chiyan, & Chen, Gang. (2003). Guarded recursive datatype constructors.
Pages 224–235 of: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages. POPL ’03. New York, NY, USA: ACM.
Yang, Yanpeng, & Oliveira, Bruno C. d. S. (2017). Unifying typing and subtyping. Proc. acm
program. lang., 1(OOPSLA), 47:1–47:26.
Yang, Yanpeng, Bi, Xuan, & Oliveira, Bruno C. d. S. (2016). Unified syntax with iso-types. Pages
251–270 of: Igarashi, Atsushi (ed), Programming Languages and Systems. Cham: Springer
International Publishing.
Yorgey, Brent A., Weirich, Stephanie, Cretin, Julien, Peyton Jones, Simon, Vytiniotis, Dimitrios, &Magalhães, José Pedro. (2012). Giving haskell a promotion. Pages 53–66 of: Proceedings of the
8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. TLDI ’12. New
York, NY, USA: ACM.