Cubical Higher Type Theory as a Programming Language

I gave a presentation at the Workshop on Categorical Logic and Univalent Foundations held in Leeds, UK July 27-29th 2016.  My talk, entitled Computational Higher Type Theory, concerns a formulation of higher-dimensional type theory in which terms are interpreted directly as programs and types as programs that express specifications of program behavior.  This approach to type theory, first suggested by Per Martin-Löf in his famous paper Constructive Mathematics and Computer Programming and developed more fully by The NuPRL Project, emphasizes constructive mathematics in the Brouwerian sense: proofs are programs, propositions are types.

The now more popular accounts of type theory emphasize the axiomatic freedom given by making fewer foundational commitments, such as not asserting the decidability of every type, but give only  an indirect account of their computational content, and then only in some cases.  In particular, the computational content of Voevodsky’s Univalence Axiom in Homotopy Type Theory remains unclear, though the Bezem-Coquand-Huber model in cubical sets carried out in constructive set theory gives justification for its constructivity.

To elicit the computational meaning of higher type theory more clearly, emphasis has shifted to cubical type theory (in at least two distinct forms) in which the higher-dimensional structure of types is judgmentally explicit as the higher cells of a type, which are interpreted as identifications.  In the above-linked talk I explain how to construe a cubical higher type theory directly as a programming language.  Other efforts, notably by Cohen-Coquand-Huber-Mörtberg, have similar goals, but using somewhat different methods.

For more information, please see my home page on which are linked two arXiv papers providing the mathematical details, and a 12-page paper summarizing the approach and the major results obtained so far.  These papers represent joint work with Carlo Angiuli and Todd Wilson.


3 Responses to Cubical Higher Type Theory as a Programming Language

  1. If John Backus was right (the famous vicious circle: “programming languages are abstract copies (reflections) of von Neumann computer architecture”), and the answer is no, then there must be a non-von Neumann architecture for CHTT to be compiled on.

    Actually, the contemporary functional languages are still of von Neumann, i.e. with additional lazy evaluation (term reduction to normal form). This means, the computation on higher type objects are done there in a symbolic way.

    The original idea of Backus was “programs as mathematical objects”, where the objects (like functionals) are not represented by names (terms) in computations.

    Although symbolic computations make sense (like algebraic calculations), and the computations on higher order object can be done (via some equations) if they are evaluated to the primitive types, the intuition behind the functionals is that they are *objects* that can be constructed as concrete structures.
    Such objects may be envisioned as programmable integrated circuits (FPGAs).
    This may break the current paradigm in IT that only symbolic computations (term rewriting) can be done on higher order objects.

    It seems that the hardware technology is still far from making possible to break the paradigm.

    By the way, human brain is non-von Neumann. The recent advances in Neurobiology may shed some light on how non symbolic computations can be done, google
    R. Douglas Fields. Glial Regulation of the Neuronal Connectome through Local and Long-Distant Communication.

  2. Is CHTT a von Neumann programming language (according to John Backus) ? Of course, the question is interesting if it is not.

Leave a Reply


WordPress.com Logo


Twitter picture


Facebook photo


Google+ photo


Connecting to %s

%d bloggers like this: