Séance de cours

Sous-typage algorithmique : preuve de transitivité

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

Cette séance de cours couvre le concept de sous-typage algorithmique et se concentre sur la preuve de la transitivité dans le contexte des relations de sous-type. Linstructeur explique comment dériver les relations de sous-type entre différents types en utilisant linduction sur la dérivation des jugements de sous-typage. Grâce à une analyse étape par étape de la règle de transitivité, la séance de cours montre comment appliquer des hypothèses d'induction pour prouver la transitivité dans divers scénarios. La séance de cours aborde également les défis de la mise en œuvre de la transitivité dans un système de sous-typage algorithmique et donne un aperçu du processus de dérivation des relations de sous-type entre les types de fonctions. En outre, la séance de cours explore l'importance de comprendre les formes des types et comment elle influence la dérivation des relations de sous-type.

Source officielle

Concepts associés (11)

Théorie des types

En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant.

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).

Héritage (informatique)

En programmation orientée objet, l’héritage est un mécanisme qui permet, lors de la déclaration d’une nouvelle classe, d'y inclure les caractéristiques d’une autre classe. L'héritage établit une relation de généralisation-spécialisation qui permet d'hériter dans la déclaration d’une nouvelle classe (appelée classe dérivée, classe fille, classe enfant ou sous-classe) des caractéristiques (propriétés et méthodes) de la déclaration d'une autre classe (appelée classe de base, classe mère, classe parent ou super-classe).

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

Fonction anonyme

En programmation informatique, une fonction anonyme, aussi appelée lambda expression ou fonction lambda est une fonction n'ayant pas de nom. Les fonctions anonymes existent dans certains langages de programmation comme Python, JavaScript, OCaml ou C++. Certains langages, comme le C et Pascal (tout au moins les versions standards de ces langages), ne permettent pas d'écrire des fonctions anonymes. Parce que ces fonctions n'ont pas de nom, à l'endroit où l'on voudrait mettre leur nom, on trouve directement les instructions définissant la fonction introduites par une syntaxe particulière.

Afficher plus

Séances de cours associées (19)

Type Inférence

Explore l'inférence de type dans les langages typés statiquement, en utilisant des algorithmes pour attribuer des types aux expressions de programme avec précision.

Variance et recherche combinée

Couvre le sous-typage, les génériques, la variance, les limites de type, la covariance, la contravariance et la recherche combinatoire.

Sous-typage et calcul de type Connectez-vous à Mediaspace pour regarder cette vidéo

Explore le sous-typage, le calcul de type et le calcul de limites de type dans un système avec sous-typage, guidant à travers des exercices et des preuves étape par étape.

Fonctions d'ordre supérieur

Couvre les fonctions d'ordre supérieur, les types de fonctions et les fonctions anonymes dans la programmation.

Fondements de Scala: Modélisation et Systèmes de Type

Couvre les fondements de Scala, y compris la modélisation des types récursifs, des types paramétrés et de la variance.

Afficher plus

Concepts associés (11)

Théorie des types

Function type

Héritage (informatique)

Subtyping

Fonction anonyme

Afficher plus