>> Ругать получившуюся систему типов можно будет затем лишь от непонимания причинно-следственных связей характеристик языка и подходящей под эти характеристики системы типов.
VE>Т.е. если я понимаю причинно-следственные связи характеристик языка, то ругать уже не буду вне зависимости от того, нравятся мне такие характеристики или нет? Интересное мнение.
Ес-но, если тебе некие характеристики языка не важны, но они, в свою очередь являются определяющими для системы типов, возможной в этих характеристиках, то надо брать другой язык. Т.е. сам смори что тебе первично — система типов инструментария или характеристики порождаемого инструментарием результата.
Здравствуйте, vdimas, Вы писали:
V>Здравствуйте, VoidEx, Вы писали:
VE>>Тогда if-else тоже динамическая типизация.
V>Если при этом проверяется внутреннее устройство данных, то бишь их тип — несомненно.
Т.е. всегда. Ибо в чём фундаментальное отличие нижеприведённых примеров?
if (x < 0)
foo1(x) // x is (a:int){a<0}else
foo2(x) // x is (a:int){a>=0}
if (isChild1(p))
foo3(p) // x is Child1*else
foo4(p) // x is Child2*
Вы могли бы сказать, что в первом случае у нас используется само число, в во втором доступ к членам, но
1. Это далеко не всегда так, может, foo3 и foo4 этот указатель в списки добавляют
2. Разницы всё равно нет, так как foo1 и foo2 могут на основе значения бегать по таблицам, использовать числа как смещения и т.п. Грубо говоря вообще можно написать такой код, что foo1 и foo2 будут через таблицы эмулировать доступы в объектам.
VE>>Во-первых, как это нету?
V>Так что нету. Потому что нет параметризации типов константами и нет compile-time диспетчеризации по этим константам и нет частичного или явного инстанциирования шаблонных типов для конкретных комбинаций аргументов. Есть только такое инстанциирование для ф-ий.
Чой-то нету-то? Там вообще макросы есть, если что.
VE>>Во-вторых, можно пример, когда static_if не является сам по себе костылём?
V>Ха. Тогда любая статическая система типов — это костыль сам по себе, т.к. это способ перенести ограничения прикладной логики на компилятор.
Неверное обобщение. Если static_if используется для диспетчеризации, то для этого есть и другие механизмы. При этом с учётом того, что в Haskell никто не использует static_if, есть основания полагать, что все use-case покрываются другими средствами. Причём тут вся статическая типизация — не ясно.
V>Я могу спросить в ответ привести пример, когда классы типов Хаскеля не являются костылем?
А они костыль.
VE>>Можно пример в псевдокоде? Как предполагается это указывать?
DG>вообще, что интересует? нотация, какая-то часть семантики?
Какие типы "грязи" предлагаются? Зависимость от конкретной внешней переменной? Использование состояние? Ввод-вывод?
Вроде как в Disciple все функции могут иметь эффект, причём выводимый автоматически. Например putStrLn там имеет тип что-то вроде String -{!Console}-> ()
При этом в обычном коде это {!Console} писать не надо, хотя можно.
Посмотрите по ссылке (я выше давал), скажите, в чём не сходится с вашим представлением.
VE>>Т.е. всегда. Ибо в чём фундаментальное отличие нижеприведённых примеров?
DG>вроде о том и речь, что ПМ это лишь красивый сахар для последовательности if/else-ов
Если смотреть с этой стороны, то с этим никто не спорит. Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили.
Если смотреть в целом, то всё-таки нет, ибо паттерны могут быть вложенными, есть view-patterns, в Agda для функции, определённой через ПМ можно проводить доказательства (т.к. например для оператора сравнения будет существовать утверждение типа succ x == succ y = x == y), а через if-else будет значительно сложнее (т.к. приведённое выше утверждение уже отсутствует и им не попользуешься при доказательствах, его само сначала придётся доказать), и т.п.
V>Я тебя спросил — покажи как это работает в рантайм? Ведь вызываемая затем ф-ия scalarProduct — рекурсивная, а глубина рекурсии заведомо неизвестна. Т.е. я понимаю твои предположения, если полностью раскрутить и переписать рекурсию, просчитав всё с конца списка. Давай тогда добавим побочный эффект в код scalarProduct, чтобы избежать этого. Думаю, добавление IO не должно сломать тайпчекер.
в данном случае речь о том, что scalarProduct в runtime-е будет следующим с гарантией, что First никогда не выкинет исключение, и что закоментированный if не нужен:
int scalarProduct(as, bs)
{
//if(as == Nil && bs != Nil || as != Nil && bs == Nil)
// throw new Exception("длина списков не совпадает");if(as == Nil)
return 0;
return as.First() * bs.First() + scalarProduct(as.Tail(), bs.Tail());
}
VE>Если смотреть с этой стороны, то с этим никто не спорит. Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили.
в моем понимании, динамическая типизация — это когда в рантайме есть if на основе признака типа или виртуальный вызов на основе vtable типа. И то, и другое — роняет производительность.
а почти весь ПМ (при условии, что есть несколько веток) в это и транслируется.
VE>Если смотреть в целом, то всё-таки нет, ибо паттерны могут быть вложенными, есть view-patterns, в Agda для функции, определённой через ПМ можно проводить доказательства (т.к. например для оператора сравнения будет существовать утверждение типа succ x == succ y = x == y), а через if-else будет значительно сложнее (т.к. приведённое выше утверждение уже отсутствует и им не попользуешься при доказательствах, его само сначала придётся доказать), и т.п.
да, это всё есть и очень полезно, но динамическую типизацию уберет только в редких случаях
VE>Посмотрите по ссылке (я выше давал), скажите, в чём не сходится с вашим представлением.
сходу не вижу примера самого интересного, когда при композиции та или иная грязь пропадает
VE> isNumber (needNoState rnd)
тут основной подвох, что необходимо сначала в нужное место вставить нужный needNoState, а потом при рефакторинге в:
isNumber-Больше-Одной-Второй(needNoState rnd)
не забыть его убрать.
те же явные касты (вид в профиль) с теми же последствиями
VE>>Посмотрите по ссылке (я выше давал), скажите, в чём не сходится с вашим представлением.
DG>сходу не вижу примера самого интересного, когда при композиции та или иная грязь пропадает
Не уверен, что там это есть. Тогда соответственно назревает вопрос. Как вы предлагаете проверять то, что грязь убирается?
Можно на таком примере: isEven (rnd * 2)
Ну или на ваш вкус
VE>> isNumber (needNoState rnd)
DG>тут основной подвох, что необходимо сначала в нужное место вставить нужный needNoState, а потом при рефакторинге в: DG>isNumber-Больше-Одной-Второй(needNoState rnd) DG>не забыть его убрать. DG>те же явные касты (вид в профиль) с теми же последствиями
Явные касты — это благо. Именно потому, что при рефакторинге вас мордой ткнут и придётся убрать. А вот если молча проглотит, будет беда.
VE>>Если смотреть с этой стороны, то с этим никто не спорит. Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили.
DG>в моем понимании, динамическая типизация — это когда в рантайме есть if на основе признака типа или виртуальный вызов на основе vtable типа. И то, и другое — роняет производительность.
Любой if — это вызов блока в if или блока в else на основе таблицы из true/false.
DG>а почти весь ПМ (при условии, что есть несколько веток) в это и транслируется.
Любая программа содержит условные переходы, но динамической типизацией это называть было бы крайне странно.
Поэтому первостепенной задачей было бы как раз решить, что же такое динамическая типизация.
То, что при наличии разных вариантов у АлгТД происходит ветвление — это динамическая типизация в той же мере, что и ветвление по 0 и не 0 в факториале. Назвать это динамической типизацией можно только при большой фантазии, да и то, с натяжкой.
С другой стороны динамическую типизацию можно было представить как кортеж из имени типа и значения.
Фундаментальную разницу я вижу в том, что при динамической типизации тип ровно один: dynamic.
VE>Явные касты — это благо. Именно потому, что при рефакторинге вас мордой ткнут и придётся убрать. А вот если молча проглотит, будет беда.
говоря явный каст, я имел ввиду reinterpreted_cast или dynamic_cast, т.е. такой cast валидность которого не проверяется компилятором
извини, что сказал двусмысленно.
VE> Любая программа содержит условные переходы, но динамической типизацией это называть было бы крайне странно. VE> Поэтому первостепенной задачей было бы как раз решить, что же такое динамическая типизация.
весь смысл статической типизации, что она может убирать if-ы
имея следующий код:
T Sum<T>(this IEnumerable<T> items)
{
var sum = default(T);
foreach (var item in items)
sum = Sum(sum, item);
return sum;
}
int Sum(int a, int b)
{
return a + b;
}
double Sum(double a, double b)
{
return a + b;
}
void Main()
{
Enumerable.Range(1, 10).Sum().ToConsole();
}
при сильной статической типизации можно ожидать, что при исполнении будет следующий код без всяких if-ов:
Int Sum_Int(this IEnumerable<int> items)
{
var sum = 0;
foreach (var item in items)
sum = Sum_Int(sum, item);
return sum;
}
int Sum_Int(int a, int b)
{
return a + b;
}
void Main()
{
Enumerable.Range(1, 10).Sum_Int().ToConsole();
}
без статической типизации при исполнении не будет ничего лучше, чем следующий код:
object Sum(this items)
{
var sum = null;
foreach (var item in items)
sum = Sum(sum, item);
return sum;
}
object Sum(a, b)
{
if (a is int && b is int)
return (int)a + (int)b;
if (a is double && b is double)
return (double)a + (double)b;
throw new Exception(..);
}
void Main()
{
Enumerable.Range(1, 10).Sum().ToConsole();
}
данный код достаточно сильно тормозит по сравнению с предыдущим, потому что на каждой итерации идут проверки.
и я утверждаю, что ПМ в основном именно в такой тормозной код и разворачивается.
Здравствуйте, DarkGray, Вы писали:
DG>весь смысл статической типизации, что она может убирать if-ы
Я бы сказал, что это побочный её эффект. Тем не менее в таком определении типизация не статическая или динамическая, а более или менее статическая.
В любой программе у нас так или иначе будут if'ы, без ветвлений ничего полезного не написать.
Мы могли бы ограничиться кортежами и целыми числами, и как будто бы и нет динамической типизации, но нам бы пришлось её эмулировать так или иначе через те самые if'ы.
АлгТД решает эту проблему. if при обработке АлгТД никуда не убрать, но его никуда не уберёшь в любой программе. Просто тут он в АлгТД, а там он был бы где-то ещё.
Тем не менее, в языке с зависимыми типами и теоремами и для АлгТД можно было бы выбрать ветку без if'а, но в частных случаях.
В общем, от ввода АлгТД "динамичности" не прибавляется, она просто перекочёвывает из if-else'ов в АлгТД, вот и всё.
DG>и я утверждаю, что ПМ в основном именно в такой тормозной код и разворачивается.
Нет. С ПМ у вас ровно первый вариант. Проверка на окончание итерирования аналогична проверке, Null ли список или Cons head tail. Функция суммирования же используется одна и никакого диспатча нет.
Я же утверждаю, что когда ПМ разворачивается в "такой тормозной код", то и без ПМ будет он же.
Основываюсь на том, что "хороший код" без ПМ можно перевести в код с ПМ, где классы перейдут в кортежи, а ветвления в варианты АлгТД (например nullable ссылки (ветвление по null и not-null) в Maybe).
VE>Нет. С ПМ у вас ровно первый вариант. Проверка на окончание итерирования аналогична проверке, Null ли список или Cons head tail. Функция суммирования же используется одна и никакого диспатча нет.
VE>Я же утверждаю, что когда ПМ разворачивается в "такой тормозной код", то и без ПМ будет он же.
с этим утверждением не поспоришь, если брать в общем виде.
я больше говорил в разрезе, что если брать ПМ как он реализован в том же Haskell-е, то он будет генерить тормозной код, не сильно лучше, чем какая-нибудь динамика аля питон.
в тоже время я согласен, что теоретически в ПМ информации содержится больше, и его проще конвертнуть во что-нибудь хорошее.
VE>>Я же утверждаю, что когда ПМ разворачивается в "такой тормозной код", то и без ПМ будет он же.
DG>с этим утверждением не поспоришь, если брать в общем виде.
Не понимаю только, как после этой фразы вы пишете сразу же ей противоречащую:
DG>я больше говорил в разрезе, что если брать ПМ как он реализован в том же Haskell-е, то он будет генерить тормозной код, не сильно лучше, чем какая-нибудь динамика аля питон.
Нет, он будет генерить код не тормознее любой другой статики. Разумеется, не в абсолютной величине, а относительно обсуждаемого вопроса. Т.е. если статика а-ля C# обходится 10 if'ами, ПМ тоже обойдётся ими (с учётом тех, что в АлгТД).
DG>в тоже время я согласен, что теоретически в ПМ информации содержится больше, и его проще конвертнуть во что-нибудь хорошее.
VE>Не уверен, что там это есть. Тогда соответственно назревает вопрос. Как вы предлагаете проверять то, что грязь убирается? VE>Можно на таком примере: isEven (rnd * 2)
для функций isEven и '*' можно восстановить условные pre/post-conditions
соответственно, на основе этих condition-ов для выражения isEven(rnd * 2) вообще вычисляется, что его post-condition: true
и что соответственно его можно заменить целиком на true при компиляции
VE>Ну или на ваш вкус
возьмем типичную ручную мемоизацию
class MyXY
{
public MyXY(object x)
{
this.x = x;
}
readonly object x;
public object Get()
{
if (_cache != null)
_cache = Zzz.My(x);
return _cache;
}
object _cache;
}
где Zzz.My — чистая функция возвращающая ненулевой результат
в этом коде Get.result = F(x, _cache, Zzz.My) и соответственно чистота(Get.result) = чистота(x) && чистота(_cache) && чистота(Zzz.My). x — чистая переменная, т.к. readonly, Zzz.My — чистая по определению, остался _cache.
_cache — может быть в двух состояниях: или null, или результат Zzz.My. Нулевое состояние _cache снаружи наблюдать(обнаружить) невозможно, т.к. для метода get: F(x, null, Zzz.My) == F(x, != null, Zzz.My), а других способов получить доступ к _cache нет.
Здравствуйте, VoidEx, Вы писали:
VE>Вы могли бы сказать, что в первом случае у нас используется само число, в во втором доступ к членам, но VE>1. Это далеко не всегда так, может, foo3 и foo4 этот указатель в списки добавляют VE>2. Разницы всё равно нет, так как foo1 и foo2 могут на основе значения бегать по таблицам, использовать числа как смещения и т.п. Грубо говоря вообще можно написать такой код, что foo1 и foo2 будут через таблицы эмулировать доступы в объектам.
Ну это ты далеко зашел в рассуждениях. Естественно, на любом тьюринг-полном языке можно написать некий интрепретатор другого тьюринг-полного языка с его системой типов, отличной от исходной. Этот случай обсуждать заведомо неинтересно.
V>>Я могу спросить в ответ привести пример, когда классы типов Хаскеля не являются костылем? VE>А они костыль.
А что не так без них?
Дело в том, что С++ static_if в большинстве случаев не нужен, он удобен лишь для диагностики, остальное система типов С++ разруливает и так. Т.е. всё, что может быть описано через static_if, может быть описано и без него или даже не описано совсем, а получится "по факту". Т.е. это не костыль, а сахар. А вот классы типов — натуральный костыль, без которого многие трюки в Хаскеле просто не взлетят. А костыль это потому, что изначально в языке отсутствовала концепция контрактов/интерфейсов. И вот ее заменяет этот недокостыль. Исключительно из-за скудной системы типов, где все пользовательские типы данных — это АлгТД.
Здравствуйте, VoidEx, Вы писали:
VE>Если смотреть с этой стороны, то с этим никто не спорит. Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили.
Определили. Это проверка/тестирование типа в рантайм.
Да и о чем спорить? По-определению АлгТД — это такой тип данных, в который упаковываются значения других типов. Вариант, он и в Африке вариант.
VE>Если смотреть в целом, то всё-таки нет, ибо паттерны могут быть вложенными, есть view-patterns, в Agda для функции, определённой через ПМ можно проводить доказательства (т.к. например для оператора сравнения будет существовать утверждение типа succ x == succ y = x == y), а через if-else будет значительно сложнее (т.к. приведённое выше утверждение уже отсутствует и им не попользуешься при доказательствах, его само сначала придётся доказать), и т.п.
Во-первых речь о Хаскеле, во вторых, Agda — это язык с зависимыми типами, у него типизация зависит от логических утверждений относительно значений в коде, в т.ч. от значений дискриминатора АлгТД. В любом случае, динамическая типизация никуда не девается. Просто ПМ по АлгТД — это такой встроенный трюк, что в конкретной ветке ПМ мы уже опять имеем статическую типизацию, но уже по фактическому выясненному содержимому АлгТД (а не по исходному, завернутому типу). Компилятор лишь гарантирует нам типобезопасность через отсутствие других способов реинтерпретировать память, занимаемую значениями АлгТД, кроме как через ПМ.
Здравствуйте, VoidEx, Вы писали:
VE>Любой if — это вызов блока в if или блока в else на основе таблицы из true/false.
В случае динамической типизации — не любой.
DG>>а почти весь ПМ (при условии, что есть несколько веток) в это и транслируется. VE>Любая программа содержит условные переходы, но динамической типизацией это называть было бы крайне странно. VE>Поэтому первостепенной задачей было бы как раз решить, что же такое динамическая типизация.
Это такое условное ветвление, целью которого является выбрать ветку алгоритма, умеющего работать с неким конкретным устройством значения (т.е. с неким конкретным типом).
Т.е. имеем следующее: в compile-time пишем алгоритмы под все возможные (или уникально обрабатываемые) типы, ожидаемые в некоей точке алгоритма, а в рантайм через ветвление выбираем одну из веток алгоритма, согласно фактически поданному типу значения.
Для работоспособности этой схемы обязательно нужен некий механизм реинтерпретации памяти. Например, в C# это приведение типов as или через (Type1), в С++ через dynamic_cast или через reinterpret_cast, еще через встроенный рантайм-полиморфизм, в ML-языках через паттерн-матчинг.
VE>То, что при наличии разных вариантов у АлгТД происходит ветвление — это динамическая типизация в той же мере, что и ветвление по 0 и не 0 в факториале.
Нет.
VE>Назвать это динамической типизацией можно только при большой фантазии, да и то, с натяжкой. VE>С другой стороны динамическую типизацию можно было представить как кортеж из имени типа и значения.
Так и представляют, например АлгТД в Хаскеле. Разве что область значения нетипизирована в представлении, т.е. это просто область байт неизвестного содержания. Неизвестного до тех пор, пока не будет проверена метка типа.
VE>Фундаментальную разницу я вижу в том, что при динамической типизации тип ровно один: dynamic.
V>>Я тебя спросил — покажи как это работает в рантайм? Ведь вызываемая затем ф-ия scalarProduct — рекурсивная, а глубина рекурсии заведомо неизвестна. Т.е. я понимаю твои предположения, если полностью раскрутить и переписать рекурсию, просчитав всё с конца списка. Давай тогда добавим побочный эффект в код scalarProduct, чтобы избежать этого. Думаю, добавление IO не должно сломать тайпчекер.
DG>в данном случае речь о том, что scalarProduct в runtime-е будет следующим с гарантией, что First никогда не выкинет исключение, и что закоментированный if не нужен: DG>
Я именно это и утверждаю, а оппонент не соглашается.
Только при большом кол-ве задействованных инстансов класса типов обычно применяют табличную диспетчеризацию, как более эффективную. Т.е. полный аналог виртуальных ф-ий, о чем я сразу и сказал. Но про диспетчеризацию на if, как возможную реализацию, тоже упомянул.
Знаешь какая ключевая фишка в обсуждаемом коде? Что Nil — это тип, независимый от Cons. Поэтому я и попросил кто может по-быстрому сгенерить сишный код компилятором, бо любопытно посмотреть диспетчеризацию по типам, не входящим в один АлгТД. Я ставлю на то, что компилятор унутре будет использовать ту же технику, что для обычных АлгТД, просто он объявит нужный алгТД сам, неявно.
Здравствуйте, vdimas, Вы писали:
VE>>Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили.
V>Определили. Это проверка/тестирование типа в рантайм.
Это фиговое и неправильное определение.
Типизация — это навешивание на каждое выражение в программе некоторого ярлыка-типа. Можем в компайл-тайме навесить достаточно конкретные типы на все — получили статическую типизацию. Не можем и вынуждены навешивать один неконкретный ярлык dynamic — получили динамическую.
V>Да и о чем спорить? По-определению АлгТД — это такой тип данных, в который упаковываются значения других типов. Вариант, он и в Африке вариант.
Это фиговое и неправильное определение, ведь "внутри" может оказаться он сам, не только "другие типы".
