Lecture

Algorithmic Subtyping: Transitivity Proof

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture covers the concept of algorithmic subtyping and focuses on proving transitivity in the context of subtype relationships. The instructor explains how to derive subtype relationships between different types using induction on the derivation of subtyping judgments. Through a step-by-step analysis of the transitivity rule, the lecture demonstrates how to apply induction hypotheses to prove transitivity in various scenarios. The lecture also discusses the challenges of implementing transitivity in an algorithmic subtyping system and provides insights into the process of deriving subtype relationships between function types. Additionally, the lecture explores the importance of understanding the shapes of types and how it influences the derivation of subtype relationships.

Official source

Related concepts (11)

Type theory

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general, type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation, a common one is Thierry Coquand's Calculus of Inductive Constructions.

Function type

In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or returning a function. A function type depends on the type of the parameters and the result type of the function (it, or more accurately the unapplied type constructor · → ·, is a higher-kinded type).

Inheritance (object-oriented programming)

In object-oriented programming, inheritance is the mechanism of basing an object or class upon another object (prototype-based inheritance) or class (class-based inheritance), retaining similar implementation. Also defined as deriving new classes (sub classes) from existing ones such as super class or base class and then forming them into a hierarchy of classes. In most class-based object-oriented languages like C++, an object created through inheritance, a "child object", acquires all the properties and behaviors of the "parent object", with the exception of: constructors, destructors, overloaded operators and friend functions of the base class.

Subtyping

In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation (written as S

Anonymous function

In computer programming, an anonymous function (function literal, lambda abstraction, lambda function, lambda expression or block) is a function definition that is not bound to an identifier. Anonymous functions are often arguments being passed to higher-order functions or used for constructing the result of a higher-order function that needs to return a function. If the function is only used once, or a limited number of times, an anonymous function may be syntactically lighter than using a named function.

Related lectures (19)

Type Inference

Explores type inference in statically typed languages, using algorithms to assign types to program expressions accurately.

Variance and Combinatorial Search

Covers subtyping, generics, variance, type bounds, covariance, contravariance, and combinatorial search.

Subtyping and Type Calculus Log in to Mediaspace to watch this video

Explores subtyping, type calculus, and type bounds calculation in a system with subtyping, guiding through exercises and proofs step by step.

Higher-Order Functions

Covers higher-order functions, function types, and anonymous functions in programming.

Foundations of Scala: Modelling and Type Systems