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), но сходу не получилось, а много времени тратить не хотел.
  • 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