Unified Syntax with Iso-Types
Yanpeng Yang, Xuan Bi, and Bruno C. d. S. Oliveira
The University of Hong Kong, Pokfulam, Hong Kong, China{ypyang,xbi,bruno}@cs.hku.hk

Abstract. Traditional designs for functional languages (such as Haskell
or ML) have separate sorts of syntax for terms and types. In contrast,
many dependently typed languages use a unified syntax that accounts
for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, andadded expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level oftype-level computation is present, as decidable type-checking is easily
lost.
This paper argues that the advantages of unified syntax also apply to
traditional functional languages, and there is no need to give up decidable
type-checking. We present a dependently typed calculus that uses unified
syntax, supports general recursion and has decidable type-checking. The
key to retain decidable type-checking is a generalization of iso-recursive
types called iso-types. Iso-types replace the conversion rule typically usedin dependently typed calculus, and make every computation explicit via
cast operators. We study two variants of the calculus that differ on the
reduction strategy employed by the cast operators, and give different
trade-offs in terms of simplicity and expressiveness.

1

Introduction

We live exciting times in the design of functional programming languages. In
recent years, dependent types have inspired novel designs for new programming
languages, such as Agda [19] or Idris [6], as well as numerous programming language research [2, 3, 8, 23–25, 28]. Dependently typed languages bring additional
expressiveness to type systems, and they can also support different forms ofassurances, such as strong normalization and logical consistency, not typicallypresent in traditional programming languages. Nevertheless, traditional designs
for functional languages still have some benefits. While strong normalization andlogical consistency are certainly nice properties to have, and can be valuable tohave in many domains, they can also impose restrictions 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. In contrast Haskell
or ML programmers can write their programs much more freely, since they do
not need to worry about retaining strong normalization and logical consistency.
Thus there is still plenty of space for both types of designs.

2

Y. Yang et al.

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 (mimicking value level application) may beneeded. 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 isneeded. Thus duplication can be avoided. Having less language constructs simplifies the language, making it easier to study (from the meta-theoretical pointof view) and maintain (from the implementation point of view).
In principle having unified syntax would be beneficial even for more traditional designs of functional languages, which have no strong normalization or
logical consistency. Not surprisingly, researchers have in the past considered suchan option for implementing functional languages [3, 7, 21], by using some variantof pure type systems (PTS) [5] (normally extended with general recursion). Thus,
with a simple and tiny calculus, they showed that powerful and quite expressivefunctional 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 and unrestricted general recursion [3,7] lose all threeproperties. For pragmatic reasons languages like Agda or Idris also allow turning
off the termination checker, which allows for added expressiveness, but loses thethree properties as well. More recently, various researchers [8, 24, 27] have been
investigating how to combine those properties, general recursion and dependent
types. However, this is usually done by having the type system carefully control the total and partial parts of computation, adding significant complexity tothose calculi when compared to systems based on pure type systems.
Nevertheless, if we are interested in traditional languages, only the loss ofdecidable type-checking is problematic. Unlike strong normalization and logicalconsistency, decidable type-checking is normally one property that is expectedfrom a traditional programming language design.
This paper proposes λI: a simple call-by-name variant of the calculus of
constructions. The key challenge solved in this work is how to define a calculus
comparable in simplicity to the calculus of constructions, while featuring bothgeneral recursion and decidable type checking. The main idea, is to recoverdecidable type-checking 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 typechecking is possible even in the presence of non-terminating programs at thetype level. At the same time term-level programs using general recursion work
as in any conventional functional languages, and can be non-terminating.

Unified Syntax with Iso-Types

3

Our design generalizes iso-recursive types [22], which are our main source ofinspiration. In λI, not only folding/unfolding of recursion at the type level is
explicitly controlled by term level constructs, but also any other type level computation (including beta reduction/expansion). There is an analogy to language
designs with equi-recursive types and iso-recursive types, which are normally thetwo options for adding recursive types to languages. With equi-recursive types,
type-level recursion is implicitly folded/unfolded, which makes establishing decidability of type-checking much more difficult. In iso-recursive designs, the idea
is to trade some convenience by a simple way to ensure decidability. Similarly, weview the design of traditional dependently typed calculi, such as the calculus of
constructions as analogous to systems with equi-recursive types. In the calculusof constructions it is the conversion rule that allows type-level computation toby implicitly triggered. However, the proof of decidability of type checking forthe calculus of constructions [10] (and other normalizing PTS) is non-trivial,
as it depends on strong normalization [16]. Moreover decidability is lost when
adding general recursion. In contrast, the cast operators in λI have to be used
to explicitly trigger each step of type-level computation, but it is easy to ensure
decidable type-checking, even with general recursion.
We study two variants of the calculus that differ on the reduction strategy
employed by the cast operators, and give different trade-offs in terms of simplicity
and expressiveness. The first variant λIw uses weak-head reduction in the castoperators. This allows for a very simple calculus, but loses some expressivenessin terms of type level computation. Nevertheless in this variant it is still possible
to encode useful language constructs such as algebraic datatypes. The second
variant λIp uses parallel reduction for casts and is more expressive. It allows
equating terms such as Vec (1 + 1) and Vec 2 as equal. The price to pay forthis more expressive design is some additional complexity. For both designs typesoundness and decidability of type-checking are proved.
It is worth emphasizing that λI does sacrifice some convenience when performing type-level computations in order to gain the ability of doing arbitrary
general recursion at the term level. The goal of this work is to show the benefitsof unified syntax in terms of economy of concepts for programming language design, and not use unified syntax to express computationally intensive type-level
programs. Investigating how to express computationally intensive type-level programs (as in dependently typed programming) in λI is left for future work.
In summary, the contributions of this work are:
– The λI calculus: A simple calculus for functional programming, that collapses terms, types and kinds into the same hierarchy and supports generalrecursion. λI is type-safe and the type system is decidable. Full proofs areprovided in the extended version of this paper [29].
– Iso-types: λI generalizes iso-recursive types by making all type-level computation steps explicit via casts operators. In λI the combination of casts
and recursion subsumes iso-recursive types.
– A prototype implementation: The prototype of λI is available online1 .
1https://bitbucket.org/ypyang/aplas16

4

2

Y. Yang et al.

Overview

In this section, we informally introduce the main features of λI. In particular,
we show how the casts in λI can be used instead of the typical conversion rulepresent in calculi such as the calculus of constructions. The formal details of λI
are presented in Section 3 and 4.
2.1

The Calculus of Constructions and the Conversion Rule

The calculus of constructions (λC) [10] is a higher-order typed lambda calculus
supporting dependent types (among various other features). A crucial feature of
λC is the conversion rule:Γ ` e : τ1

Γ ` τ2 : sΓ ` e : τ2

τ1 =β τ2

It allows one to derive e : τ2 from the derivation of e : τ1 and the beta equalityof τ1 and τ2 . This rule is important to automatically allow terms with beta
equivalent types to be considered type-compatible. For example, consider thefollowing identity function:f = λy : (λ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 ((λx : ?. x ) Int). Note that the beta equivalence(λx : ?. x ) Int =β Int holds. The conversion 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 λC brings a lot of convenience, an unfortunate consequence is that it couples decidability of type checking with strong normalization of the calculus [16].
Therefore adding general recursion to λC becomes difficult, since strong normalization is lost. Due to the conversion rule, any non-terminating term would
force the type checker to go into an infinite loop (by constantly applying theconversion rule without termination), thus rendering the type system undecidable. For example, assume a term z that has type loop, where loop stands for any
diverging computation. If we type check (λx : Int. x ) z under the normal typing
rules of λC, the type checker would get stuck as it tries to do beta equality on
two terms: Int and loop, where the latter is non-terminating.
2.2

An Alternative to the Conversion Rule: Iso-Types

In contrast to the conversion rule of λC, λI features iso-types, making it explicit
as to when and where to convert one type to another. Type conversions are
explicitly controlled by two language constructs: cast↓ (one-step reduction) andcast↑ (one-step expansion). The benefit of this approach is that decidability oftype checking is no longer coupled with strong normalization of the calculus.

Unified Syntax with Iso-Types

5

Reduction. The cast↓ operator allows a type conversion provided that the resulting type is a reduction of the original type of the term. To explain the useof cast↓ , assume an identity function g defined by g = λy : Int. y and a terme such that e : (λx : ?. x ) Int. In contrast to λC, we cannot directly apply gto e in λI since the type of e ((λx : ?. x ) Int) is not syntactically equal to Int.
However, note that the reduction relation (λx : ?. x ) Int −→ Int holds. We canuse 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 use of cast↑ , let us revisit the example from Section 2.1. We
cannot apply f to 3 without the conversion rule. Instead, we can use cast↑ toexpand the type of 3:(cast↑ [(λx : ?. x ) Int] 3) : (λx : ?. x ) Int
Thus, the application f (cast↑ [(λx : ?. x ) Int] 3) becomes well-typed. Intuitively,
cast↑ performs expansion, as the type of 3 is Int, and (λx : ?. x ) Int is the
expansion of Int witnessed by (λx : ?. x ) Int −→ Int. Notice that for cast↑ towork, we need to provide the resulting type as argument. This is because for thesame 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 rules allow only one-step reduction or expansion. If two
type-level terms require more than one step of reductions or expansions for normalization, then multiple casts must be used. Consider a variant of the example
such that e : (λx : ?. λy : ?. x ) Int Bool . Given g = λy : Int. y, the expression
g (cast↓ e) is ill-typed because cast↓ e has type (λy : ?. Int) Bool , which is notsyntactically equal to Int. Thus, we need another cast↓ :cast↓ (cast↓ e) : Intto further reduce the type and allow the program g (cast↓ (cast↓ e)) to type check.
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 presenceof non-termination at type level. Consider the same example using the termz from Section 2.1. This time the type checker will not get stuck when typechecking (λx : Int. x ) z . This is because in λI, the type checker only performs
syntactic comparison between Int and loop, instead of beta equality. Thus itrejects the above application as ill-typed. Indeed it is impossible to type checksuch application even with the use of cast↑ and/or cast↓ : one would need towrite infinite number of cast↓ ’s to make the type checker loop forever (e.g.,(λx : Int. x )(cast↓ (cast↓ . . . z))). But it is impossible to write such program inpractice.

6

Y. Yang et al.

Variants of Casts. A reduction relation is used in cast operators to convert types.
We study two possible reduction relations: call-by-name weak-head reduction andfull reduction. Weak-head reduction cannot reduce sub-terms at certain positions(e.g., inside λ or Π binders), while full reduction can reduce sub-terms at any
position. We define two variants of casts, namely weak and full casts, by employing weak-head and full reduction respectively. We also create two variants of λI,
namely λIw and λIp . The only difference is that λIw uses weak-head reduction
in weak cast operators cast↑ and cast↓ , while λIp uses full reduction, specificallyparallel reduction, in full cast operators cast⇑ and cast⇓ . Both variants reflect
the idea of iso-types, but have trade-offs between simplicity and expressiveness:λIw uses the same call-by-name reduction for both casts and evaluation to keep
the system and metatheory simple, but loses some expressiveness, e.g. cannot
convert Vec (1 + 1) to Vec 2. λIp is more expressive but results in a more complicated metatheory (see Section 4.2). Note that when generally referring to λI,
we do not specify the reduction strategy, which could be either variant.
2.3

General Recursion

λI supports general recursion and allows writing unrestricted recursive programs
at term level. The recursive construct is also used to model recursive types attype level. Recursive terms and types are represented by the same µ primitive.
Recursive Terms. The primitive µx : τ. e can be used to define recursive functions. For example, the factorial function would be written as:fact = µf : Int → Int. λx : Int. if x == 0 then 1 else x × f (x − 1)
We treat the µ operator as a fixpoint, which evaluates µx : τ. e to its recursive
unfolding e[x 7→ µx : τ. e]. Term-level recursion in λI works as in any standard
functional language, e.g., fact 3 produces 6 as expected (see Section 3.4).
Recursive Types. The same µ primitive is used at the type level to represent
iso-recursive types [11]. 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. In λI, such isomorphism is witnessedby cast↑ and cast↓ . In fact, cast↑ and cast↓ generalize fold and unfold: they canconvert any types, not just recursive types, as we shall see in the example ofencoding parametrized datatypes in Section 5.

3

Dependent Types with Iso-Types

In this section, we present the λIw calculus, which uses a (call-by-name) weakhead reduction strategy in casts. This calculus is very close to the calculus of
constructions, except for three key differences: 1) the absence of the  constant(due to use of the “type-in-type” axiom); 2) the existence of two cast operators;

Unified Syntax with Iso-Types

73) general recursion on both term and type level. Unlike λC the proof of decidability of type checking for λIw does not require the strong normalization of
the calculus. Thus, the addition of general recursion does not break decidable
type checking. In the rest of this section, we demonstrate the syntax, operationalsemantics, typing rules and metatheory of λIw . Full proofs of the meta-theory
can be found in the extended version of this paper [29].

3.1

SyntaxFigure 1 shows the syntax of λIw , including expressions, contexts and values. λIw
uses a unified representation for different syntactic levels by following the puretype system (PTS) representation of λC [5]. There is no syntactic distinction
between terms, types or kinds. We further merge types and kinds together by
including only a single sort ? instead of two distinct sorts ? and  of λC. This
design brings economy for type checking, since one set of rules can cover all
syntactic levels. We use metavariables τ and σ for an expression on the typelevel position and e for one on the term level. We use τ1 → τ2 as a syntactic
sugar for Πx : τ1 . τ2 if x does not occur free in τ2 .
Explicit Type Conversion. We introduce two new primitives cast↑ and cast↓(pronounced as “cast up” and “cast down”) to replace the implicit conversion
rule of λC with one-step explicit type conversions. The type-conversions perform
two directions of conversion: cast↓ is for the one-step reduction of types, and cast↑is for the one-step expansion. The cast↑ construct takes a type parameter τ as
the result type of one-step expansion for disambiguation (see also Section 2.2).
The cast↓ construct does not need a type parameter, because the result type of
one-step reduction is uniquely determined, as we shall see in Section 3.5.
We use syntactic sugar castn↑ and castn↓ to denote n consecutive cast operators(see Figure 1). Alternatively, we can introduce them as built-in operators but
treat one-step casts as syntactic sugar instead. Making n-step casts built-in can
reduce the number of individual cast constructs, but makes cast operators lessfundamental in the discussion of meta-theory. Thus, in the paper, we treat n-step
casts as syntactic sugar but make them built-in in the implementation for better
performance. Note that castn↑ is simplified to take just one type parameter, i.e.,
the last type τ1 of the n cast operations. Due to the determinacy of one-step
reduction (see Lemma 1), the intermediate types can be uniquely determined,
thus can be left out from the castn↑ operator.
General Recursion. We add one primitive µ to represent general recursion. It hasa uniform representation on both term level and type level: the same construct
works both as a term-level fixpoint and a recursive type. The recursive expressionµx : τ. e is polymorphic, in the sense that τ is not restricted to ? but can be any
type, such as a function type Int → Int or a kind ? → ?.

8

Y. Yang et al.
Expressionse, τ, σ ::= x | ? | e1 e2 | λx : τ. e | Πx : τ1 . τ2
| µx : τ. e | cast↑ [τ ] e | cast↓ eΓ ::= ∅ | Γ, x : τv ::= ? | λx : τ. e | Πx : τ1 . τ2 | cast↑ [τ ] v

Contexts
ValuesSyntactic Sugar
τ1 → τ2, Πx : τ1 . τ2 , where x 6∈ FV(τ2 )castn↑ [τ1 ] e , cast↑ [τ1 ](cast↑ [τ2 ](. . . (cast↑ [τn ] e) . . . )), where τ1 −→ τ2 −→ · · · −→ τn
castn
e
,
cast↓ (cast↓ (. . . (cast↓ e) . . . ))
↓
|
{z
}
n

Fig. 1. Syntax of λIw
e −→ e 0

One-step Weak-head Reduction(λx : τ. e1 ) e2 −→ e1 [x 7→ e2 ]S Mu

µx : τ. e −→ e[x 7→ µx : τ. e]e −→ e 0
S CastUp
cast↑ [τ ] e −→ cast↑ [τ ] e 0

e1 −→ e10
S App
e1 e2 −→ e10 e20e −→ eS CastDown
cast↓ e −→ cast↓ e 0

S Betacast↓ (cast↑ [τ ] v ) −→ v

S CastElim

Fig. 2. Operational semantics of λIw

3.2

Operational Semantics

Figure 2 shows the small-step, call-by-name operational semantics. Three basecases include S Beta for beta reduction, S Mu for recursion unrolling and
S CastElim for cast canceling. Three inductive cases, S App, S CastDown
and S CastUp, define reduction at the head position of an application, and theinner expression of cast↓ and cast↑ terms, respectively. Note that S CastElim
and S CastDown do not overlap because in the former rule, the inner term ofcast↓ is a value (see Figure 1), i.e., cast↑ [τ ] v , but not a value in the latter rule.
The reduction rules are called weak-head because only the head term of an
application can be reduced, as indicated by the rule S App. Reduction is also notallowed inside the λ-term and Π-term which are both defined as values. Weakhead reduction rules are used for both type conversion and term evaluation.
Thus, we refer to cast operators in λIw as weak casts. To evaluate the value ofa 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 onestep reduction.
3.3

TypingFigure 3 gives the syntax-directed typing rules of λIw , including rules of context
well-formedness ` Γ and expression typing Γ ` e : τ . Note that there is onlya single set of rules for expression typing, because there is no distinction ofdifferent syntactic levels.

Unified Syntax with Iso-Types

9

Most typing rules are quite standard. We write ` Γ if a context Γ is wellformed. We use Γ ` τ : ? to check if τ is a well-formed type. Rule T Ax
is the “type-in-type” axiom. Rule T Var checks the type of variable x fromthe valid context. Rules T App and T Lam check the validity of application
and abstraction respectively. Rule T Pi checks the type well-formedness of thedependent function. Rule T Mu checks the validity of a recursive term. It ensuresthat the recursion µx : τ. e should have the same type τ as the binder x andalso the inner expression e.
The Cast Rules. We focus on the rules T CastUp and T CastDown thatdefine the semantics of cast operators and replace the conversion rule of λC.
The relation between the original and converted type is defined by one-stepweak-head reduction (see Figure 2). For example, given a judgment Γ ` e : τ2and relation τ1 −→ τ2 −→ τ3 , cast↑ [τ1 ] e expands the type of e from τ2 to τ1 ,while cast↓ e reduces the type of e from τ2 to τ3 . We can formally give the typing
derivations of the examples in Section 2.2:Γ ` e : (λx : ?. x ) Int(λx : ?. x ) Int −→ Int
Γ ` (cast↓ e) : IntΓ ` 3 : IntΓ ` (λx : ?. x ) Int : ?
(λx : ?. x ) Int −→ Int
Γ ` (cast↑ [(λx : ?. x ) Int] 3) : (λx : ?. x ) Int

Importantly, in λIw term-level and type-level computation are treated differently.
Term-level computation is dealt in the usual way, by using multi-step reduction
until a value is finally obtained. Type-level computation, on the other hand, iscontrolled by the program: each step of the computation is induced by a cast. If
a type-level program requires n steps of computation to reach the normal form,
then it will require n casts to compute a type-level value.
Pros and Cons of Type in Type. The “type-in-type” axiom is well-known to giverise to logical inconsistency [14]. However, since our goal is to investigate corelanguages for languages that are logically inconsistent anyway (due to generalrecursion), we do not view “type-in-type” as a problematic rule. On the other
hand the rule T Ax brings additional expressiveness and benefits: for example
kind polymorphism [30] is supported in λIw .
Syntactic Equality. Finally, the definition of type equality in λIw differs from
λC. Without λC’s conversion rule, the type of a term cannot be converted freely
against beta equality, unless using cast operators. Thus, types of expressions areequal only if they are syntactically equal (up to alpha renaming).
3.4

The Two Faces of Recursion

Term-level Recursion. In λIw , the µ-operator works as a fixpoint on the termlevel. By rule S Mu, evaluating a term µx : τ. e will substitute all x ’s in e withthe whole µ-term itself, resulting in the unrolling e[x 7→ µx : τ. e] . The µ-term
is equivalent to a recursive function that should be allowed to unroll without

10

Y. Yang et al.

`Γ

Well-formed Context

Γ `e:τ

Typing`∅`ΓΓ `τ :?
Env Var` Γ, x : τ`Γ

x :τ ∈ Γ
T VarΓ `x :τ

Env Empty`ΓT AxΓ `?:?

Γ ` e1 : Πx : τ2 . τ1
Γ ` e2 : τ2
Γ, x : τ1 ` e : τ2
Γ ` Πx : τ1 . τ2 : ?
T App
T Lam
Γ ` e1 e2 : τ1 [x 7→ e2 ]Γ ` λx : τ1 . e : Πx : τ1 . τ2
Γ ` τ1 : ?
Γ, x : τ1 ` τ2 : ?
Γ, x : τ ` e : τΓ `τ :?
T Pi
T Mu
Γ ` Πx : τ1 . τ2 : ?
Γ ` µx : τ. e : τΓ ` e : τ1
τ1 −→ τ2Γ ` e : τ2
Γ ` τ1 : ?
τ1 −→ τ2
T CastUp
T CastDownΓ ` cast↑ [τ1 ] e : τ1
Γ ` cast↓ e : τ2

Fig. 3. Typing rules of λIw

restriction. Recall the factorial function example in Section 2.3. By rule T Mu,
the type of fact is Int → Int. Thus we can apply fact to an integer. Note thatby rule S Mu, fact will be unrolled to a λ-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−→ (λx : Int. if x == 0 then 1 else x × fact (x − 1)) 3 -- by S App−→ if 3 == 0 then 1 else 3 × fact (3 − 1)-- by S Beta−→ · · · −→ 6
Note that we never check if a µ-term can terminate or not, which is anundecidable problem for general recursive terms. The factorial function example
above can stop, while there exist some terms that will loop forever. However,term-level non-termination is only a runtime concern and does not block thetype checker. In Section 3.5 we show type checking λIw is still decidable in thepresence of general recursion.
Type-level Recursion. On the type level, µx : τ. e works as a iso-recursivetype [11], 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 forthe iso-recursive type to map back and forth between the original and unrolled
form. Assuming there exist expressions e1 and e2 such that e1 : µx : τ. σ ande2 : σ[x 7→ µx : τ. σ] , we have the following typing results:
unfold e1: σ[x 7→ µx : τ. σ]fold [µx : τ. σ] e2 : µx : τ. σ
by applying standard typing rules of iso-recursive types [22]:Γ ` e1 : µx : τ. σΓ ` unfold e1 : σ[x 7→ µx : τ. σ]

Γ ` µx : τ. σ : ?
Γ ` e2 : σ[x 7→ µx : τ. σ]Γ ` fold [µx : τ. σ] e2 : µx : τ. σ

Unified Syntax with Iso-Types

11

However, in λIw we do not need to introduce fold and unfold operators, because with the rule S Mu, cast↑ and cast↓ generalize fold and unfold. Consider
the same expressions e1 and e2 above. The type of e2 is the unrolling of e1 ’stype, which follows the one-step reduction relation by rule S Mu: µx : τ. σ −→σ[x 7→ µx : τ. σ] . By applying rules T CastUp and T CastDown, we canobtain the following typing results:
cast↓ e1
: σ[x 7→ µx : τ. σ]cast↑ [µx : τ. σ] e2 : µx : τ. σThus, cast↑ and cast↓ witness the isomorphism between the original recursivetype and its unrolling, behaving in the same way as fold and unfold in isorecursive types.
An important remark is that casts are necessary, not only for controlling theunrolling of recursive types, but also for type conversion of other constructs,
which is essential for encoding parametrized algebraic datatypes (see Section 5).
Also, the “type-in-type” axiom [7] makes it possible to encode fixpoints even
without a fixpoint primitive, i.e., the µ-operator. Thus if no casts would be
performed on terms without recursive types, it would still be possible to build aterm with a non-terminating type and make type-checking non-terminating.
3.5

Metatheory

We now discuss the metatheory of λIw . We focus on two properties: the decidability of type checking and the type safety of the language. First, we show thattype checking λIw is decidable without requiring strong normalization. Second,
the language is type-safe, proven by subject reduction and progress theorems.
Decidability of Type Checking. 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
rules T CastUp and T CastDown. Both rules contain a premise that needs
to judge if two types τ1 and τ2 follow the one-step reduction, i.e., if τ1 −→ τ2holds. We show that τ2 is unique with respect to the one-step reduction, or
equivalently, reducing τ1 by one step will get only a sole result τ2 . Such property
is given by the following lemma:
Lemma 1 (Determinacy of One-step Weak-head Reduction). If e −→e1 and e −→ e2 , then e1 ≡ e2 .
We use the notation ≡ to denote the alpha equivalence of e1 and e2 . Note thatthe presence of recursion does not affect this lemma: given a recursive term µx :τ. e, by rule S Mu, there always exists a unique term e 0 ≡ e[x 7→ µx : τ. e] suchthat µx : τ. e −→ e 0 . With this result, we show it is decidable to check whether
the one-step relation τ1 −→ τ2 holds. We first reduce τ1 by one step to obtain τ10(which is unique by Lemma 1), and compare if τ10 and τ2 are syntactically equal.
Thus, we can further show type checking cast-terms is decidable.

12

Y. Yang et al.

For other forms of terms, the typing rules only contain typing judgments inthe premises. Thus, type checking is decidable by the induction hypothesis andthe following lemma which ensures the typing result is unique:
Lemma 2 (Uniqueness of Typing for λIw ). If Γ ` e : τ1 and Γ ` e : τ2 ,then τ1 ≡ τ2 .
Thus, we can conclude the decidability of type checking:
Theorem 1 (Decidability of Type Checking for λIw ). Given a well-formed
context Γ and a term e, it is decidable to determine if there exists τ such thatΓ ` e : τ.
We emphasize that when proving the decidability of type checking, we do
not rely on strong normalization. Intuitively, explicit type conversion rules use
one-step weak-head reduction, which already has a decidable checking algorithm
according to Lemma 1. We do not need to further require the normalization ofterms. This is different from the proof for λC which requires the language to bestrongly normalizing [16]. In λC the conversion rule needs to examine the beta
equivalence of terms, which is decidable only if every term has a normal form.
Type Safety. The proof of the type safety of λIw is by showing subject reduction
and progress theorems:
Theorem 2 (Subject Reduction of λIw ). If Γ ` e : σ and e −→ e0 thenΓ ` e 0 : σ.
Theorem 3 (Progress of λIw ). If ∅ ` e : σ then either e is a value v or there
exists e 0 such that e −→ e 0 .
The proof of subject reduction is straightforward by induction on the derivation of e −→ e0 . Some cases need supporting lemmas: S CastElim requires
Lemma 1; S Beta and S Mu require the following substitution lemma:
Lemma 3 (Substitution of λIw ). If Γ1 , x : σ, Γ2 ` e1 : τ and Γ1 ` e2 : σ,then Γ1 , Γ2 [x 7→ e2 ] ` e1 [x 7→ e2 ] : τ [x 7→ e2 ] .
The proof of progress is also standard by induction on ∅ ` e : σ. Noticethat cast↑ [τ ] v is a value, while cast↓ e1 is not: by rule S CastDown, e1 will
be constantly reduced until it becomes a value that could only be in the form
cast↑ [τ ] v by typing rule T CastDown. Then rule S CastElim can be further
applied and the evaluation does not get stuck. Another notable remark is thatwhen proving the case for application e1 e2 , if e1 is a value, it could only be a
λ-term but not a cast↑ -term. Otherwise, suppose e1 has the form cast↑ [Πx :τ1 . τ2 ] e10 . By inversion, we have ∅ ` e10 : τ10 and Πx : τ1 . τ2 −→ τ10 . But such τ10does not exist because Πx : τ1 . τ2 is a value which is not reducible.

Unified Syntax with Iso-Typesr −→p r 0

13

One-step Parallel Reduction

x −→p x

P Var

? −→p ?

P StarP Beta(λx : ρ. r1 ) r2 −→p r1 [x 7→ r2 ]r1 −→p r10
r2 −→p r20
P App
P MuBetaµx : ρ. r −→p r [x 7→ µx : ρ. r ]r1 r2 −→p r10 r20
ρ −→p ρ0r −→p r 0
ρ1 −→p ρ01
ρ2 −→p ρ02
P Pi
0
0 P Lam
λx : ρ. r −→p λx : ρ . r
Πx : ρ1 . ρ2 −→p Πx : ρ01 . ρ0200ρ −→p ρr −→p rP Mu
µx : ρ. r −→p µx : ρ0 . r 0
Fig. 4. One-step parallel reduction of erased terms

4

Iso-Types with Full Casts

In Section 3, casts use one-step weak-head reduction, which is also used by term
evaluation and simplifies the design. To gain extra expressiveness, we take one
step further to generalize casts with full reduction. In this section, we present avariant of λI called λIp , where casts use parallel reduction for type conversion.
Full specification and proofs can be found in the extended version [29].
4.1

Full Casts with Parallel Reduction

Using weak-head reduction in cast operators keeps the simplicity of the language
design. However, it lacks the ability to do full type-level computation, because
reduction cannot occur at certain positions of terms. For example, weak casts
cannot convert the type Vec (1 + 1) to Vec 2 since the desired reduction is at the
non-head position. Thus, we generalize weak casts to full casts (cast⇑ and cast⇓ )utilizing one-step parallel reduction (−→p ) for type conversion. Figure 4 shows
the definition of −→p . It allows to reduce terms at any position, e.g., non-head
positions or inside binders λx : ?. 1+1 −→p λx : ?. 2, thus enables full type-levelcomputation for casts.
There are three remarks for parallel reduction worth mentioning. First, parallel reduction is defined up to erasure, a process that removes all casts fromterms (see Figure 5). We use metavariable r and ρ to range over erased terms
and types, respectively. The only syntactic change of erased terms is that there
is no cast. The syntax is omitted here and can be found in the extended version [29]. It is feasible to define parallel reduction only for erased terms because
casts in λIp (also λIw ) are only used to ensure the decidability of type checking
and have no effect on dynamic semantics, thus are computationally irrelevant.
Second, the definition of parallel reduction in Figure 4 is slightly different
from the standard one for PTS [1]. It is partially parallel: rules P Beta andP MuBeta do not parallel reduce sub-terms but only do beta reduction andrecursion unrolling, respectively. Such definition makes the decidability property(see Lemma 6) easier to prove than the conventional fully parallel version. It also
requires fewer reduction steps than the non-parallel version, thus correspondingly
needs fewer casts.

14

Y. Yang et al.

Erased Expressions r , ρErasure
|x|
=x
|?|
=?
|e1 e2 |= |e1 | |e2 ||λx : τ. e| = λx : |τ |. |e||Πx : τ1 . τ2 | = Πx : |τ1 |. |τ2 ||µx : τ. e| = µx : |τ |. |e||cast⇑ [τ ] e| = |e||cast⇓ [τ ] e| = |e|Fig. 5. Erasure of casts

Erased Values
u ::= ? | λx : ρ. r | Πx : ρ1 . ρ2
Evaluation Rules(λx : ρ. r1 ) r2 −→ r1 [x 7→ r2 ]r1 −→ r10
r1 r2 −→ r10 r2µx : ρ. r −→ r [x 7→ µx : ρ. r ]Fig. 6. Values and evaluation rules of erased termse, τ, σ ::= · · · | cast⇑ [τ ] e | cast⇓ [τ ] ev ::= · · · | cast⇑ [τ ] v | cast⇓ [τ ] v

Expressions
ValuesTypingΓ ` e : τ2

Γ ` τ1 : ?

|τ1 | −→p |τ2 |Γ ` cast⇑ [τ1 ] e : τ1Γ ` e : τ1

Γ ` τ2 : ?

TF CastUp|τ1 | −→p |τ2 |Γ ` cast⇓ [τ2 ] e : τ2

TF CastDown

Fig. 7. Syntactic and typing changes of λIp

Third, parallel reduction does not have the determinacy property like weakhead reduction (Lemma 1). For example, for term (λx : ?. 1 + 1) Int, we can(parallel) reduce it to either (λx : ?. 2) Int by rule P App and P Lam, or 1 + 1
by rule P Beta. Thus, to ensure the decidability, we also need to add the type
annotation for cast⇓ operator to indicate what exact type we want to reduce to.
Similar to cast⇑ , cast⇓ [τ ] v is a value, which is different from the weak cast↓ -term.
Figure 7 shows the syntactic and typing changes of λIp . Notice that in λIw ,reduction rules for type casting and term evaluation are the same, i.e., the weakhead call-by-name reduction. But in λIp , parallel reduction is only used by casts.
We define weak-head reduction (−→) for term evaluation individually (see Figure6). Note that the relation −→ is defined only for erased terms, which is similar to
the treatment of −→p . We also define syntactic values for erased terms, ranged
over by u (see Figure 6).
4.2

Metatheory

We show that the two key properties, type safety and decidability of type checking, still hold in λIp .
Type Safety. Full casts are more expressive but also complicate the metatheory:term evaluation could get stuck by full casts. For example, the following term,(cast⇓ [Int → Int] (λx : ((λy : ?. y) Int). x )) 3

Unified Syntax with Iso-Types

15

cannot be further reduced because the head position is already a value but nota λ-term. Note that weak casts do not have such problem because only cast↑ isannotated and not legal to have a Π-type in the annotation (see last paragraphof Section 3.5). To avoid getting stuck by full casts, one could introduce several
cast push rules similar to System FC [26]. For example, the stuck term above
can be further evaluated by pushing cast⇓ into the λ-term:(cast⇓ [Int → Int] (λx : ((λy : ?. y) Int). x )) 3 −→ (λx : Int. x ) 3
However, adding “push rules” significantly complicates the reduction relations and metatheory. Instead, we adopt the erasure approach inspired by Zombie [24] and Guru [25] that removes all casts when proving the type safety. We
define a type system for erased terms, called erased system. Its typing judgment
is ∆ ` r : ρ where ∆ ranges over the erased context. Omitted typing rules areavailable in the extended version [29].
The erased system is basically calculus of constructions with recursion and“type-in-type”. Thus, we follow the standard proof steps for PTS [5]. Noticethat 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 .
Lemma 4 (Substitution of Erased System). If ∆1 , x : ρ0 , ∆2 ` r1 : ρ and∆1 ` r2 : ρ0 , then ∆1 , ∆2 [x 7→ r2 ] ` r1 [x 7→ r2 ] : ρ[x 7→ r2 ] .
Theorem 4 (Subject Reduction of Erased System). If ∆ ` r : ρ andr −→p r 0 then ∆ ` r 0 : ρ.
Theorem 5 (Progress of Erased System). If ∅ ` r : ρ then either r is avalue u or there exists r 0 such that r −→ r 0 .
Given that the erased system is type-safe, if we want to show the type-safetyof the original system, it is sufficient to show the typing is preserved after erasure:Lemma 5 (Soundness of Erasure). If Γ ` e : τ then |Γ | ` |e| : |τ |.
Decidability of Type Checking. The proof of decidability of type checking λIp issimilar to λIw in Section 3.5. The only difference is for cast rules TF CastUp
and TF CastDown, which use parallel reduction |τ1 | −→p |τ2 | as a premise.
We first show the decidability of parallel reduction:
Lemma 6 (Decidability of Parallel Reduction). If ∆ ` r1 : ρ1 and ∆ `r2 : ρ2 , then whether r1 −→p r2 holds is decidable.
As cast⇑ and cast⇓ are annotated, both τ1 and τ2 can be determined andthe well-typedness is checked in the original system. By Lemma 5, the erased
terms keeps the well-typedness. Thus, by Lemma 6, it is decidable to check if|τ1 | −→p |τ2 |. We conclude the decidability of type checking by following lemmas:

16

Y. Yang et al.

Lemma 7 (Uniqueness of Typing for λIp ). If Γ ` e : τ1 and Γ ` e : τ2 ,then τ1 ≡ τ2 .
Theorem 6 (Decidability of Type Checking for λIp ). Given a well-formed
context Γ and a term e, it is decidable to determine if there exists τ such thatΓ ` e : τ.

5

Application of Iso-Types

λI is a simple core calculus, but expressive enough to encode useful language
constructs. We have implemented a simple functional language Fun to show
how features of modern functional languages can be encoded in λI. We focus oncommon features available in traditional functional languages and some interesting type-level features, but not the full power of dependent types. Supported
features include algebraic datatypes, records, higher-kinded types, kind polymorphism [30] and datatype promotion [30].
Due to lack of space, many examples illustrating the various language features
supported in Fun are provided only in the extended version [29]. Here we show
the essential idea of how to exploit iso-types to encode language constructs.
Encoding Parametrized Algebraic Datatypes with Weak Casts. We give an example of encoding parametrized algebraic datatypes in λIw via µ-operator andweak casts. Importantly we should note that having iso-recursive types alone(and alpha equality) would be insufficient to encode parametrized types: thegeneralization afforded by iso-types is needed here. In Fun we can define polymorphic list as:
data List a = Nil | Cons a (List a);This Fun definition is translated into λIw using a Scott encoding [18] of datatypes:
List = µL : ? → ?. λa : ?. Πb : ?. b → (a → L a → b) → b
Nil = λa : ?. cast2↑ [List a ] (λb : ?. λn : b. λc : (a → List a → b). n)Cons = λa : ?. λx : a. λ(xs : List a).
cast2↑ [List a ] (λb : ?. λn : b. λc : (a → List a → b). c x xs)
The type constructor List is encoded as a recursive type. The body is a type-level
function that takes a type parameter a and returns a dependent function type,i.e., Π-type. The body of Π-type is universally quantified by a type parameter b,which represents the result type 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 Consare encoded as functions. Each of them selects a different function from theparameters (n and c). This provides branching in the process flow, based on
the constructors. Note that cast↑ is used twice here (written as cast2↑ ): one forone-step expansion from τ to (λa : ?. τ ) a and the other for folding the recursivetype from (λa : ?. τ ) a to List a, where τ is the type of cast2↑ body.

Unified Syntax with Iso-Types

17

We have two notable remarks from the example above. First, iso-types are
critical for the encoding and cannot be replaced by iso-recursive types. Since type
constructors are parameterized, not only folding/unfolding recursive types, butalso type-level reduction/expansion is required, which is only possible with casts.
Second, though weak casts are not as powerful as full casts, they are capable ofencoding many useful constructs, such as algebraic datatypes and records [29].
Nevertheless full-reduction casts enable other important applications. Some applications of full casts are discussed in the extended version [29].

6Related Work

Core calculus for functional languages. Girard’s System Fω [14] is a typed
lambda calculus with higher-kinded polymorphism. For the well-formedness oftype expressions, an extra level of kinds is added to the system. In comparison,because of unified syntax, λI is considerably simpler than System Fω , both interms of language constructs and complexity of proofs. As for type-level computation, System Fω differs from λI in that it uses a conversion rule, while λI
uses explicit casts. The current core language for GHC Haskell, System FC [26]is a significant extension of System Fω , which supports GADTs [20], functional
dependencies [15], type families [13], and kind equality [28]. These features use
a non-trivial form of type equality, which is currently missing from λI. On theother hand, λI uses unified syntax and has only 8 language constructs, whereas
System FC uses multiple levels of syntax and currently has over 30 language
constructs, making it significantly more complex. One direction of our future
work is to investigate the addition of such forms of non-trivial type-equality.
Unified syntax with decidable type-checking. Pure Type Systems [4] show how awhole family of type systems can be implemented using just a single syntactic
form. PTSs are an obvious source of inspiration for our work. Although thispaper presents a specific system based on λC, it should be easy to generalize
λI in the same way as PTSs and further show the applicability of our ideas toother systems. An early attempt of using a PTS-like syntax for an intermediate
language for functional programming was Henk [21]. The Henk proposal was touse the lambda cube as a typed intermediate language, unifying all three levels.
However the authors have not studied the addition of general recursion nor fulldependent types.
Zombie [8] 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 (witharound 24 language constructs) as it tries to be both consistent as a logic andpragmatic as a programming language. Even if one is only interested in modelinga programmatic fragment, additional mechanisms are required to ensure thevalidity of proofs, e.g., call-by-value semantics and value restriction [23, 24]. In
contrast to Zombie, λI takes another point of the design space, giving up logicalconsistency and reasoning about proofs for simplicity in the language design.

18

Y. Yang et al.

Unified syntax with general recursion and undecidable type checking. Cayenne [3]integrates the full power of dependent types with general recursion, which bears
some similarities with λI. It uses one syntactic form for both terms and types,
allows arbitrary computation at type level and is logically inconsistent becauseof allowing unrestricted recursion. However, the most crucial difference from λI
is that 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 [7] also featuresgeneral recursion to implement equi-recursive types. Recursion and recursive
types are unified in a single construct. However, both equi-recursive types andthe Type:Type axiom make the type system undecidable. ΠΣ [2] is anotherexample of a language that uses one recursion mechanism for both types andfunctions. The type-level recursion is controlled by lifted types and boxes since
definitions are not unfolded inside boxes. However, ΠΣ does not have decidable type checking due to the “type-in-type” axiom. And its metatheory is notformally developed.
Casts for managed type-level computation. Type-level computation in λI is controlled by explicit casts. Several studies [12,17,23–26] 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 λI do not. The need for equality proof terms complicates the language design because: 1) building equality proofs requires various other language
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 [25] and Sep3 [17] make syntactic separation between
proofs and programs to prevent certain programmatic terms turning into invalid
proofs. The programmatic part of Zombie [23,24], which has no such separation,
employs value restriction that restricts proofs to be syntactic values to avoid
non-terminating terms. PTS with convertibility proofs (PTSf ) [12] extends PTS
by replacing the implicit conversion rule with explicit conversion proofs embedded into terms. However, it requires many language constructs to build equality
proofs; and it does not allow general recursion, thus does not need to deal withproblem 2). Our treatment of full casts in λIp , using a separate erased systemfor developing metatheory, is similar to the approach of Zombie or Guru whichuses an unannotated system.
Restricted recursion with termination checking. As proof assistants, dependently
typed languages such as Coq [9] and Adga [19] are conservative as to what kindof computation is allowed. They require all programs to terminate by means ofa termination checker, ensuring recursive calls are decreasing. Decidable typechecking and logical consistency are preserved. But the conservative, syntactic
criteria is insufficient to support a variety of important programming paradigms.
Agda offers an option to disable the termination checker to allow writing arbitrary functions. However, this may endanger both decidable type checking andUnified Syntax with Iso-Types

19

logical consistency. Idris [6] 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 evaluatedby the type checker. While logical consistency is an appealing property, it is
not a goal of λI. Instead λI aims at retaining (term-level) general recursion as
found in languages like Haskell or ML, while benefiting from a unified syntax tosimplify the implementation of the core language.

7

Conclusion

This work proposes λI: a minimal dependently typed core language that allows the same syntax for terms and types, supports type-level computation, andpreserves 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 requiring strong normalization of the calculus. At
the same time one-step casts together with recursion provide a generalizationof iso-recursive types. Two variants of λI show trade-offs of employing different reduction strategies in casts. In future work, we hope to investigate surface
language mechanisms, such as type families in Haskell, to express intensive typelevel computation in a more convenient way.
Acknowledgments. We thank the anonymous reviewers for their helpful comments. This work has been sponsored by the Hong Kong Research Grant Council
Early Career Scheme project number 27200514.

References
1. Adams, R.: Pure type systems with judgemental equality. Journal of Functional
Programming 16(02), 219–246 (2006)
2. Altenkirch, T., Danielsson, N.A., Löh, A., Oury, N.: ΠΣ: Dependent types without
the sugar. In: Functional and Logic Programming, pp. 40–55. Springer (2010)
3. Augustsson, L.: Cayenne — a language with dependent types. In: ICFP ’98. pp.
239–250 (1998)
4. Barendregt, H.: Introduction to generalized type systems. Journal of Functional
Programming 1(2), 125–154 (1991)
5. Barendregt, H.: Lambda calculi with types. In: Handbook of Logic in Computer
Science. vol. 2, pp. 117–309 (1992)
6. Brady, E.: IDRIS—systems programming meets full dependent types. In: PLPV
’11. pp. 43–54 (2011)
7. Cardelli, L.: A Polymorphic lambda-calculus with Type: Type. Digital Systems
Research Center (1986)
8. Casinghino, C., Sjöberg, V., Weirich, S.: Combining proofs and programs in adependently typed language. In: POPL ’14. pp. 33–45 (2014)
9. Coq development team: The coq proof assistant. http://coq.inria.fr/20

Y. Yang et al.

10. Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76, 95–120 (1988)
11. Crary, K., Harper, R., Puri, S.: What is a recursive module? In: PLDI ’99. pp.
50–63 (1999)
12. van Doorn, F., Geuvers, H., Wiedijk, F.: Explicit convertibility proofs in pure typesystems. In: LFMTP ’13. pp. 25–36 (2013)
13. Eisenberg, R.A., Vytiniotis, D., Peyton Jones, S., Weirich, S.: Closed type families
with overlapping equations. In: POPL ’14 (2014)
14. Girard, J.Y.: Interprtation fonctionnelle et limination des coupures de l’arithmtiqued’ordre suprieur. Ph.D. thesis, Universit Paris VII (1972)
15. Jones, M.P.: Type Classes with Functional Dependencies. Proceedings of the 9th
European Symposium on Programming Languages and Systems (March) (2000)
16. Jutting, L.: Typing in pure type systems. Information and Computation 105(1),30–41 (1993)
17. Kimmell, G., Stump, A., III, H.D.E., Fu, P., Sheard, T., Weirich, S., Casinghino,C., Sjöberg, V., Collins, N., Ahn, K.Y.: Equational reasoning about programs withgeneral recursion and call-by-value semantics. In: PLPV ’12. pp. 15–26 (2012)
18. Mogensen, T.A.: Theoretical pearls: Efficient self-interpretation in lambda calculus.
Journal of Functional Programming 2(3), 345–364 (1992)
19. Norell, U.: Towards a practical programming language based on dependent typetheory. Ph.D. thesis, Chalmers University of Technology (2007)
20. Peyton Jones, S., Washburn, G., Weirich, S.: Wobbly types: type inference for generalised algebraic data types. Tech. Rep. MS-CIS-05-26, University of Pennsylvania(Jul 2004)
21. Peyton Jones, S., Meijer, E.: Henk: a Typed Intermediate Language. In: Types inCompilation Workshop (1997)
22. Pierce, B.C.: Types and programming languages. MIT press (2002)
23. Sjöberg, V., Casinghino, C., Ahn, K.Y., Collins, N., III, H.D.E., Fu, P., Kimmell,G., Sheard, T., Stump, A., Weirich, S.: Irrelevance, heterogenous equality, andcall-by-value dependent type systems. In: MSFP ’12. pp. 112–162 (2012)
24. Sjöberg, V., Weirich, S.: Programming up to congruence. In: POPL ’15. pp. 369–
382 (2015)25. Stump, A., Deters, M., Petcher, A., Schiller, T., Simpson, T.: Verified programmingin guru. In: PLPV ’09. pp. 49–58 (2008)
26. Sulzmann, M., Chakravarty, M.M.T., Jones, S.P., Donnelly, K.: System f with typeequality coercions. In: TLDI ’07. pp. 53–66 (2007)
27. Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure
distributed programming with value-dependent types. In: ICFP ’11. pp. 266–278(2011)
28. Weirich, S., Hsu, J., Eisenberg, R.A.: System fc with explicit kind equality. In:
ICFP ’13. pp. 275–286 (2013)
29. Yang, Y., Bi, X., Oliveira, B.C.d.S.: Unified syntax with iso-types. Extended version available from https://bitbucket.org/ypyang/aplas16 (2016)30. Yorgey, B.A., Weirich, S., Cretin, J., Peyton Jones, S., Vytiniotis, D., Magalhães,
J.P.: Giving Haskell a Promotion. In: TLDI ’12. pp. 53–66 (2012)