Qu'est-ce que la saisie dépendante ?

Question

Quelqu'un peut-il m'expliquer ce qu'est la frappe dépendante ? J'ai peu d'expérience en Haskell, Cayenne, Epigram ou d'autres langages fonctionnels, donc plus vous utiliserez des termes simples, plus je l'apprécierai !

Answer 1

Considérez ceci : dans tous les langages de programmation décents, vous pouvez écrire des fonctions, par ex.

def f(arg) = result

Ici, f prend une valeur arg et calcule une valeur result . Il s'agit d'une fonction de valeurs à valeurs.

Maintenant, certains langages vous permettent de définir des valeurs polymorphes (ou génériques) :

def empty<T> = new List<T>()

Ici, empty prend un type T et calcule une valeur. Il s'agit d'une fonction allant des types aux valeurs.

En général, vous pouvez également avoir des définitions de types génériques :

type Matrix<T> = List<List<T>>

Cette définition prend un type et retourne un type. Elle peut être considérée comme une fonction de type à type.

Voilà pour ce qu'offrent les langues ordinaires. Un langage est dit typé de manière dépendante s'il offre également la 4ème possibilité, à savoir la définition de fonctions de valeurs vers des types. Ou en d'autres termes, paramétrer une définition de type sur une valeur :

type BoundedInt(n) = {i:Int | i<=n}

Certaines langues courantes en ont une forme factice qu'il ne faut pas confondre. Par exemple, en C++, les modèles peuvent prendre des valeurs comme paramètres, mais elles doivent être des constantes de compilation lorsqu'elles sont appliquées. Ce n'est pas le cas dans un langage véritablement typé de manière dépendante. Par exemple, je pourrais utiliser le type ci-dessus comme ceci :

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

Ici, le type de résultat de la fonction dépend de sur la valeur réelle de l'argument j d'où la terminologie.

Answer 2

Les types dépendants permettent un ensemble plus large de erreurs logiques à éliminer à temps de compilation . Pour illustrer cela, considérons la spécification suivante sur la fonction f :

Fonction f ne doit prendre que même entiers en entrée.

Sans types dépendants, vous pourriez faire quelque chose comme ceci :

def f(n: Integer) := {
  if  n mod 2 != 0 then 
    throw RuntimeException
  else
    // do something with n
}

Ici, le compilateur ne peut pas détecter si n est effectivement pair, c'est-à-dire que du point de vue du compilateur, l'expression suivante est correcte :

f(1)    // compiles OK despite being a logic error!

Ce programme s'exécute et lève une exception au moment de l'exécution, c'est-à-dire que votre programme a une erreur de logique.

Les types dépendants vous permettent d'être beaucoup plus expressifs et vous permettraient d'écrire quelque chose comme ceci :

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

Ici n est de type dépendant {n: Integer | n mod 2 == 0} . Il peut être utile de lire à haute voix ce qui suit

n est un membre d'un ensemble d'entiers tel que chaque entier est divisible par 2.

Dans ce cas, le compilateur détecterait, au moment de la compilation, une erreur de logique lorsque vous avez passé un nombre impair à la commande f et empêcherait le programme d'être exécuté en premier lieu :

f(1)    // compiler error

---

Voici un exemple illustratif utilisant Scala types dépendants du chemin de comment nous pourrions essayer de mettre en œuvre la fonction f satisfaire à une telle exigence :

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

La clé est de remarquer comment la valeur n apparaît dans le type de valeur proof à savoir n.IsEven.type :

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

Nous disons type n.IsEven.type dépend de la valeur n d'où le terme Types de dépendance .

---

À titre d'exemple supplémentaire, définissons une fonction typée dépendante où le type de retour dépend de l'argument valeur.

En utilisant les installations de Scala 3, considérez ce qui suit liste hétérogène qui maintient le type précis de chacun de ses éléments (par opposition à la déduction d'une borne supérieure minimale commune).

val hlist: (Int, List[Int], String)  = 42 *: List(42) *: "foo" *: Tuple()

L'objectif est que l'indexation ne perde aucune information de type au moment de la compilation. Par exemple, après avoir indexé le troisième élément, le compilateur devrait savoir qu'il s'agit exactement d'un String

val i: Int = index(hlist)(0)           // type Int depends on value 0
val l: List[Int] = index(hlist)(1)     // type List[Int] depends on value 1 
val s: String = index(hlist)(2)        // type String depends on value 2

Voici la signature d'une fonction typée dépendante index

type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type] 
                                  |                     |        
                                 value           return type depends on value

ou en d'autres termes

pour toutes les listes hétérogènes de type L et pour tous les indices (de valeur) idx de type Int le type de retour est Elem[L, idx.type]

où encore une fois nous notons comment le type de retour dépend de la valeur idx .

Voici l'implémentation complète pour référence, qui fait usage de Types de singleton basés sur les littéraux , Peano implémentation des entiers au niveau du type, types de match et types de fonctions dépendantes Cependant, les détails exacts sur le fonctionnement de cette implémentation spécifique à Scala ne sont pas importants aux fins de cette réponse qui tente simplement d'illustrer deux concepts clés concernant les types dépendants.

1. un type peut dépendre d'une valeur

2. ce qui permet d'éliminer un plus grand nombre d'erreurs au moment de la compilation.

   // Bring in scope Peano numbers which are integers lifted to type-level import compiletime.ops.int._

   // Match type which reduces to the exact type of an HList element at index IDX type Elem[L <: Tuple, IDX <: Int] = L match { case head *: tail => IDX match { case 0 => head case S[nextIdx] => Elem[tail, nextIdx] } }

   // type of dependently typed function index type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type]

   // implementation of DTF index val index: DTF = [L <: Tuple] => (hlist: L) => (idx: Int) => { hlist.productElement(idx).asInstanceOf[Elem[L, idx.type]] }

Type de dépendance donné DFT est maintenant capable de détecter l'erreur suivante au moment de la compilation.

val a: String = (42 :: "foo" :: Nil)(0).asInstanceOf[String] // run-time error
val b: String = index(42 *: "foo" *: Tuple())(0)             // compile-time error

scastie

Answer 3

Si vous connaissez C++, il est facile de fournir un exemple motivant :

Disons que nous avons un certain type de conteneur et deux instances de celui-ci

typedef std::map<int,int> IIMap;
IIMap foo;
IIMap bar;

et considérez ce fragment de code (vous pouvez supposer que foo est non vide) :

IIMap::iterator i = foo.begin();
bar.erase(i);

C'est un déchet évident (et corrompt probablement les structures de données), mais le contrôle de type est parfait puisque "iterator into foo" et "iterator into bar" sont du même type, IIMap::iterator même s'ils sont totalement incompatibles sur le plan sémantique.

Le problème est qu'un type d'itérateur ne doit pas dépendre uniquement du conteneur. type mais en fait sur le conteneur objet c'est-à-dire qu'il devrait être un "type de membre non statique" :

foo.iterator i = foo.begin();
bar.erase(i);  // ERROR: bar.iterator argument expected

Une telle caractéristique, la possibilité d'exprimer un type (foo.iterator) qui dépend d'un terme (foo), est exactement ce que signifie le typage dépendant.

La raison pour laquelle vous ne voyez pas souvent cette fonctionnalité est qu'elle ouvre une grande boîte de Pandore : vous vous retrouvez soudainement dans des situations où, pour vérifier à la compilation si deux types sont identiques, vous devez prouver que deux expressions sont équivalentes (elles donneront toujours la même valeur à l'exécution). En conséquence, si l'on compare l'expression de wikipedia liste des langages typés de manière dépendante avec son liste des prouveurs de théorèmes vous remarquerez peut-être une similitude suspecte ;-)

Answer 4

En citant le livre Types et langages de programmation (30.5) :

Une grande partie de cet ouvrage a été consacrée à la formalisation de l'abstraction d'abstraction de différentes sortes. Dans le lambda-calcul simplement typé, nous avons formalisé l'opération consistant à prendre un terme et à abstraire un sous-terme un sous-terme, ce qui donne une fonction qui peut ensuite être instanciée en en l'appliquant à différents termes. Dans le système F nous avons considéré l'opération l'opération consistant à prendre un terme et à abstraire un type, ce qui donne un terme qui peut être instancié en l'appliquant à divers types. Dans nous avons Nous avons récapitulé les mécanismes du lambda-calcul simplement typé "un niveau supérieur ", en prenant un type et en abstrayant une sous-expression pour obtenir un opérateur de type qui peut ensuite être instancié en l'appliquant à différents types. différents types. Une façon pratique de penser à toutes ces formes d'abstraction d'abstraction est en termes de familles d'expressions, indexées par d'autres expressions. expressions. Une abstraction lambda ordinaire x:T1.t2 est une famille de termes [x -> s]t1 indexé par termes s . De même, une abstraction de type X::K1.t2 est une famille de termes indexés par des types, et un opérateur de type est une famille de types indexés par des types.

• x:T1.t2 famille de termes indexée par des termes

• X::K1.t2 famille de termes indexés par types

• X::K1.T2 famille de types indexée par les types

En regardant cette liste, il est clair qu'il y a une possibilité que nous n'avons pas encore envisagée : les familles de types indexées par des termes. Cette forme d'abstraction forme d'abstraction a également été étudiée de manière approfondie, sous la sous la rubrique des types dépendants.