Подтвердить что ты не робот

Алгоритм проверки типа ML-подобным образом?

Как вы определяете, является ли данный шаблон "хорошим", в частности, является ли он исчерпывающим и неперекрывающимся, для языков программирования в стиле ML?

Предположим, что у вас есть такие шаблоны, как:

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

или

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

Хорошая проверка типа предупреждает, что первая не является исчерпывающей, а вторая перекрывается. Как бы тип проверки мог принимать такие решения в общем случае для произвольных типов данных?

4b9b3361

ОТВЕТЫ

Ответ 1

Здесь представлен эскиз алгоритма. Это также основа Леннарта Августсона, знаменитого техника для эффективного сопоставления шаблонов. (бумага находится в этом невероятном процессе FPCA (LNCS 201) с большим количеством хитов.) Идея состоит в том, чтобы восстановить исчерпывающий, не избыточный анализ путем многократного разбиения наиболее общего шаблона на случаи конструктора.

В общем, проблема в том, что ваша программа имеет, возможно, пустую группу " фактическое & rsquo; шаблоны {p 1,.., p n}, и вы хотите знать, покрывают ли они данный & lsquo; ideal & rsquo; шаблон q. Чтобы начать, возьмите q, чтобы быть переменной x. Инвариант, первоначально удовлетворенный и впоследствии поддерживаемый, состоит в том, что каждый p i is & sigma; i q для некоторой подстановки & sigma; i отображение переменных в шаблоны.

Как действовать. Если n = 0, пучок пуст, поэтому у вас есть возможный случай q, который не покрывается шаблоном. Жалуйтесь, что ps не являются исчерпывающими. Если & sigma; 1 является инъективным переименованием переменных, то p 1 улавливает каждый случай, соответствующий q, поэтому мы тепло: if n = 1, мы побеждаем; если n > 1, то oops, нет способа p 2. В противном случае мы имеем это для некоторой переменной x, & sigma; 1 x - шаблон конструктора. В этом случае проблема разбивается на несколько подзадач, по одному для каждого конструктора c j типа x. То есть разбить исходный q на несколько идеальных шаблонов q j= [x: = c j y 1.. y arity (c j)] q и уточнить шаблоны соответственно для каждого q j, чтобы сохранить инвариант, отбросив те, которые не совпадают.

Возьмем пример с {[], x :: y :: zs} (используя :: для cons). Начнем с

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

и мы [xs: = []] сделали первый образец экземпляром идеала. Итак, мы разделили xs, получив

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

Первое из них оправдано пустым инъективным переименованием, так что это нормально. Вторая принимает [x: = x, ys: = y:: zs], поэтому мы снова уходим, раскалываем ys, получаем.

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

и из первой подзадачи мы можем видеть, что мы запрещены.

Случай с перекрытием более тонкий и допускает вариации, в зависимости от того, хотите ли вы отмечать любое перекрытие или просто шаблоны, которые полностью избыточны в порядке приоритета сверху вниз. Ваш основной рок-н-ролл - то же самое. Например, начинайте с

  xs covering {[], ys}

с [xs: = []], оправдывающим первый из них, поэтому разделим. Заметим, что мы должны усовершенствовать ys с помощью случаев конструктора для сохранения инварианта.

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

Ясно, что первый случай - строго совпадение. С другой стороны, когда мы замечаем, что для поддержания инварианта требуется уточнение фактического шаблона программы, мы можем отфильтровать те строгие уточнения, которые становятся излишними, и проверить, что по крайней мере один выживает (как это происходит в случае :: здесь).

Таким образом, алгоритм строит набор идеальных исчерпывающих перекрывающихся шаблонов q таким образом, который мотивирован фактическими шаблонами программ p. Вы разбиваете идеальные шаблоны на случаи конструктора, когда фактические шаблоны требуют более подробной информации о конкретной переменной. Если вам повезет, каждый фактический узор покрывается несвязанными непустыми наборами идеальных шаблонов, и каждый идеальный образец покрывается только одним фактическим шаблоном. Дерево разломов case, которые дают идеальные шаблоны, дает вам эффективную компиляцию фактических паттернов с помощью прыжка-таблицы.

Алгоритм, который я представил, явно оканчивается, но если существуют типы данных без конструкторов, он может не согласиться с тем, что пустой набор шаблонов является исчерпывающим. Это серьезная проблема в зависимых типизированных языках, где исчерпываемость традиционных шаблонов неразрешима: разумный подход заключается в том, чтобы допускать "опровержения", а также уравнения. В Agda вы можете написать(), произносится как "моя тетя Фанни", в любом месте, где невозможно уточнение конструктора, и это освобождает вас от требования заполнить уравнение с возвращаемым значением. Каждый исчерпывающий набор шаблонов можно сделать узнаваемо исчерпывающим, добавив достаточное количество опровержений.

Во всяком случае, что основная картина.

Ответ 2

Вот код от неспециалиста. Он показывает, как выглядит проблема, если вы ограничиваете свои шаблоны списком конструкторов. Другими словами, шаблоны могут использоваться только со списками, которые содержат списки. Вот несколько таких списков: [], [[]], [[];[]].

Если вы включите -rectypes в свой интерпретатор OCaml, этот набор списков имеет один тип: ('a list) as 'a.

type reclist = ('a list) as 'a

Здесь тип для представления паттернов, которые соответствуют типу reclist:

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

Чтобы перевести шаблон OCaml в эту форму, сначала перепишите с помощью (::). Затем замените [] с Nil, _ с Any и (::) with Cons. Таким образом, шаблон [] :: _ переводит Cons (Nil, Any)

Вот функция, которая соответствует шаблону против списка:

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

Вот как он выглядит в использовании. Обратите внимание на использование -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
#

Образец Cons (Any, Nil) должен соответствовать любому списку длины 1, и он определенно работает.

Итак, кажется довольно простой написать функцию intersect, которая принимает два шаблона и возвращает шаблон, соответствующий пересечению того, что соответствует двум шаблонам. Поскольку шаблоны вообще не пересекаются, он возвращает None, когда нет пересечения и 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

Как простой тест, пересечь шаблон [_, []] по шаблону [[], _]. Первый те же, что и _ :: [] :: [], и поэтому Cons (Any, Cons (Nil, Nil)). Последнее совпадает с [] :: _ :: [], и, следовательно, Cons (Nil, (Cons (Any, Nil)).

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

Результат выглядит довольно правильно: [[], []].

Кажется, этого достаточно, чтобы ответить на вопрос о перекрывающихся шаблонах. Два шаблона перекрываются, если их пересечение не None.

Для полноты вам нужно работать со списком шаблонов. Вот функция exhaust, который проверяет, является ли данный список шаблонов исчерпывающим:

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

Образец похож на дерево с Cons во внутренних узлах и Nil или Any на листах. Основная идея состоит в том, что набор шаблонов является исчерпывающим, если вы всегда достигаете Any по крайней мере в одном из шаблонов (независимо от того, как выглядит вход). И по пути, вам нужно видеть и Нил, и Минуты в каждой точке. Если вы достигнете Nil в том же месте во всех шаблонах, это означает, что есть более длинный вход, который не будет соответствовать ни одному из них. С другой стороны, если вы видите только Cons в одном и том же месте во всех шаблонах, есть вход, который заканчивается в этой точке, который не будет соответствовать.

Трудная часть - проверка полноты двух подшаблонов Минусов. Этот код работает так, как я делаю, когда проверяю вручную: он находит все разные подмножества, которые могут совпадать слева, а затем гарантирует, что соответствующие правые подшаблоны в каждом случае являются исчерпывающими. Тогда то же самое с левым и правым обратным. Поскольку я - неэксперт (более очевидный для меня все время), вероятно, есть лучшие способы сделать это.

Вот сеанс с этой функцией:

# 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

Я проверил этот код против 30 000 случайно сгенерированных шаблонов, и поэтому у меня есть определенная уверенность в правильности этого. Я надеюсь, что эти скромные наблюдения могут оказаться полезными.

Ответ 3

Я считаю, что суб-язык шаблона достаточно прост, чтобы его легко анализировать. Это является причиной того, что шаблоны должны быть "линейными" (каждая переменная может появляться только один раз) и т.д. С этими ограничениями каждый шаблон представляет собой проекцию из своего рода вложенного кортежа в ограниченный набор кортежей. Я не думаю, что это слишком сложно проверить на полноту и перекрытие в этой модели.