Code exerçant les possibilités uniques de chaque bord du calcul lambda

Question

Je ne peux pas expliquer le terme lambda cube beaucoup mieux que Wikipédia n':

[...] le λ-cube est un cadre de travail pour explorer les axes de raffinement dans Coquand du calcul des constructions, à partir de la tout simplement tapé lambda calcul comme le sommet d'un cube placé à l'origine, et la le calcul des constructions (d'ordre supérieur dépendante de typage polymorphe lambda calcul) comme diamétralement opposé sommet. Chaque axe de le cube représente une nouvelle forme d'abstraction:

• Les termes en fonction de types ou de polymorphisme. Le système F, aka second ordre lambda calcul, est obtenue en imposant seulement cette propriété.
• Types selon les types, ou le type d'opérateurs. Simplement tapé lambda-calcul avec le type d'opérateurs, λω, est obtenue en imposant seulement cette propriété. Combiné avec le Système F il rendements Système de Fw.
• Types en fonction des conditions, ou des types dépendants. Imposer que cette propriété rendements λΠ, un système de type étroitement liées à la FL.

Tous les huit calculs incluent la forme la plus élémentaire de l'abstraction, les conditions selon les termes, les fonctions ordinaires comme dans les simplement tapé lambda le calcul. Les plus riches de calcul du cube, avec tous les trois les abstractions, est le calcul des constructions. Tous les huit calculs sont fortement normalisant.

Est-il possible de trouver des exemples de code dans des langages comme Java, Scala, Haskell, Agda, Coq pour chaque raffinement qui serait impossible à réaliser dans les calculs de ce manque de raffinement?

Answer 1

Est-il possible de trouver des exemples de code dans des langages comme Java, Scala, Haskell, Agda, Coq pour chaque raffinement qui serait impossible à réaliser dans les calculs de ce manque de raffinement?

Ces langues ne correspondent pas directement à un système dans le lambda cube, mais on peut encore illustrer la différence entre les systèmes dans le lambda cube par la différence entre ces langues. Voici quelques exemples:

• Agda a des types dépendants, mais Haskell n'a pas. Ainsi, dans Agda, on peut paramétrer des listes avec leur longueur:

  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat
  
  data Vec (A : Set) : Nat -> Set where
    empty : Vec zero
    cons : (n : Nat) -> A -> Vec n -> Vec (succ n)
  

  Ce n'est pas possible en Haskell.

• Scala a un meilleur support pour le type d'opérateurs de Java. Donc, en Scala, nous pouvons paramétrer un type sur un type d'opérateur:

  class Foo[T[_]] {
    val x: T[Int]
    val y: T[Double]
  }
  

  Ce n'est pas possible en Java.

• Java 1.5 a un meilleur support pour le polymorphisme de Java 1.4. Donc, depuis Java 1.5, on peut paramétrer une méthode sur un type:

  public static <A> A identity(A a) {
    return a;
  }
  

  Ce n'est pas possible en Java 1.4

Je pense que ces exemples peuvent aider à comprendre le lambda cube, et le lambda cube peut aider à comprendre ces exemples. Mais cela ne signifie pas que ces exemples de saisir tout ce qu'il ya à savoir sur le lambda cube, ou que le lambda cube capture toutes les différences entre ces langues.