В этой стране даже типы и те зависимые
Насколько я понимаю, в мире пока не существует ни одного полноценного языка программирования общего назначения, который в полной мере поддерживал бы зависимые типы. Если я не ошибаюсь -- всяческие agda2 и coq достаточно ограничены в плане применимости.
Попробую в этом посте поразмышлять на тему зависимых типов в CL. В принципе, сама типизация в CL, конечно, опциональна, но от этого она ничуть не становится ущербной, и кое-что на ее базе изобразить можно.
Что такое вообще эти зависимые типы и нахрена они нужны в реальной жизни? Сразу скажу, что всю связанную с ними математику я даже и не пытался осиливать, поэтому попробую объяснить так, как я понял их практическую пользу.
По-сути, зависимые типы, как и обычные, активно пытаются донести до компилятора максимум информации об используемых в нашей программе данных. Зачем это надо -- понятно: чем больше компилятор знает о данных, тем успешнее он может следить за корректностью программы и генерировать более производительный код.
В отличие от обычных типов, зависимые типы компилятор волен "конструировать" на ходу, согласно собственным гипотезам, которые он сделал, анализируя программу.
Попробую проиллюстрировать на простом примере:
(defun f (x y)
(declare (type fixnum x)
(type fixnum y))
Имеем функцию f, о которой компилятор точно знает, что оба ее аргумента -- fixnum.
(when (and (< 100 x 300) (< 200 y 400))
(values (type-of x)
(type-of y))))
Далее, мы проверяем условие, что 100 < x < 300 и 200 < y < 400 и проходим в случае успеха внутрь sexp'а, отображая типы. Что мы видим в результате?
CL-USER> (f 200 300)
(INTEGER 0 1152921504606846975)
(INTEGER 0 1152921504606846975)
Что x и y как были fixnum'ами, так и остались. Хотя интуитивно понятно, что раз уж мы попали внутрь условия (прошли сравнения), типы должны быть вроде (INTEGER 101 299) для x и (INTEGER 201 399) для y -- это достаточно очевидно любому школьнику в средних классах.
Так вот, компилятор, который умеет так делать, поддерживает зависимые типы. Мало того:
(let ((a (+ y x)))
Переменная a получит тип (INTEGER 302 698).
(let ((s (make-array 100)))
(elt s x))
Вернет ошибку: s получает тип (SIMPLE-VECTOR 100), а левая граница у x -- 101.
(* x x x)
Сгенерирует эффективный код (без точного знания о типе возведение в куб какого-то неизвестного FIXNUM уже может в один регистр и не влезть).
Ну и так далее. Разумеется, желательно, чтобы компилятор с зависимыми типами был чисто функцинальным (иначе, например, уже после проверки на 100 < x < 300 текущий тред может быть прерван, и другой тред может поменять x на 500. Это приведет к рассинхронизации гипотиз компилятора и реального положения вещей). Но это не обязательное требование.
Вернемся к нашим баранам. Давайте теперь попробуем изобразить что-то подобное на CL, используя его систему типов и макросистему. Сразу оговорюсь, что моя основная (и пока ваще единственная) причина использования типизации в лиспе -- это оптимизация ассемблера при компиляции. Отслеживание машиной корректности моей программы мне не нужно, да и не интересует меня никак.
Рассмотрим такой пример (несколько искусственный, ну да ладно):
(defmacro with-matrix ((var width height) &body body)
`(let ((,var (make-array ,(* width height) :element-type 'single-float)))
(macrolet ((item (row col)
`(elt ,',var (+ (* ,row ,',width) ,col))))
,@body)))
Суть вкрадце: предоставляем инструмент для работы с матрицей, основанной на (simple-array single-float *). Разумеется, для этого есть средства disposed-массивов, но пока забудем про него.
С этим понятно. Сделаем на его основе другой макрос:
(defmacro with-cleared-matrix ((var width height) &body body)
(with-gensyms (row col)
`(with-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the fixnum ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the fixnum ,col) from 0 below ,width)
(setf (item ,row ,col) 0.0)))
,@body)))
То же самое, но матрицу мы получаем проинициализированную нулями (забьем еще разок на тот факт, что она и так проинициализирована нулями).
Вот на этом примере компилятор уже может запутаться с типами:
(defun test-matrix ()
(declare (optimize (speed 3) (safety 0)))
(with-cleared-matrix (m 10 5)
m))
Компиляция завершается с четырьмя замечаниями, сводящимися к:
; note: forced to do GENERIC-* (cost 30)
; note: forced to do GENERIC-+ (cost 10)
Проблема возникает в трансляции двухмерных координат (row col) в плоские (index) по формуле index = row * 5 + col, определенной в сгенерированном macrolet макросом with-matrix.
Компилятор справедливо замечает, что если он возьмет row (fixnum) и умножит его на пять, то результат может в fixnum уже не влезть. А ежели к этому результату добавить еще один fixnum, то и подавно.
Давайте успокоим компилятор, сообщив ему о границах значений:
(defmacro with-cleared-matrix ((var width height) &body body)
(with-gensyms (row col)
`(with-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,height) ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,width) ,col) from 0 below ,width)
(setf (item ,row ,col) 0.0)))
,@body)))
Теперь компиляция test-matrix завершается без ругани. Почему я установил интервалы в (-1 5) и (-1 10) для счетчиков? Из-за особенностей реализации iter: если натравить на конструкцию с циклом macroexpand, можно увидеть, что в правиле (for .. from a below b) счетчик инициализируется с -1 (на единицу меньше нижнего значения a), а для окончания цикла используется условие "пока счетчик меньше b". Поэтому диапазон значений пришлось чуток расширить.
А теперь давайте рассмотрим третье поколение наших странных макросов. Пусть нам теперь создают матрицу, у которой левая половина обнулена, а правая заполнена единицами:
(defmacro with-right-half-one-matrix ((var width height) &body body)
(with-gensyms (row col)
(let ((half-width (truncate (/ width 2))))
`(with-cleared-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,height) ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the (integer ,(1- half-width) ,width) ,col) from ,half-width below ,width)
(setf (item ,row ,col) 1.0)))
,@body))))
Тип счетчика по колонкам мы ограничили аналогично вышеприведенному примеру, расширив в обе стороны на единичку. Вроде все выглядит корректно, но теперь test-matrix компилироваться перестала. Почему? В макроэкспанде соответствующего iter'а мы видим инициализацию счетчика в нуль, а левая граница счетчика у нас 4.
Можно, конечно, понизить ее до нуля, но в CL существует более корректное в этом плане решение: составные типы.
(for (the (or (integer 0 0) (integer ,(1- half-width) ,width)) ,col) from ,half-width below ,width)
Тобишь, либо нуль, либо диапазон от 4 до 10.
Вроде все нормально, но тип получается слишком длинный, а нужен он будет довольно часто. И тут нам на помощь приходит такая малоизвесная вещь в CL как deftype -- конструктор собственных типов!
(deftype int/0 (low-bound hi-bound)
`(or (integer 0 0) (integer ,low-bound ,hi-bound)))
И теперь можно переписать счетчик так:
(for (the (int/0 ,(1- half-width) ,width) ,col) from ,half-width below ,width)
Ну красота. В принципе, это довольно малая часть того, что умеет deftype, можете еще почитать про него в CLHS, ну и на закуску весьма любопытную статью про типизацию в CL.
Собственно, что я хотел показать. Моя цель достигнута: с помощью макросистемы и родной лисповой типизации я добился какого-то подобия зависимых типов в CL, достаточного, чтобы снабдить компилятор необходимой информацией для генерации оптимизированного кода. В принципе, если в этом направлении продолжать думать, можно пойти еще дальше в эмуляции полноценных зависимых типов.
Попробую в этом посте поразмышлять на тему зависимых типов в CL. В принципе, сама типизация в CL, конечно, опциональна, но от этого она ничуть не становится ущербной, и кое-что на ее базе изобразить можно.
Что такое вообще эти зависимые типы и нахрена они нужны в реальной жизни? Сразу скажу, что всю связанную с ними математику я даже и не пытался осиливать, поэтому попробую объяснить так, как я понял их практическую пользу.
По-сути, зависимые типы, как и обычные, активно пытаются донести до компилятора максимум информации об используемых в нашей программе данных. Зачем это надо -- понятно: чем больше компилятор знает о данных, тем успешнее он может следить за корректностью программы и генерировать более производительный код.
В отличие от обычных типов, зависимые типы компилятор волен "конструировать" на ходу, согласно собственным гипотезам, которые он сделал, анализируя программу.
Попробую проиллюстрировать на простом примере:
(defun f (x y)
(declare (type fixnum x)
(type fixnum y))
Имеем функцию f, о которой компилятор точно знает, что оба ее аргумента -- fixnum.
(when (and (< 100 x 300) (< 200 y 400))
(values (type-of x)
(type-of y))))
Далее, мы проверяем условие, что 100 < x < 300 и 200 < y < 400 и проходим в случае успеха внутрь sexp'а, отображая типы. Что мы видим в результате?
CL-USER> (f 200 300)
(INTEGER 0 1152921504606846975)
(INTEGER 0 1152921504606846975)
Что x и y как были fixnum'ами, так и остались. Хотя интуитивно понятно, что раз уж мы попали внутрь условия (прошли сравнения), типы должны быть вроде (INTEGER 101 299) для x и (INTEGER 201 399) для y -- это достаточно очевидно любому школьнику в средних классах.
Так вот, компилятор, который умеет так делать, поддерживает зависимые типы. Мало того:
(let ((a (+ y x)))
Переменная a получит тип (INTEGER 302 698).
(let ((s (make-array 100)))
(elt s x))
Вернет ошибку: s получает тип (SIMPLE-VECTOR 100), а левая граница у x -- 101.
(* x x x)
Сгенерирует эффективный код (без точного знания о типе возведение в куб какого-то неизвестного FIXNUM уже может в один регистр и не влезть).
Ну и так далее. Разумеется, желательно, чтобы компилятор с зависимыми типами был чисто функцинальным (иначе, например, уже после проверки на 100 < x < 300 текущий тред может быть прерван, и другой тред может поменять x на 500. Это приведет к рассинхронизации гипотиз компилятора и реального положения вещей). Но это не обязательное требование.
Вернемся к нашим баранам. Давайте теперь попробуем изобразить что-то подобное на CL, используя его систему типов и макросистему. Сразу оговорюсь, что моя основная (и пока ваще единственная) причина использования типизации в лиспе -- это оптимизация ассемблера при компиляции. Отслеживание машиной корректности моей программы мне не нужно, да и не интересует меня никак.
Рассмотрим такой пример (несколько искусственный, ну да ладно):
(defmacro with-matrix ((var width height) &body body)
`(let ((,var (make-array ,(* width height) :element-type 'single-float)))
(macrolet ((item (row col)
`(elt ,',var (+ (* ,row ,',width) ,col))))
,@body)))
Суть вкрадце: предоставляем инструмент для работы с матрицей, основанной на (simple-array single-float *). Разумеется, для этого есть средства disposed-массивов, но пока забудем про него.
С этим понятно. Сделаем на его основе другой макрос:
(defmacro with-cleared-matrix ((var width height) &body body)
(with-gensyms (row col)
`(with-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the fixnum ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the fixnum ,col) from 0 below ,width)
(setf (item ,row ,col) 0.0)))
,@body)))
То же самое, но матрицу мы получаем проинициализированную нулями (забьем еще разок на тот факт, что она и так проинициализирована нулями).
Вот на этом примере компилятор уже может запутаться с типами:
(defun test-matrix ()
(declare (optimize (speed 3) (safety 0)))
(with-cleared-matrix (m 10 5)
m))
Компиляция завершается с четырьмя замечаниями, сводящимися к:
; note: forced to do GENERIC-* (cost 30)
; note: forced to do GENERIC-+ (cost 10)
Проблема возникает в трансляции двухмерных координат (row col) в плоские (index) по формуле index = row * 5 + col, определенной в сгенерированном macrolet макросом with-matrix.
Компилятор справедливо замечает, что если он возьмет row (fixnum) и умножит его на пять, то результат может в fixnum уже не влезть. А ежели к этому результату добавить еще один fixnum, то и подавно.
Давайте успокоим компилятор, сообщив ему о границах значений:
(defmacro with-cleared-matrix ((var width height) &body body)
(with-gensyms (row col)
`(with-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,height) ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,width) ,col) from 0 below ,width)
(setf (item ,row ,col) 0.0)))
,@body)))
Теперь компиляция test-matrix завершается без ругани. Почему я установил интервалы в (-1 5) и (-1 10) для счетчиков? Из-за особенностей реализации iter: если натравить на конструкцию с циклом macroexpand, можно увидеть, что в правиле (for .. from a below b) счетчик инициализируется с -1 (на единицу меньше нижнего значения a), а для окончания цикла используется условие "пока счетчик меньше b". Поэтому диапазон значений пришлось чуток расширить.
А теперь давайте рассмотрим третье поколение наших странных макросов. Пусть нам теперь создают матрицу, у которой левая половина обнулена, а правая заполнена единицами:
(defmacro with-right-half-one-matrix ((var width height) &body body)
(with-gensyms (row col)
(let ((half-width (truncate (/ width 2))))
`(with-cleared-matrix (,var ,width ,height)
(iter (declare (declare-variables))
(for (the (integer -1 ,height) ,row) from 0 below ,height)
(iter (declare (declare-variables))
(for (the (integer ,(1- half-width) ,width) ,col) from ,half-width below ,width)
(setf (item ,row ,col) 1.0)))
,@body))))
Тип счетчика по колонкам мы ограничили аналогично вышеприведенному примеру, расширив в обе стороны на единичку. Вроде все выглядит корректно, но теперь test-matrix компилироваться перестала. Почему? В макроэкспанде соответствующего iter'а мы видим инициализацию счетчика в нуль, а левая граница счетчика у нас 4.
Можно, конечно, понизить ее до нуля, но в CL существует более корректное в этом плане решение: составные типы.
(for (the (or (integer 0 0) (integer ,(1- half-width) ,width)) ,col) from ,half-width below ,width)
Тобишь, либо нуль, либо диапазон от 4 до 10.
Вроде все нормально, но тип получается слишком длинный, а нужен он будет довольно часто. И тут нам на помощь приходит такая малоизвесная вещь в CL как deftype -- конструктор собственных типов!
(deftype int/0 (low-bound hi-bound)
`(or (integer 0 0) (integer ,low-bound ,hi-bound)))
И теперь можно переписать счетчик так:
(for (the (int/0 ,(1- half-width) ,width) ,col) from ,half-width below ,width)
Ну красота. В принципе, это довольно малая часть того, что умеет deftype, можете еще почитать про него в CLHS, ну и на закуску весьма любопытную статью про типизацию в CL.
Собственно, что я хотел показать. Моя цель достигнута: с помощью макросистемы и родной лисповой типизации я добился какого-то подобия зависимых типов в CL, достаточного, чтобы снабдить компилятор необходимой информацией для генерации оптимизированного кода. В принципе, если в этом направлении продолжать думать, можно пойти еще дальше в эмуляции полноценных зависимых типов.