Algoritmo para la comprobación de tipo ML-como coincidencia de patrones?

Aquí hay un código de un no experto. Muestra cómo se ve el problema si restringes tus patrones a constructores de listas. En otras palabras, los patrones solo se pueden usar 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 reclist:

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

A traduzca un patrón OCaml a esta forma, primero reescriba usando (::). Luego reemplace [] con Nil, _ con Any, y (::) con Cons. Así que el patrón [] :: _ se traduce como Cons (Nil, Any)

Aquí hay una función que coincide con un patrón contra una lista:

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. Observe 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 un función intersect que toma dos patrones y devuelve un patrón que coincide con la intersección de lo que coincide con los dos patrones. Dado que los patrones pueden no cruzarse en absoluto, devuelve None cuando no hay intersección y Some p de lo contrario.

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, intersecar el patrón [_, []] contra el patrón [[], _]. El primero es lo mismo que _ :: [] :: [], y también lo es Cons (Any, Cons (Nil, Nil)). Este último es lo 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 se ve bastante bien: [[], []].

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

Para ser exhaustivo necesitas trabajar con una lista de patrones. Aquí hay una función 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 alcance Any en al menos uno de los patrones (sin importar cómo se vea la entrada). Y en el camino, necesitas ver Nil y Cons en cada punto. Si alcanzas Nil en el mismo lugar en todos los patrones, significa que hay una entrada más larga que no será emparejada por ninguno de ellos. Por otro lado, si ves solo Cons en el mismo lugar en todos los patrones, hay una entrada que termina en ese punto que no se emparejará.

La parte difícil es verificar la exhaustividad de los dos sub-patrones de un Cons. Este código funciona como yo cuando lo compruebo a mano: encuentra todos los subconjuntos diferentes que podrían coincidir a la izquierda, luego se asegura de que los subpatrones de la derecha correspondientes sean exhaustivos en cada caso. Luego lo mismo con izquierda y derecha invertida. Dado que soy un no experto (más obvio para mí todo el tiempo), probablemente hay mejores maneras de hacer esto.

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

He comprobado este código contra 30.000 al azar patrones generados, por lo que tengo cierta confianza en que es correcto. Espero que estas humildes observaciones puedan ser de alguna utilidad.

Creo que el sub-lenguaje de patrones es lo suficientemente simple como para que sea fácil de analizar. Esta es la razón para requerir 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 de una especie de espacio de tuplas anidado a un conjunto restringido de tuplas. No creo que sea demasiado difícil comprobar la exhaustividad y la superposición en este modelo.