Suponga que extiende el cálculo de construcciones con "agujeros", es decir, piezas de código incompletas que aún no completó. Me pregunto si hay un algoritmo para llenar esos roles automáticamente. Por ejemplo (usando la sintaxis de Morte ):
Caso A:
λ (pred : ?)
-> λ (Nat : *)
-> λ (Succ : Nat -> Nat)
-> λ (Zero : Nat)
-> (Succ (pred Nat Succ Zero))
En esta situación, un algoritmo de inferencia de tipos puede identificar que ?
obviamente sólo puede ser ∀ (Nat : *) -> (Nat -> Nat) -> Nat -> Nat
, porque pred
recibe Nat : *
, Succ : Nat -> Nat
, Zero : Nat
, y debe volver Nat
, porque es el primer argumento de Succ
.
Caso B:
(Id ? 4)
Donde 4 está codificado en λ y Id
es la función de identidad (es decir, ∀ (t:*) -> λ (x:t) -> x
). En esa situación, ´? ´ es nuevamente claro ∀ (N:*) -> (N -> N) -> N -> N
, porque ese es el tipo de 4
.
Caso C:
(Id (Equals Nat 7 (add 3 ?)) (Refl 7))
Aquí, Equals
y Refl
se definen de manera similar a Idris. ?
obviamente, solo puede ser 4
, pero ¿cómo se da cuenta de eso? Una forma sería usar el hecho de que ? : Nat
, y Nat
es un tipo que sabemos enumerar, por lo que podemos intentarlo todo Nats
hasta que compruebe el tipo. Eso se puede hacer para cualquier tipo enumerable.
Caso D:
(Id (Equal Nat 10 (MulPair ?)) 10)
Aquí, ?
solo puede ser de tipo Pair Nat
; sólo tiene más de una respuesta válida, sin embargo: que puede ser (Pair 10 1)
, (Pair 2 5)
, (Pair 5 2)
y (Pair 1 10)
.
Caso E:
(Id (Equal Nat 7 (Mul 2 ?)) 7)
Aquí, no hay una respuesta válida, ya 7
que no es un múltiplo de 2
.
Todos esos ejemplos me hicieron notar que podemos hacer un algoritmo general que identifica algunos patrones conocidos y da una respuesta seleccionando a mano un algoritmo específico (inferencia de tipo, fuerza bruta, etc.), algo así como Wolfram Alpha descubre la estrategia correcta para resolver una integral. Pero eso suena como un enfoque de ingeniería / codificado. ¿Hay alguna forma de principios para resolver este problema? ¿Hay algún estudio de investigación / área en él?
fuente