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

V>При чем тут классы типов и паттерн-матчинг алгебраических типов?

Понятия не имею. Это вы вдруг про паттерн-матчинг АлгТД заговорили.

V>Классы типов — это лишь проверяемые в compile-time ограничения, то бишь контракты.

Не только.

V>Я обратил внимание на то, что сама реализация контракта была описана для разных значений дескриминатора АлгТД.

Что такое "разные значения дескриминатора АлгТД"? Разные конструкторы?

V>Я обратил внимание на то, что сама реализация контракта была описана для разных значений дескриминатора АлгТД.

Если "декскриминаторы" — конструкторы, то нет. Кмплементации класса нельзя писать для разных конструкторов. Только для типов. Так в этом примере и сделано.

V>Никогда в Хаскеле распаковка АлгТД не происходит во время компиляции.

Если под "распаковкой" подразумевается паттерн-матчинг, то да, не происходит. Но в данном случае это и не нужно. Вычисления то тайплевелные — матчатся типы Nil и Cons. Они, естественно, матчатся в компайл-тайме, потому что в рантайме их просто нет.

V>Это тип одного из возможных значений в группе, которая, в свою очередь, реализована техникой АлгТД.

Но у всех значений один и тот же тип — именно что АлгТД.

K>>Для АлгТД статически проверяется множество населяющих его значений — как и у любого другого типа.

V>Неверно, статически проверяется мн-во ТИПОВ населяющих его значений, но не сами значения

Откуда всялось множество типов? Проверяется принадлежность значения к множеству значений — типу.

V>Хаскель, в отличии от С++ НЕ умеет статически реагировать на сами значения (С++ умеет на целочисленные, в т.ч. на указатели).

Хаскель этого, понятное дело, не умеет. Зависимых типов в хаскеле нет. Точно так же и C++ не умеет. Статически "реагирует" он не нацелочисленные значения, а на целочисленные типы — типы кайнда Nat.

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

Алиас типа нельзя принять за имя конструктора (тег в размеченном объединении). Первое — тип. Второе — значение. Они в разных пространствах имен живут, работать с ними можно на разных стадиях — первые существуют только в компайл-тайме (это некоторое упрощение, при желании есть метаданные/рефлексия, но в данном случае они не используются), вторые только в рантайме. Отображать из типов в термы, правда, можно — для этого классы типов есть, но наоборот — нельзя.

V>Вид, сорт, тип — это синонимы в теории групп.

А в теории типов — нет. Вид (кайнд) — это тип типа, а сорт — тип кайнда.

K>>Каст преобразует тип значения. Матчинг АлгТД никаким преобразованием типов не занимается.
V>Опять неверно, dynamic_cast НЕ изменяет само значение

Я и не говорю, что меняет значение — меняет тип.

V>, переданное по ссылке (это обязательно, использовать dynamic_cast можно только через ссылку или указатель), оно тестирует тип поданного значения и преобразует тип ссылки, а не само значение, предоставляя доступ затем к мемберам типа по ссылке.

Аналог dynamic_cast в Хаскеле — Data.Dynamic. Там действительно есть проверка типа в рантайме.

V>Матчинг АлгТД в Хаскеле аналогично проверяет в рантайм дискриминатор объединения,

Ну разумеется.

V> то бишь запакованный тип

Вот только имя конструктора — тег в размеченном объединении — это не тип. Точно так же как 3 не тип и "hello" — не тип. Это значение.

V>, примерно точно так же, как dynamic_cast проверяет токен типа (на который ссылается экземпляр типа через указатель на vtable), а удачная ветка матчинга затем предоставляет доступ к значению упакованного в АлгТД типа.

Еще раз, типы в АлгТД не упаковываются. Вы путаете сабтайпинг и АлгТД. Они не родственники и даже не однофамильцы.

K>>Какая разница, боксированы значения или нет, если речь идет о типах?
V>Разница в том, что боксированный рекурсивный тип представляет из себя в памяти список (в простейшем случае, в непростейшем — дерево) из однородных узлов, а в небоксированном случае значение типа должно располагаться в памяти сплошным куском. Поэтому для первого случая достаточно одной реализации на каждый узел, а во втором потребуется столько различного кода, сколько типов было использовано во время компиляции. Поэтому в первом случае — в случае интерпретации структуры типа в рантайм, этот список/дерево может быть сколь угодно большой длины/глубины, то бишь мощность рекурсивного типа может быть сколь угодно большой.

Еще раз повторяю, если речь идет о типах. Типы в памяти ничего из себя не представляют (в рантайме). Их просто нет. А для значений да, все это верно (с оговорками). Вот только никакой интерпретации структуры типов в рантайме тут нет.

V>Справедливости ради, в простейшем случае можно обойтись и без боксинга для рекурсивных типов, т.е. для линейного списка в памяти, где рекурсивный тип идет как хвостовой, его можно расположить линейно и сгенерить лишь один однородный код на все типы разной мощности. Но для дерева или для случая нехвостового рекурсивного типа — уже никак. Почему никак? Предлагаю попробовать нарисовать карту памяти как будут располагаться поля.

V>То бишь боксированность нам гарантирует одинаковый размер полей, т.е. одинаковую карту размещения для любого инстанса такого типа. Возвращаясь к примеру: в итоге, код ф-ии scalarProduct будет одинаков для всех узлов рекурсивного типа Cons int a.

Ну правильно. Я тут так и писал. Код используется повторно ценой боксинга, такую цену за повторное использование сгенерированного кода C++ платить не может. Но мне справедливо напомнили, что я увлекаюсь деталями реализации. Ну а теперь вы увлекаетесь. Разница-то в системе типов. И в гипотетической реализации C++ где скомпилированный код повторно используется (это только для частных случаев можно будет сделать) и все забоксено — этот код или не будет работать все равно, или это будет не C++. Речь то о системе типов и семантике языка.

K>>Будут значения боксированными или нет — это вообще детали реализации, на статичность/динамичность системы типов не влияющие.

V>Угу, именно на это твое непонимание и обратил внимание. Статическая система типов хапрактерна не тлько статической проверкой контрактов. Упоминание эффективности статики как само собой разумеющееся (и даже ты тут отметился не раз в этой ветке, напоминая про статику) — это следствие того, что статически порожденный код ЗНАЕТ, как расположено в памяти значение оперируемого типа, и обращается к полям значения непосредственно, то бишь через фиксированные смещения в памяти, а не через дескрипторы/акцессоры.

Ну так он и в хаскеле знает смещения и расположения в памяти. Теги "типов" как в динамике он в рантайме не проверяет.

V>Мн-во допустимых типов значений АлгТД проверяется статически, конкретный тип из множества — динамически. Какие проблемы-то?

Ну так динамически проверяются значения, а не типы. точно так же, как и в C++. В чем динамическая типизация-то? Вот a == 3 — проверка динамическая, а типизация — сатическая, потому, что и код сравнения и структура для хранения 3 в памяти известна на этапе компиляции. Вы как-то систематически типы и значения путаете.

V>Наверно криво выразился. Имел ввиду, что в случае боксированной реалиации рекурсивных типов порожденному компилятором коду для его работоспособности достаточно знать об устройстве лишь части значения, а не всего значения целиком. Доступ к остальной части значения происходит рекурсивно через паттерн-матчинг, т.е. через рантайм-проверку, ну т.е. через динамику.

Для самой рекурсивной структуры данных — да. Точно так же, как и в C++.

V>Неверно. Дискриминатор АлгТД присутствует в рантайм будучи сохраненным по адресу значения, и этот дискриминатор проверяется исключительно в рантайм. Доступ к запакованному в АлгТД значению предоставляется затем исключительно через ПМ (фишка Хаскеля — у него других способов и нет), т.е. делает невозможным неверную интерпретацию памяти, в которой находится значение АлгТД. В этом и заключается типобезопасность, которая таки для случая Хаскеля динамическая, когда идет оперирование АлгТД.

Ну да, безопасность размеченных объединений по сравнению с неразмеченными достигается рантайм проверкой. Точно так же как и с доступом по индексу в массиве, например. Но какое это отношение имеет к типизации? В C++ аналогично и то и другое либо опасно, либо безовасно за счет рантайм проверки. Но тип у массива любой длины — одинаковый. И у любого конструктора АлгТД — одинаковый. Ну так при чем тут динамическая типизация-то?