kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

Инварианты типа и зависимые типы

Кажется, кстати, в языках с всей этой наукой про пред- и пост- условия и проч. зависимые типы возникают естественным образом - в качестве ответа на потреность в инвариантах, зависящих от каких-то контекстных параметров:
  type array 'a model { length : int; mutable elts : map int 'a }
    invariant { 0 <= self.length }
val ([]) (a: array 'a) (i: int) : 'a
    requires { "expl:index in array bounds" 0 <= i < length a }
...

let  rev (len : int) (a : array 'a) (b : array 'a) 
      requires { a.length = len = b.length }
      ensures  { forall i : int . (0 <= i < len -> b [len - 1 - i] = a [i]) }
	=
      for i =  0 to len - 1 do
	invariant { forall k : int . (0 <= k < i -> b [len - 1 - k] = a [k]) } 
	b [len - 1 - i] <- a [i] 
      done
В общем-то поле length в типе array в данном коде лишнее и только мешает - например тем, что приходится доказывать условие a.length = len = b.length, которое в варианте вроде (если бы его язык допускал):

  type array (length : int) 'a model { mutable elts : map int 'a }
    invariant { 0 <= self.length }
val ([]) (a: array length 'a) (i: int) : 'a
    requires { "expl:index in array bounds" 0 <= i < length }
...
let  rev (len : int) (a : array len 'a) (b : array len 'a) 
      ensures  { forall i : int . (0 <= i < len -> b [len - 1 - i] = a [i]) }
	=
      for i =  0 to len - 1 do
	invariant { forall k : int . (0 <= k < i -> b [len - 1 - k] = a [k]) } 
	b [len - 1 - i] <- a [i] 
      done
Оказывается просто излишним.

C другой стороны - наличие инвариантов типов делает довольно многие "красивые" применения зависимых типов просто излишними - половина примеров "зачем они нужны" которые мне приводил в трепе приятель (вроде красночерного дерева с статически гарантируемой красночерностью) инвариантами прописыаются без всяких зависимых типов
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment