algorithm - sintáctico - ¿Algoritmo para la comprobación de tipos de coincidencia de patrones tipo ML?

manejo de errores semanticos lenguajes y automatas 2

Question

¿Cómo se determina si un patrón dado es "bueno", específicamente si es exhaustivo y no superpuesto, para los lenguajes de programación estilo ML?

Supongamos que tienes patrones como:

match lst with
  x :: y :: [] -> ...
  [] -> ...

o:

match lst with
  x :: xs -> ...
  x :: [] -> ...
  [] -> ...

Un buen tipo de verificador advertiría que el primero no es exhaustivo y el segundo se superpone. ¿Cómo haría el verificador de tipos ese tipo de decisiones en general, para tipos de datos arbitrarios?

Answer 1

Aquí hay un boceto de un algoritmo. También es la base de la célebre técnica de Lennart Augustsson para compilar la concordancia de patrones de manera eficiente. (El paper está en ese increíble procedimiento de FPCA (LNCS 201) con oh tantos éxitos). La idea es reconstruir un análisis exhaustivo y no redundante dividiendo repetidamente el patrón más general en casos de constructores.

En general, el problema es que su programa tiene un grupo posiblemente vacío de patrones "reales" {p ₁ , .., p _n }, y desea saber si cubren un patrón "ideal" dado q. Para comenzar, tome q para ser una variable x. Lo invariable, inicialmente satisfecho y subsecuentemente mantenido, es que cada p _i es σ _i q para algunas sustituciones σ _{i que} asignan variables a los patrones.

Cómo proceder. Si n = 0, el grupo está vacío, por lo que tiene un posible caso q que no está cubierto por un patrón. Quejarse de que los ps no son exhaustivos. Si σ ₁ es un cambio de nombre por inyección de variables, entonces p ₁ detecta todos los casos que coinciden con q, por lo que estamos calientes: si n = 1, ganamos; si n> 1 entonces uu, no hay manera de que p ₂ pueda ser alguna vez necesario. De lo contrario, tenemos que para alguna variable x, σ ₁ x es un patrón de constructor. En ese caso divida el problema en múltiples subproblemas, uno para cada constructor c _j del tipo de x. Es decir, divida el q original en patrones ideales múltiples q _j = [x: = c _j y ₁ .. y _{arity (c j )} ] q, y refine los patrones en consecuencia para cada q _j para mantener el invariante, descartando aquellos que no coinciden

Tomemos el ejemplo con {[], x :: y :: zs} (usando :: para cons ). Empezamos con

  xs covering  {[], x :: y :: zs}

y tenemos [xs: = []] haciendo que el primer patrón sea una instancia del ideal. Así que dividimos xs, obteniendo

  [] covering {[]}
  x :: ys covering {x :: y :: zs}

El primero de ellos está justificado por el cambio de nombre de la inyección vacía, por lo que está bien. La segunda toma [x: = x, ys: = y :: zs], por lo que estamos fuera otra vez, dividiendo ys, obteniendo.

  x :: [] covering {}
  x :: y :: zs covering {x :: y :: zs}

y podemos ver desde el primer subproblema que estamos banjaxed.

El caso de superposición es más sutil y permite variaciones, dependiendo de si desea marcar cualquier superposición, o solo patrones que son completamente redundantes en un orden de prioridad de arriba a abajo. Tu rock''n''roll básico es el mismo. Por ejemplo, comenzar con

  xs covering {[], ys}

con [xs: = []] justificando el primero de ellos, por lo que se divide. Tenga en cuenta que tenemos que refinar ys con casos de constructor para mantener el invariante.

  [] covering {[], []}
  x :: xs covering {y :: ys}

Claramente, el primer caso es estrictamente una superposición. Por otro lado, cuando notamos que se necesita refinar un patrón de programa real para mantener el invariante, podemos filtrar los refinamientos estrictos que se vuelven redundantes y verificar que al menos uno sobreviva (como sucede en el caso :: aquí).

Entonces, el algoritmo construye un conjunto de patrones superpuestos exhaustivos ideales q de una manera que está motivada por los patrones reales del programa p. Se dividen los patrones ideales en casos de constructores cuando los patrones reales exigen más detalles de una variable en particular. Si tienes suerte, cada patrón real está cubierto por conjuntos disjuntos no vacíos de patrones ideales y cada patrón ideal está cubierto por un solo patrón real. El árbol de las divisiones de mayúsculas y minúsculas que producen los patrones ideales le proporciona la compilación eficiente de los patrones reales.

El algoritmo que he presentado está claramente terminado, pero si hay tipos de datos sin constructores, puede dejar de aceptar que el conjunto vacío de patrones es exhaustivo. Este es un problema grave en los lenguajes tipificados de manera dependiente, donde la exhaustividad de los patrones convencionales es indecidible: el enfoque sensato es permitir "refutaciones" y ecuaciones. En Agda, puedes escribir (), pronunciado "mi tía Fanny", en cualquier lugar donde no sea posible el refinamiento del constructor, y eso te absuelve del requisito de completar la ecuación con un valor de retorno. Cada conjunto exhaustivo de patrones puede hacerse reconociblemente exhaustivo agregando refutaciones suficientes.

De todos modos, esa es la imagen básica.

Answer 2

Aquí hay un código de un no experto. Muestra cómo se ve el problema si restringe sus patrones para mostrar constructores. En otras palabras, los patrones solo se pueden utilizar con listas que contienen listas. Aquí hay algunas listas como esa: [] , [[]] , [[];[]] .

Si habilita -rectypes en su intérprete OCaml, este conjunto de listas tiene un solo tipo: (''a list) as ''a.

type reclist = (''a list) as ''a

Aquí hay un tipo para representar patrones que coinciden con el tipo de reclist :

type p = Nil | Any | Cons of p * p

Para traducir un patrón OCaml a esta forma, primero reescriba usando (: :). Luego reemplace [] con Nil, _ con Any y (: :) con Cons. Entonces el patrón [] :: _ traduce en Cons (Nil, Any)

Aquí hay una función que hace coincidir un patrón con una reclist:

let rec pmatch (p: p) (l: reclist) =
    match p, l with
    | Any, _ -> true
    | Nil, [] -> true
    | Cons (p'', q''), h :: t -> pmatch p'' h && pmatch q'' t
    | _ -> false

Así es como se ve en uso. Tenga en cuenta el uso de -rectypes :

$ ocaml312 -rectypes
        Objective Caml version 3.12.0

# #use "pat.ml";;
type p = Nil | Any | Cons of p * p
type reclist = ''a list as ''a
val pmatch : p -> reclist -> bool = <fun>
# pmatch (Cons(Any, Nil)) [];;
- : bool = false
# pmatch (Cons(Any, Nil)) [[]];;
- : bool = true
# pmatch (Cons(Any, Nil)) [[]; []];;
- : bool = false
# pmatch (Cons (Any, Nil)) [ [[]; []] ];;
- : bool = true
# 

El patrón Cons (Any, Nil) debe coincidir con cualquier lista de longitud 1, y definitivamente parece estar funcionando.

Entonces, parece bastante sencillo escribir una intersect funciones que tome dos patrones y devuelva un patrón que coincida con la intersección de lo que coinciden con los dos patrones. Dado que es posible que los patrones no se intersecten en absoluto, devuelve None cuando no hay intersección y, en caso contrario, Some p .

let rec inter_exc pa pb =
    match pa, pb with
    | Nil, Nil -> Nil
    | Cons (a, b), Cons (c, d) -> Cons (inter_exc a c, inter_exc b d)
    | Any, b -> b
    | a, Any -> a
    | _ -> raise Not_found

let intersect pa pb =
    try Some (inter_exc pa pb) with Not_found -> None

let intersectn ps =
    (* Intersect a list of patterns.
     *)
    match ps with
    | [] -> None
    | head :: tail ->
        List.fold_left
            (fun a b -> match a with None -> None | Some x -> intersect x b)
            (Some head) tail

Como una prueba simple, interseque el patrón [_, []] con el patrón [[], _] . El primero es el mismo que _ :: [] :: [] , y también lo es Cons (Any, Cons (Nil, Nil)) . Este último es el mismo que [] :: _ :: [] , y también lo es Cons (Nil, (Cons (Any, Nil)) .

# intersect (Cons (Any, Cons (Nil, Nil))) (Cons (Nil, Cons (Any, Nil)));;
- : p option = Some (Cons (Nil, Cons (Nil, Nil)))

El resultado parece bastante correcto: [[], []] .

Parece que esto es suficiente para responder la pregunta sobre patrones superpuestos. Dos patrones se superponen si su intersección no es None .

Para ser exhaustivo, debe trabajar con una lista de patrones. Aquí hay una función de exhaust que prueba si una lista dada de patrones es exhaustiva:

let twoparts l =
    (* All ways of partitioning l into two sets.
     *)
    List.fold_left
        (fun accum x ->
            let absent = List.map (fun (a, b) -> (a, x :: b)) accum
            in
                List.fold_left (fun accum (a, b) -> (x :: a, b) :: accum)
                    absent accum)
        [([], [])] l

let unique l =
   (* Eliminate duplicates from the list.  Makes things
    * faster.
    *)
   let rec u sl=
        match sl with
        | [] -> []
        | [_] -> sl
        | h1 :: ((h2 :: _) as tail) ->
            if h1 = h2 then u tail else h1 :: u tail
    in
        u (List.sort compare l)

let mkpairs ps =
    List.fold_right
        (fun p a -> match p with Cons (x, y) -> (x, y) :: a | _ -> a) ps []

let rec submatches pairs =
    (* For each matchable subset of fsts, return a list of the
     * associated snds.  A matchable subset has a non-empty
     * intersection, and the intersection is not covered by the rest of
     * the patterns.  I.e., there is at least one thing that matches the
     * intersection without matching any of the other patterns.
     *)
    let noncovint (prs, rest) =
        let prs_firsts = List.map fst prs in
        let rest_firsts = unique (List.map fst rest) in
        match intersectn prs_firsts with
        | None -> false
        | Some i -> not (cover i rest_firsts)
    in let pairparts = List.filter noncovint (twoparts pairs)
    in
        unique (List.map (fun (a, b) -> List.map snd a) pairparts)

and cover_pairs basepr pairs =
    cover (fst basepr) (unique (List.map fst pairs)) &&
        List.for_all (cover (snd basepr)) (submatches pairs)

and cover_cons basepr ps =
    let pairs = mkpairs ps
    in let revpair (a, b) = (b, a)
    in
        pairs <> [] &&
        cover_pairs basepr pairs &&
        cover_pairs (revpair basepr) (List.map revpair pairs)

and cover basep ps =
    List.mem Any ps ||
        match basep with
        | Nil -> List.mem Nil ps
        | Any -> List.mem Nil ps && cover_cons (Any, Any) ps
        | Cons (a, b) -> cover_cons (a, b) ps

let exhaust ps =
    cover Any ps

Un patrón es como un árbol con Cons en los nodos internos y Nil o Any en las hojas. La idea básica es que un conjunto de patrones es exhaustivo si siempre llega a Any en al menos uno de los patrones (sin importar cómo se ve la entrada). Y a lo largo del camino, necesita ver Nil y Cons en cada punto. Si llegas a Nil en el mismo lugar en todos los patrones, significa que hay una entrada más larga que no coincidirá con ninguno de ellos. Por otro lado, si ve solo Cons en el mismo lugar en todos los patrones, hay una entrada que termina en ese punto que no coincidirá.

La parte difícil es verificar la exhaustividad de los dos subpatrones de un Cons. Este código funciona de la manera que lo hago cuando controlo a mano: encuentra todos los subconjuntos diferentes que pueden coincidir con los de la izquierda, luego se asegura de que los subpatrones correctos correspondientes sean exhaustivos en cada caso. Luego lo mismo con la izquierda y la derecha invertida. Como soy inexperto (más obvio para mí todo el tiempo), probablemente haya mejores formas de hacerlo.

Aquí hay una sesión con esta función:

# exhaust [Nil];;
- : bool = false
# exhaust [Any];;
- : bool = true
# exhaust [Nil; Cons (Nil, Any); Cons (Any, Nil)];;
- : bool = false
# exhaust [Nil; Cons (Any, Any)];;
- : bool = true
# exhaust [Nil; Cons (Any, Nil); Cons (Any, (Cons (Any, Any)))];;
- : bool = true

Revisé este código en comparación con los 30,000 patrones generados al azar, por lo que confío en que sea correcto. Espero que estas humildes observaciones puedan ser de alguna utilidad.

Answer 3

Creo que el sub-lenguaje de patrones es lo suficientemente simple como para que sea fácil de analizar. Esta es la razón por la que se requiere que los patrones sean "lineales" (cada variable puede aparecer solo una vez), y así sucesivamente. Con estas restricciones, cada patrón es una proyección desde un tipo de espacio de tupla anidado a un conjunto restringido de tuplas. No creo que sea demasiado difícil verificar la exhaustividad y la superposición en este modelo.