gds (gds) wrote,
gds
gds

Давно хотел сделать это. Ну или подобное.

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

deni_ok напомнил про статическую типизацию, позволяющую работать с сортированными списками, сохраняя отсортированность как инвариант. Решил поиграться слегка, чтобы отвлечься как от одной работы (реляционки), так и от другой (жабаскрипт).

(* typed sorted lists *)
module TSL (Ord : sig type t; value compare : t -> t -> int; end)
 =
  struct

    (* Доказывается только этот модуль: *)
    module Core
     :
      sig

        type tsl = private list Ord.t;
        (* Значения этого типа мы не дадим создавать снаружи,
           но дадим возможность разрушать их как значения
           с типом list Ord.t. *)

        value nil : tsl;
        value one : Ord.t -> tsl;
        (* Этими значениями мы утверждаем, что пустой список
           и список из одного элемента -- сортированные. *)

        value merge : tsl -> tsl -> tsl;
        (* Этим утверждаем, что слияние сортированных списков
           даёт сортированный список. *)

        (* Далее мы можем использовать только указанные
           утверждения для написания кода, работающего с
           сортированными списками. *)
      end
     =
      struct
        type tsl = list Ord.t;
        value nil = [];
        value one elem = [elem];
        value merge a b = List.merge Ord.compare a b;
      end
    ;

    (* Этот код защищён статической типизацией: *)

    value (make_sorted : list Ord.t -> Core.tsl) lst =
      List.fold_left
        (fun acc elem -> Core.merge acc (Core.one elem))
        Core.nil
        lst
      (* implementation == facepalm, знаю *)
    ;

  end
;


module Int = struct type t = int; value compare = Pervasives.compare; end;

module I = TSL(Int);

value list_in : list int = [5;2;3;6;7;4];

value list_out = I.make_sorted list_in;

List.iter (Printf.printf "%i") (list_out :> list Int.t );


Вывод, разумеется, "234567".

Можно было бы попробовать взять чуть другую аксиоматику (модуль Core), но сходу не получилось, а много времени тратить не хотел.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 10 comments
Толково.
Общественность негодует: опять этот окамл обходится без зависимых типов там, где они так нужны! :)
;-) Точно.
Да, неплохо, но зависимыми было бы несколько прямее.
Может быть, я не прав, O'Camlу не ученый, но...

Это ведь обычная сортировка вставками, где часть функциональности, а именно вставка, вынесена в Core.merge. Где ж здесь доказательство корректности? Понятно, что статической информации привязано больше, но все же.

Тем более, как с помощью этого Core доказать корректность, например, quick sort'а?
quick sort'а -- никак, ибо аксиоматика ограничена. Я лишь взял тупые аксиомы (самые простые, которые пришли в голову по поводу сортированных списков) и накодил их. Хотел выразить только одну штуку: каждое типизированное значение является утверждением (в том числе функция -- там этот самый изоморфизм, который про лямбды и логические следствия).
Насчёт других видов сортировки -- буду думать (есть идеи), но там понту мало, как и в любых других случаях доказательства кода. (а именно, в случаях написания кода и доказательства пишутся как минимум две штуки: и сам код, и его доказательство, и они по объёму похожи, но доказательство сильно сложнее по умственным усилиям, что делает затею не слишком умной для практических применений.)
Имхо доказательная проверка имеет смысл только тогда, когда она автоматически производится компилятором (или его стандартной библиотекой). Т.е. мы даем директиву "воспользуйся интуицией", и если компилятор не может доказать, что наша программа выполняет заданное действие, то, скорее всего, в ней ошибка. Если же ошибки нет, обновляется набор тактик и отправляется в общий репозиторий, дабы быть разосланным в следующем еженедельном апдейте.
К сожалению, сложность такой системы куда выше, чем может быть запрограммирована одним программистом без глубокого погружения в сабж. Что-то такое появится, не раньше, чем люди вдоволь наиграются с Agda/Epigram и пр.

зы Кроме доказательства корректности компилятор может доказывать некорректность, уменьшая, таким образом, количество программ, которые он не может обработать.
автоматически проверить корректность очень сложно, так как неизвестно, корректность чего мы проверяем. Из моего примера -- сигнатуре функции merge удовлетворяет и concat, а ещё и любая из двух функций, имеющих тип a->a->a.
Конкретно с Coq -- игрался год-два назад, и там всё зависело от того, какой именно спецификации должна соответствовать моя программа, и надо было серьёзно формулировать спецификацию. Количество текста на спецификацию соответствовало количеству кода.

А вот идея про доказательства некорректности мне очень по нраву, хотя бы потому, что корректность доказывать обычно очень сложно, либо я просто не умею. Одним из самых клёвых доказателей некорректности для меня являются системы типов: они говорят, что нельзя складывать целые со строками, например. Или вот, если у javascript-объекта нет свойства top_left, то его нельзя передавать в функцию, которая делает "argument.top_left = $V([123,456]);" (но это из злободневного).
Наверное, нужен правильный DSEL для спецификации спецификации. =)
засада в том, что всё-таки надо указывать, что мы хотим доказать.
Впрочем, если будут сколько-нибудь приличные идеи про таковой DSEL -- будет интересно почитать, ибо тема очень интересна.
Извиняюсь, если где налажал с operator precedence.

forall f : is_weak f, is_strict f .
    forall x : is_container x .
        forall i : in_range x i, in_range x (i+1) .
            (sort f x !! i) `f` (sort f x !! i+1)

qsort :: (T -> T -> Bool) -> Cont T -> Cont2 T
qsort f [] = []
qsort f x = do
    m <- middle x
    p1, p2 <- partition m x
    return $ qsort p1 ++ qsort p2


qsort `does` sort -- does производит тайпчек

Очень умный (rank-n logic) Prolog, короче говоря. Проблема в том, что нужно пройти по самой границе undecidability, потому что проверка is_weak, например, уже похожа на проблему сравнения двух функций на равенство. Если f будет функцией лексикографической сортировки, доказательство совсем нетривиально.