История изменений
Исправление monk, (текущая версия) :
Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^W основа :)
Хаскель не такая уж и плохая основа. GADT ghc + произвольный предикат LH – практически произвольный контракт.
Они чем-то принципиально отличаются от зависимых типов LH?
Нет.
Дважды проверять придется в любом случае, сами по себе типы тебе не гарантируют корректность преобразований.
Нет.
Делаем сортировку вставкой:
;; контракт
(define/contract (add-item a x)
(-> sorted/c -> any/c -> sorted/c)
...)
;; тип
(: add-item/t (-> Sorted Any Sorted))
(define (add-item/t a x) ...)
(: sorted/c (-> Any Boolean : Sorted))
;; вызываем версию с контрактом
(define a (get-array))
(set! a (add-item a 1))
(set! a (add-item a 2))
;; 4 раза вызвался sorted/c, неявно
;; вызываем типизированную
(define a1 (get-array))
(when (sorted/c a1) ;; добавляем тип
(set! a1 (add-item a1 1))
(set! a1 (add-item a1 2)))
;; sorted/c вызвался один раз, явным образом
Исходная версия monk, :
Я не в теме, чтобы сказать, на сколько они нормальные. И в любом случае остается хаскель как проблем^W основа :)
Хаскель не такая уж и плохая основа. GADT ghc + произвольный предикат LH – практически произвольный контракт.
Они чем-то принципиально отличаются от зависимых типов LH?
Нет.
Дважды проверять придется в любом случае, сами по себе типы тебе не гарантируют корректность преобразований.
Нет.
Делаем сортировку вставкой:
;; контракт
(define/contract (add-item a x)
(-> sorted/c -> any/c -> sorted/c)
...)
;; тип
(: add-item/t (-> Sorted Any Sorted))
(define (add-item/t a x) ...)
(: sorted/c (-> Any Boolean : Sorted))
;; вызываем версию с контрактом
(define a (get-array))
(add-item a 1)
(add-item a 2)
;; 4 раза вызвался sorted/c, неявно
;; вызываем типизированную
(define a1 (get-array))
(when (sorted/c a1) ;; добавляем тип
(add-item a1 1)
(add-item a1 2))
;; sorted/c вызвался один раз, явным образом