![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Еще про статическую типизацию
Mar. 24th, 2008 09:37 amНемного подумал про статическую типизацию.
Буду использовать определение: статическая типизация — это такая система, которая по тексту программы может доказать какие-то свойства программы в отношении типов данных.
Подобным образом заданная статическая типизация может использоваться для:
Собственно статическую типизацию можно представить как предикат ST(Property,P), где Property — некоторое свойство, а P — кусок программы, который проверяет, выполняется ли свойство Property в P. Теперь, подставляя Property и P, можно проверять нужные свойства. Например, Property=«Переменная V имеет тип T», или Property=«К переменной V применима операция O», и т.п.
Но это в идеальном случае. В реальности же, мы не можем построить такой предикат ST даже для простейших случаев (например, Property=«Переменная V имеет тип T»), а лишь его аппроксимацию (из-за неразрешимости ряда проблем). То есть, ST — это уже не предикат, а функция, область значений которой лежит либо в трехнзначной логике, либо в нечеткой логике, но никак не в булевой логике (а если, все-таки, мы построим этот ST так, что его область значений лежит в булевой логике, то мы будем обманывать сами себя, в меньшей или большей степени в зависимости от качества аппроксимации).
То есть, статическая типизация может и не давать точного ответа на вопрос, выполняется ли свойство Property в P, или нет. К сожалению, это часто (почти всегда) упускается из внимания при создании ЯП.
Теперь, рассмотрим, например, короткую программу на C# (только для примера, во многих других языках будет то же самое).
Эта программа не скомпилируется. Хотя, любой нормальный программист скажет, что если бы правила языка подразумевали динамическую типизацию, а не статическую, то должен был получиться вполне определенный и корректный результат (а именно, должна была быть выведена строка «1+2=3»).
Та же программа на питоне:
Эта программа нормально исполняется и выводит «1+2=3».
На простом примере видно, что если реализовывать статическую типизацию определенным образом, то это накладывает ограничение на программиста (многие корректные программы1 не могут быть написаны). Полностью динамическая типизация (т.е., отказ от динамической типизации вообще) не ограничивает программиста в написании корректных программ, но взамен этого компилятор не может находить огромное число ошибок, которые мог бы находить.
Можно привести более сложные примеры. Например, одна часть программы динамически генерирует другие программы, а другая часть программы использует сгенерированные программы. Необходимо удостовериться в том, что сгенерированные программы используются корректно. И, например, проверить то, что xml-документ, генерируемый в программе, удовлетворяет указанной схеме. Динамически это можно сделать и делается. Весь вопрос в том, можно ли это сделать статически? И если нельзя, то как поступать? Априори считать, что если не можем доказать свойство, то оно не выполняется? Тогда необходимы всякие извороты в виде type-cast'ов и подобных вещей.
Всякие различные усовершенствования систем типов (templates, GADT, dependent types) сужают то множество программ, в которых статическая типизация не может доказать выполнение свойств, но не устраняет его полностью.
Поэтому, хотелось бы видеть в ЯП следующие особенности статической типизации:
Было бы интересно увидеть это в лиспе. Если летом будет время, то попробую заняться этим :)
1под корректными программами подразумеваю такие программы, для которых выполняются все свойства из множества свойств, определяющих корректность получаемых результатов и корректность исполнения, независимо от того, доказуемы ли эти свойства или нет.
Буду использовать определение: статическая типизация — это такая система, которая по тексту программы может доказать какие-то свойства программы в отношении типов данных.
Подобным образом заданная статическая типизация может использоваться для:
- Обнаружения определенного класса ошибок в программе
- Оптимизации
- Ассистирования при написании кода
Собственно статическую типизацию можно представить как предикат ST(Property,P), где Property — некоторое свойство, а P — кусок программы, который проверяет, выполняется ли свойство Property в P. Теперь, подставляя Property и P, можно проверять нужные свойства. Например, Property=«Переменная V имеет тип T», или Property=«К переменной V применима операция O», и т.п.
Но это в идеальном случае. В реальности же, мы не можем построить такой предикат ST даже для простейших случаев (например, Property=«Переменная V имеет тип T»), а лишь его аппроксимацию (из-за неразрешимости ряда проблем). То есть, ST — это уже не предикат, а функция, область значений которой лежит либо в трехнзначной логике, либо в нечеткой логике, но никак не в булевой логике (а если, все-таки, мы построим этот ST так, что его область значений лежит в булевой логике, то мы будем обманывать сами себя, в меньшей или большей степени в зависимости от качества аппроксимации).
То есть, статическая типизация может и не давать точного ответа на вопрос, выполняется ли свойство Property в P, или нет. К сожалению, это часто (почти всегда) упускается из внимания при создании ЯП.
Теперь, рассмотрим, например, короткую программу на C# (только для примера, во многих других языках будет то же самое).
object a = 1;
object b = 2;
Console.WriteLine("{0}+{1}={2}",a,b,a+b);
Эта программа не скомпилируется. Хотя, любой нормальный программист скажет, что если бы правила языка подразумевали динамическую типизацию, а не статическую, то должен был получиться вполне определенный и корректный результат (а именно, должна была быть выведена строка «1+2=3»).
Та же программа на питоне:
a = 1 b = 2 print "%d+%d=%d"%(a,b,a+b)
Эта программа нормально исполняется и выводит «1+2=3».
На простом примере видно, что если реализовывать статическую типизацию определенным образом, то это накладывает ограничение на программиста (многие корректные программы1 не могут быть написаны). Полностью динамическая типизация (т.е., отказ от динамической типизации вообще) не ограничивает программиста в написании корректных программ, но взамен этого компилятор не может находить огромное число ошибок, которые мог бы находить.
Можно привести более сложные примеры. Например, одна часть программы динамически генерирует другие программы, а другая часть программы использует сгенерированные программы. Необходимо удостовериться в том, что сгенерированные программы используются корректно. И, например, проверить то, что xml-документ, генерируемый в программе, удовлетворяет указанной схеме. Динамически это можно сделать и делается. Весь вопрос в том, можно ли это сделать статически? И если нельзя, то как поступать? Априори считать, что если не можем доказать свойство, то оно не выполняется? Тогда необходимы всякие извороты в виде type-cast'ов и подобных вещей.
Всякие различные усовершенствования систем типов (templates, GADT, dependent types) сужают то множество программ, в которых статическая типизация не может доказать выполнение свойств, но не устраняет его полностью.
Поэтому, хотелось бы видеть в ЯП следующие особенности статической типизации:
- Если статическая типизация может доказать, что необходимые для корректности свойства программы не выполняются, то это должно приводить к ошибкам компиляции.
- Если статическая типизация не может доказать, что необходимое для корректности программы свойство выполняется, то это не должно быть ошибкой компиляции, а warning'ом. Либо же, невозможность доказать считается ошибкой компиляции, если программист не вставил явное объявление о том (но в форме type-cast'а, так как это очень-очень нехорошо, а в какой-нибудь другой, более красивой, форме), что такое свойство выполняется, и используется динамическая проверка этого свойства.
Было бы интересно увидеть это в лиспе. Если летом будет время, то попробую заняться этим :)
1под корректными программами подразумеваю такие программы, для которых выполняются все свойства из множества свойств, определяющих корректность получаемых результатов и корректность исполнения, независимо от того, доказуемы ли эти свойства или нет.
