Большинство из вас наверняка знакомы с этим фрагментом кода:
List<Integer>
Это синтаксис для универсальных (параметризованных) типов, который доступен в Java с 2004 года. И, конечно, вы знаете, что вы должны поместить в скобки: тип (класс или интерфейс). Но вы когда-нибудь задумывались, что еще мы могли бы использовать там, кроме типов?
Например, как насчет:
List<Integer><2> // not legal Java
Вместо типа я теперь использую значение определенного типа (целое число) в качестве параметра типа.
Что это может означать? Ну, так как я создаю синтаксис (и я буду использовать эту свободу чуть больше в оставшейся части этого поста), я мог бы также придумать, что это значит. Как насчет того, чтобы сказать, что целое число здесь представляет размер списка?
Другими словами:
List<Integer><2> l = List(1, 2); // compiles List<Integer><2> l = List(1); // does not compile
Или мы можем решить, что если индексируемый нами тип (Integer) поддерживает оператор +, то это значение является суммой всех его элементов:
List<Integer><2> l = List(2); // compiles List<Integer><2> l = List(0, 1, 1); // compiles List<Integer><2> l = List(0, 1); // does not compile
Вы, наверное, уже догадались: List <Integer> <2> является зависимым типом. Тип, параметризованный не только другими типами, но и значениями других типов. Правильная терминология здесь такова, что тип «индексируется» по значению (не путать со значением «индекс» в контексте списка).
Различные значения определяют разные типы, и, конечно, нам не нужно останавливаться на этом: значение может иметь тип, отличный от Integer, например, String (List <Integer> <«abc» >> и т. Д. Очевидно, что вы Не ограничиваясь списком, вы можете представить себе карты, деревья или любой другой параметризованный тип.
К сожалению, веселье на этом заканчивается. В то время как привлекательность зависимых типов выглядит сильной, на самом деле очень сложно перейти в область конкретного кода.
Давайте вернемся к нашему списку: как нам манипулировать зависимым списком с фиксированным размером, чтобы компилятор отмечал любую попытку нарушить это ограничение, отказываясь проверять тип нашей программы?
Я использовал простую ситуацию в приведенных выше фрагментах кода, инициализируя мои списки константами, но, очевидно, это не очень полезно: вы почти никогда не используете списки, которые инициализируются константами во время объявления, за исключением, может быть, в тестах. Очень часто мы создаем список, заполняем его во время выполнения каким-то алгоритмом и, если он изменчив, мы изменяем его различными способами.
Во-первых, нам нужно создать наш список, не добавляя в него никаких элементов, но не нарушает ли это ограничение?
List<Integer><2> l = new ArrayList<Integer><2>(); // should not compile
Если мы не можем даже скомпилировать это, то мы никогда не сможем использовать ничего, кроме списков, инициализированных с константами, поэтому давайте представим, что компилятор позволит нам сойти с рук. Как мы сейчас заполняем наш список? Как оказалось, мы не достигли большого прогресса:
List<Integer><2> l = new ArrayList<Integer><2>(); // assume this compiles l.add(1); // will not compile l.add(2); // would compile if the previous linecompiled
Наличие списка с одним элементом будет ошибкой типа, поэтому вторая строка во фрагменте выше не должна компилироваться. Вы можете обойти это ограничение, добавив add (), возвращающий другой список другого типа . Это все еще будет список, но проиндексированный по значению +1 исходного. И теперь вы должны определить, как List <Integer> <1> и List <Integer> <2> могут взаимодействовать и насколько они совместимы ..
Мы находимся в тупике, и если мы хотим добиться прогресса, мы должны сконфигурировать компилятор, чтобы все больше освобождать условие зависимой типизации. Например, возможно, он применил бы проверку типов только к операциям, которые обращаются к содержимому списка (чтение), но он не будет выполнять никакой проверки для операций, которые его изменяют (запись). Отчасти отказ от образца строителя, когда объекту разрешено находиться в незаконном состоянии в четко определенных границах.
Тем не менее, бремя проверки типов станет довольно большим и потребует от компилятора не только генерировать код, но и фактически выполнять анализ ветвлений, чтобы убедиться, что количество элементов списка всегда удовлетворяет зависимости в определенных заданных точках.
Также обратите внимание, что я упустил еще один нетривиальный аспект: как мы можем научить компилятор, что означает приведенный выше синтаксис? Должен ли он быть настраиваемым или частью определения языка? Какие типы разрешено индексировать? Какие типы разрешены в качестве индексов? Как взаимодействуют типы одной семьи, но с разными показателями?
К настоящему времени должно стать все более очевидным, что изменяемые типы не могут быть реально зависимыми, что ограничивает зависимые типы неизменяемыми. Насколько это полезно на самом деле? Все еще работаю над этим.
Если тема вас интересует, лучшая статья, которую я нашел до сих пор, это « Зависимые типы в работе» (PDF) , представляющая собой краткое введение зависимых типов через Agda. Agda, вероятно, является первым языком, на который вы должны смотреть, поскольку он гораздо более поздний, чем Coq (который я уже изучал в рамках своей докторской диссертации пятнадцать лет назад, так как я работал в том же исследовательском институте, который создал Coq). Эта статья (и большая часть литературы по этому вопросу) не затрагивает ни одной из тем, которые я описал в этом коротком введении, они больше сосредоточены на описании того, как вы можете использовать Agda для формализации доказательств вашей системы типов, что, в свою очередь, даст вам руководство о том, как должна быть реализована ваша проверка типов.
И если у вас есть интересные практические примеры зависимых типов, комментируйте!
С http://beust.com/weblog/2011/08/18/a-gentle-introduction-to-dependent-types/