Здравствуйте, jazzer, Вы писали:



J> Нет никакой реализации логики (т.е. реальных действий) на типах. На типах реализуются ограничения,
J> которым должен удовлетворять код. При этом в коде реализации самих ограничений могут быть ошибки, естественно.
не совсем понятно где нет реализации логики. у вас или вообще на типах. если вообще на типах то с этим сложно согласиться. давайте возьмем очень простой пример. a = b + c; пускай это строки. тут происходит неявное выделение памяти, которое на си мы бы делали руками. это -- логика.

некоторые языки типа js могут вести себя неожиданно для си-программиста и вместо того, чтобы объединять строки -- переводят из строки в число (если переводится) и складывать их как числа. это уже некислый слой логики (хотя и неожиданный порой и для самих js программистов).

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

тип "градусы ххх" (цельсия, фаренгейта, кельвина) так же может автоматически складывать c = a + b даже если а это по цельсию, а b -- по фаренгейту. более того, тип c, в котором записан результат, интересуется какой это именно градус только при выводе на экран. тогда мы уже явно указываем какие градусы нам нужны. как, впрочем, и при иницилизации (но тут как бы очевидно).

идем дальше. конструкция for line in lines может читать файл по строкам. или массив по элементам. и где же эта логика? так она в типе и реализована. чудес не бывает. реализацию можно прятать, но она таки должна быть. однако, именно это позволяет одной и той же конструкцией и читать массив, и файл, и... да что угодно! хоть базу данных. при этом в последнем случае реализация "скрытой" логики может быть совсем уж нетривиальной. у меня такая конструкция с одинаковой легкостью выводит на экран строку по символам или дизассемблирует хоть x86, хоть jvm. дизассемблер (или парсер) имеет сложную реалиацию, но "каркас" об этом не знает. каркасу абсолютно все равно массив ли это байт (символов) или байт-код.

так вот, если вчера было ноль по цельсию, а сейчас 14 по фаренгейту и я хочу узнать дельту и эту дельту выводит код вида a — b, то что же это такое как не реализация _логики_ на _типах_ ?! потому что а это один тип, b -- другой. при вычитании одного из другого создается третий тип — кельвина, в котором и хранится результат. а вот при отображении его на экране... ну просто print (a-b) выдаст ошибку. нужно писать что-то типа print "температура %Ц" % (a — b), где %Ц у нас задает формат вывода -- цельсия.

мы получаем код, который легко расширять, который легко писать и легко сопровождать. если это не реализация логики на типах, то что это? это ни разу не есть ограничения операций над типами. это ни разу не более строгие проверки сложения целься с фаренгейтами. это как раз решение проблемы: что делать (элегантно) если у нас температура постоянно то в одном, то в другом, то вообще в третьем...


вот, кстати, пример из жизни. ВРЕМЯ. оно же, сволочь, у всех нас разное. мой вариант решения проблемы (чтобы избежать ошибок). если мы реализуем _логику_ на различных типах времени, то мы только указаываем типы. и раз уж зашел разговор о времени -- когда отмечать сто пятьсот лет крещения руси? сколько с той поры было календарных реформ? грубо говоря, если летописцы говорят, что событие произошло 1 декабря 865 года в риме, а нам нужно сколько с той поры прошло до 1 декабря 1865 года в питере -- это СУРОВЫЙ квест. на самом деле нет. на самом деле это легко разрулить. пускай тип ДАТА все знает о календарных реформах разных стран во все времена. нам-то до этого какое дело? у нас задача решается простым вычитанием. и пускай за этим вычитанием не только 100500 строк кода, но еще и База Знаний.

сорри за неровный стиль изложения. но, думаю, мысль моя понятна. семантика операции + и — может быть сколь угодно сложной и если она выполняется над разными типами -- это хороший способ спрятать под капот реализацию логики.