Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Categories:

Зависимые типы для дошкольников

Мне вчера показалось, что я наконец понял зависимые типы. Как следствие, я придумал объяснение понятия зависимых типов для мальчиков-дебилов.

Допустим, у нас есть реализация абстрактного типа данных массива, и функция append, соединяющая два маленьких массива в большой. Для проверки того, что всё у нас работает правильно, мы пишем юнит-тест:
a = [1, 2]
b = [3, 4, 5]
c = append(a, b)
assert (length (append [1, 2] [3, 4, 5])) == 5)
Есть системы, позволяющие генерировать серию тестов (насколько я понимаю, Haskell QuickCheck делает именно это):
setrandomseed 90484
a = makerandomarray
b = makerandomarray
c = append a b
assert (length(c) == length(a) + length(b))
Исполнение такого теста 10 000 раз даст немного больше уверенности, чем один-единственный тест, но во-первых, надо писать makerandomarray, во-вторых, частные случаи все равно скорее всего будут пропущены.

Идеальный юнит-тест выглядел бы так:

Дано:
a - произвольный массив
b - произвольный массив
c = append a b
Доказать:
length(c) == length(a) + length(b)
Существуют верификаторы программ, способные автоматически выполнять подобные доказательства, проверяя все частные случаи. Например, для случая append они выполняют точно такое же классическое доказательство по индукции, которое Вы бы выполнили сами вручную. Процесс такого доказательства традиционно называется проверкой типов.

Если верификатор может доказывать высказывания, содержащие лишь типы ("доказать, что если а и б - произвольные массивы, то  результат аppend - тоже именно массив, а не целое число") - то мы имеем дело с "обычной" системой типов.

Если верификатор настолько умён, что может доказывать утверждения не только о типах, но и о значениях - то система типов называется "системой зависимых типов".

На некоем псевдохаскеле с зависимыми типами запись данного юнит-теста могла бы выглядеть так:
data Nat = 0 | Succ a where
	a :: Nat

+ :: Nat -> Nat -> Nat
+ a 0 = a
+ a (Succ b) = Succ (+ a b) 

data Vector :: * Nat 
data Vector type 0 = VNil
data Vector type (Succ c) = VCons a b where
	b :: Vector type c
	VCons :: a -> Vector a b -> Vector a (Succ b)) where
		b :: Nat
		a :: *

append :: Vector type a -> Vector type b -> Vector type (+ a b)
append a VNil = a
append VNil a = a
append (VCons a b) c = VCons a (append b c)
Я специально привел не только сам юнит-тест (определение типа append), но и все остальные аксиомы, находящиеся в стандартной библиотеке и описывающие семантику VCons, Nil, Vector и +, которые доказыватель будет использовать в процессе доказательства.

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

1) Доказыватель снабжается эвристиками, позволяющими проводить доказательства в некоторых случаях, и признающий некоторые верные теоремы неверными просто из-за того что он не умеет их доказывать. Таким путем пошли разработчики Cayenne - система типов этого языка undecidable.

2) Ограничить входной язык таким образом, чтобы на нем можно было формулировать только доказуемые теоремы. Оказывается, для этого достаточно отказаться от рекурсии общего вида, и разрешить только структурную рекурсию, записываемую с помощью специальных встроенных в язык функций вроде natrec и listrec ("натуральной" и "списковой" рекурсий). Таким путем пошли разработчики языка Epigram, с вполне себе decidable системой типов.

Да, как результат таких ограничений - на Epigram невозможно написать функцию, возвращающую жопу _|_
Tags: compiler design
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.
  • 15 comments