scala - programacion - Código que ejercita las posibilidades únicas de cada borde del cálculo lambda.

lambda symbol

Question

No puedo explicar el término cubo lambda mucho mejor que Wikipedia:

[...] el λ-cubo es un marco para explorar los ejes de refinamiento en el cálculo de construcciones de Coquand, a partir del cálculo lambda simplemente escrito como el vértice de un cubo colocado en el origen y el cálculo de construcciones (orden superior cálculo lambda polimórfico de tipo dependiente) como su vértice diametralmente opuesto. Cada eje del cubo representa una nueva forma de abstracción:

• Términos según tipos, o polimorfismo. El sistema F, también conocido como cálculo lambda de segundo orden, se obtiene imponiendo solo esta propiedad.
• Tipos según tipos, o operadores de tipo. Simplemente se escribe lambda-cálculo con operadores de tipo, λω, se obtiene imponiendo solo esta propiedad. Combinado con el Sistema F, se obtiene el Sistema Fω.
• Tipos dependiendo de los términos, o tipos dependientes. Al imponer solo esta propiedad se obtiene λΠ, un sistema de tipos estrechamente relacionado con LF.

Los ocho cálculos incluyen la forma más básica de abstracción, términos que dependen de los términos, funciones ordinarias como en el cálculo lambda de tipo simple. El cálculo más rico del cubo, con las tres abstracciones, es el cálculo de las construcciones. Los ocho cálculos están fuertemente normalizados.

¿Es posible encontrar ejemplos de código en lenguajes como Java, Scala, Haskell, Agda, Coq para cada refinamiento que sería imposible lograr en los cálculos que carecen de este refinamiento?

Answer 1

¿Es posible encontrar ejemplos de código en lenguajes como Java, Scala, Haskell, Agda, Coq para cada refinamiento que sería imposible lograr en los cálculos que carecen de este refinamiento?

Estos idiomas no se corresponden directamente con ningún sistema en el cubo lambda, pero aún podemos ejemplificar la diferencia entre los sistemas en el cubo lambda por la diferencia entre estos idiomas. Aquí hay unos ejemplos:

• Agda tiene tipos dependientes pero Haskell no. Así que en Agda, podemos parametrizar listas con su longitud:

  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)

  Esto no es posible en Haskell.

• Scala tiene mejor soporte para operadores de tipo que Java. Así que en Scala, podemos parametrizar un tipo en un operador de tipo:

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

  Esto no es posible en Java.

• Java 1.5 tiene mejor soporte para el polimorfismo que Java 1.4. Entonces, desde Java 1.5, podemos parametrizar un método en un tipo:

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

  Esto no es posible en Java 1.4.

Creo que tales ejemplos pueden ayudar a entender el cubo lambda, y el cubo lambda puede ayudar a entender estos ejemplos. Pero esto no significa que estos ejemplos capturen todo lo que hay que saber sobre el cubo lambda, o que el cubo lambda capture todas las diferencias entre estos idiomas.