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

V>Если своими словами, то так: статическая строгая типизация — это достоверная интерпретация памяти, занимаемой значениями типов, известная в compile-time. Динамическая строгая типизация — это типизация, которая требует телодвижений в рантайм, т.е. когда невозможно достоверно интерпретировать память, занимаемую этим значением, до проверки типа.

Очень размыто, но допустим.

1. Давай реализуем АлгТД как: индекс конструктора + массив указателей на данные. При доступе мы просто берём указатель с нужным индексом. Т.е.

struct ADT
{
  int i;
  ptr ctor[N];
};

ptr getADT(ADT & x) { return x.ctor[x.i]; }

У нас тут оверхед, потому что на деле нужен только один элемент из массива (остальные всё равно средствами самого Haskell не получить из-за свойств языка), но вот такова реализация. Зато память интерпретируется достоверно. Это я для простоты нарисовал массив, на деле-то можно сгенерировать структурку с типизированными указателями.

2. Давай реализуем АлгТД как: функция, принимающая кортеж обработчиков, и вызывающая ровно один из них при каждом case of.

// Either a b
typedef std::function<void (ptr)> onData;
typedef std::function<void (onData, onData)> either;

// foo e = case e of
//    Left x -> expr1
//    Right y -> expr2
void foo(either const & e)
{
  e([] (ptr x) { expr1 }, [] (ptr y) { expr2 });
}

Теперь АДТ — функция.

Что такое "интерпретация памяти"? Когда мы compile-time знаем, какого типа данные лежат в памяти? Ну вот знаем теперь, и что?

V>Далее. Должен существовать оператор динамической проверки и приведения типа, где на входе этого оператора будет неуточненный тип выражения, а на выходе — уточненный. Заметь, приведение к объемлющему типу происходит "бесплатно": для С++ в худшем случае константное смещение указателя/ссылки, если база не первая в списке, а для Хаскеля — это безусловное конструирование АлгТД. Зато переход от объемлющего типа к уточненному требует или dynamic_cast в С++, или динамическое приведение в яве/дотнете, или ПМ в Хаскеле/Немерле. Т.е. первая операция выполняется за O(1), то вторая за O(n), где n — общее кол-во тестируемых уточненных типов.

Т.е. ПМ в Haskell выполняется за O(n), да?

Давайте разбираться.

На вход мы даём выражение одного типа, на выходе (возможно) получаем другое выражение другого типа, так ещё и с другим адресом.
Под эти свойства подходит даже взятие элемента массива или доступ к полю объекта. Или разыменование указателя.
Я тут пытался описать свойства такой функции.
Так вот на мой взгляд эти свойства выглядит так:

-- каст туда-обратно гарантированно возвращает то же выражение
dynamicCast (cast x) = Just x
-- если каст успешен, то исходное выражение было получено кастом в обратную сторону
(dynamicCast e = Just v) -> (e = cast v)

Если будешь дополнять, то лучше псевдокодом, а не словами.

Но вот беда, для моего случая как динамика подходит указатель. int мы можем преобразовать в int*, а обратно — если указатель не равен 0.
Хуже того, int мы можем преобразовать в std::pair<bool, std::pair<int, float> >, а обратно — second.first или second.second в зависимости от флага. Перечисленным выше свойствам это удовлетворяет.
Я догадываюсь, какое свойство ты захочешь ввести, но попробуй его формализовать, и наверняка всплывут двойные трактовки. "Интуитивное" понимание меня волнует мало.

VE>>Статичность типизации — возможность гарантированно убрать ветвление.
VE>>Т.е. если в обоих языках по 2 ветвления при одинаковом поведении, то их статичность равномощна.

VE>>При моём определении две программы ниже статически типизированы в одинаковой мере. Однако третья — более статически типизирована:
VE>>И наплевать, что в Си++ просто ветвление, а в Haskell — ADT.
VE>>Предложи своё определение.

V>Дык, а чего предлагать? В Хаскеле ты требуемый признак вложил в систему типов программы (Maybe), а в С++ этот признак искуственный, проверяется вручную.

Правильно. Но какая разница, вручную или нет, это ведь останется динамической типизацией. То, что в Хаскеле закладывается в систему типов (Maybe, Either, any other ADT), в C++ придётся реализовать искусственно, а значит от "телодвижений в рантайм" никуда не деться. Примеры я приводил, приведу ещё раз:

// int * foo();
int * x = foo(10);
if (x)
  std::cout << *x << std::endl;
else
  std::cout << "null" << std::endl;

connection_data cdata;
if (load_config(&cdata))
{
  some_data sdata;
  int error_code = try_receive(&sdata);
  if (error_code == 0)
  {
    std::cout << "received " << sdata.bytes << " bytes" << std::endl;
    process(sdata.value);
  }
  else
  {
    std::cout << "error " << error_code << std::endl;
  }
}
else
  std::cout << "not loaded" << std::endl;

По моему определению — здесь в обоих случаях есть динамическая типизация в той же мере, что и в Haskell (в моём определении нет бинарного понятия, есть мера), но в меньшей, чем было бы на JavaScript, например.

V>На С++ можно так же вложить в систему типов, на статическом полиморфизме, если код разруливается на шаблонах или на динамическом, если не получается.

По поводу реинтерпретации памяти. Мне не нравится это интуитивное понятие, потому что на самом нижнем уровне типов уже нет. У нас указатели и вызовы функций, принимающие указатели. Тот же Either a b можно представить как просто флаг и указатель void*. А в зависимости от флага мы вызываем ту или иную функцию, которая принимает нетипизированный указатель. И вот в самом конце, когда наконец данные по указателю будут, например, выводить, произойдёт не реинтерпретация, а просто интепретация, при том ничего не стоящая. И получается, что динамичность типизации зависит от того, как будет проинтерпретирована память когда-то там намного позже. Причём принципиальной разницы между

if (flag)
  fooInt(ptr);
else
  fooFloat(ptr);

и

if (flag)
  fooInt1(ptr);
else
  fooInt2(ptr);

нет вообще.