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

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

S>>ПП от СП я отличаю по определению (одного, другого). Ни то ни другое определение (в википедии, по крайней мере) не используют термин "типизация".

K>Но они только способом типизации однородного кода и отличаются.
K>Отличаю по способу типизации однородного кода. Другого-то способа нет.

Способ подразумевает какой-то процесс. А я в TAPL не нашел упоминаний процесса типизации. Там есть отношение типизации (8.2), определяемое набором правил вывода, присваивающих термам типы.

K>То, что квантификация во всех примерах ограниченная я с самого начала говорил. Это ничего не меняет — кол-во "ограниченных" типов все равно бесконечно. Bounded-полиморфизм — это сочетание параметрического полиморфизма и сабтайпинга, т.е. наличие полноценного параметрического полиморфизма подразумевается. Никаких работающих примеров без ПП, например только subtype среди обсуждаемых нет.
Как интересно, рассматривать наличие ПП на примере, где он лишь подразумевается...

S>>Я же не утверждаю что он не существует. Я утвреждаю что существование такого типа не связано с определением. Тем более, не очевидно существование такого типа в конкретной программе.

K>Ну так тип объявлен в конкретной программе.
В моей конкретной программе его нет. Софистика?

S>>Обращу внимание, что в TAPL нет упоминания о типе, содержащем переменные.

K>Ну разумеется есть. Он процентов на 80 состоит из упоминаний "типа, содержащем переменные"
Увы, это не так. Может быть "термы, содержащие типовые переменные"?

S>>Мой основной довод — это то, что бесконечность типов не требуется. Попытку представить бесконечность типов в бесконечности программ предлагаю игнорировать.

K>Отлично.

S>>Точно так же как и существование типа forall a. Succ a.

K>Т.е. в вашем определении ПП типизировать полиморфный код нельзя?
Я все еще не понимаю, что значит "типизировать". (8.2.1) вводит понятия t is typable (or well typed). Используется это в контексте переменных типа следующим образом (22.2)

1. "Are all substitution instances of t well typed?"
2. "Is some substitution instance of t well typed?"

K>>>Вы же прямо из TAPL сюда куски текста копируете, значит доступ к тексту у вас есть. А там все разжевано.
S>>А там об этом ничего нет.

K>Ну, это неправда.
Можно ссылку (хотя бы номер параграфа), где бы упоминались "типы, содержащие переменные"...

S>>Там говорится об использовании переменных вместо actual types, а вовсе не о типах, содержащих переменные.

K>Да ну, в главе о "типах, содержащих переменные" не говорится о "типах, содержащих переменные"?
... и номер главы о "типах, содержащих переменные"

S>>Не согласен. Там написано что кусок кода типизируется "обобщенно", используя переменные вместо типов. И ничего о параметрических типах, кстати.

K>А что такое параметрические типы, по-вашему? Ну, скажу тогда, что шаблонный код "обобщенно, используя переменные вместо(?) типов". "Вместо типов" — вообще анекдот. не вместо типов вообще, а вместо конкретных типов. Переменная типа — это тип. Посмотрите, где семантика расписана переменные типа справа от ( — операции типизации.
Параметрические типы в TAPL упомянуты лишь в главе 29 (Type Operators and Kinding), сильно после ПП. Так что я думаю что это оффтоп.

K>Какой смысл рассуждать о том, сколько ангелов поместится на выдернутом из контекста абзаце, когда в его непосредственной окресности совершщенноь ясно описывается, с примерами и что такое тип и что такое типизировать и вообще все остальное, что вы сейчас выводите из каких-то странных предположений о переносе смысла при переводе.
Можно координату абзаца, в котором описано что такое типизировать?

S>>Тогда мы в с++ и C# имеем forall, который непонятно чем отличается от forall H98

K>Нету в C++ квантора всеобности, о чем и разговор.
А в C# его тоже нет

S>>Я влез в эту тему что бы выяснить вашу позицию по поводу разграничения C++ и C# на тему присутствия в них ПП. Вы глядя на примеры migmit-а утверждаете что в С# ПП есть, а в С++ — нет. Вот мне и захотелось уточнить, почему вы так считаете.

K>Потому, что код, написанный, исходя из предположения, что полиморфизм в C# параметрический работает так же, как и в других языках с параметрическим полиморфизмом и в соотвествии с теорией, построеной на свойствах параметрического полиморфизма. С другой стороны, код, написанный, исходя из предположения, что полиморфизм в C++ параметрический не работает так же, как и в других языках с параметрическим полиморфизмом и не соотвествует теории, построеной на свойствах параметрического полиморфизма.
Можно показать мне место в теории, построенной на свойствах ПП? Где в TAPL (или еще где-то) сказано что такое в ПП должно работать, иначе это не ПП.

K>Т.е. в каком-то гипотетическом рантайме гипотетического языка (который C# не является потому, что у него другая система типов и семантика) может не быть параметрического полиморфизма. Какой из этого следует вывод?
Вывод тут следует такой: что пример на C# от примера на C++ отличается лишь тем, что его рантайм (не всякий, причем) позволяет применять/конкретизировать/инстанциировать типы в рантайме. А такое отличие не считается ключевым в контексте ПП, иначе, наверное, оно было бы где-то упомянуто. А значит, либо в C# ПП отсутствует, либо в C++ присутствует.

S>>Согласен, в общем случае не нужна и для C# не нужна тоже. Поддержка рантайма нужна для работы примера migmit-а, связь которого с определением ПП туманна. Там ПП присутствует в форме bounded полиморфизма с замесом на subtype полиморфизм.

K>Ну а на Хаскеле пример работает без поддержки рантайма. Ну так что, нужна поддержка рантайма для этого или нет?
C#-у нужна.

K>Ну, если определять ПП как "что-то, что есть в C++" тогда да.
А если определять ПП как "что-то, чего нет в C++"?

K>Применение типов в рантайме в C# отличается от применения в компайл-тайме синтаксически:
K>

K>typeof(Foo<>).MakeGenericType(new[]{typeof(Bar)})
K>Foo<Bar>
K>

K>Перепутать их никак невозможно.
Ой ли? А вот представьте, что в Foo используется List<T>. Будет ли Bar подставлен в List<> в компайл-тайме, если Bar в Foo<> подставили в рантайме? По-моему ваш способ отличия не дает однозначного ответа

K>Кроме того, если бы типы применялись в рантайме — тайпчекер не смог бы проверить их.
Что там проверять-то? конкретный тип на констрейнты? Нечего делать. Это же не вывод типов!
Проверяет, не вопрос: http://msdn.microsoft.com/en-us/library/system.type.makegenerictype.aspx
обратите внимание на раздел исключений.

K>"Код генерируется в рантайме" — это не то же самое, что и "Типы применяются в рантайме".
Да, вещи разные, но применяются типы в обсуждаемом примере именно в рантайме. И код генерится тоже.

S>>А, без проблем. Только к какому выводу это приведет? В C++ тоже ведь будет ошибка компиляции.

K>На C++ не написать код, который правильно работает.
Не написать код, который правильно работает, используя рантайм сабтайп полиморфизм (virtual же), подразумевающий ПП и неограниченное кол-во типов. Это верно. Только причем здесь ПП?
Покажите мне пример, где в C++ не работает ПП в чистом виде без всяких виртуальностей, сабтайпингов и требований к применению типов во времени выполнения.

S>>Суть возражения была в том, что обсуждаемая фича в C# работает за счет рантайм конкретизации и кодогенерации. Без этих фич C# в отношении обсуждаемых примеров будет столь же бесполезен, как и C++.

K>Именно в C# фича работает, потому что он компилируется в байткод с ПП. Что и где там потом генерируется из совсем другого языка к делу отношения не имеет.
Я вообще пока не увидел, какое отношение эта фича имеет к присутствию/отсутствию ПП.

K>>>Я сказал. В определении параметрического полиморфизма так написано. Поэтому он и "параметрический" и отличается от других видов полиморфизма.
S>>Нет, в определении такого не написано. Ни в википедии, ни в TAPL.

K>В TAPL совершенно точно написано. Определение в википедии не читал.
А TAPL?
"parametric type" упоминается в целой книге целых два раза (один раз в главе 29, другой — в индексе). Так что, я смотрю в книгу на опеределение ПП и совершенно точно (ц) вижу что там нет упоминания parametric type.

S>>"Параметрический" он потому, что параметризуется код (single piece of code), а не тип.

K>Чем код-то параметризуется?
переменной

S>>Нет, другие виды полиморфизма отличаются своими определениями. Ключевые отличия:
S>>subtyping — тут есть 2 определения. а) работает для всех подтипов автоматически;

K>Ну я и говорю. Типизацией.


K>Вот вам две length без сигнатур типа:
K>

K>length [] = 0
K>length (_:xs) = 1 + length xs

K>length [] = 0
K>length (_:xs) = 1 + length xs
K>

K>Где здесь параметрический полиморфизм, а где полиморфизм через сабтайпинг?
1) не смог найти отличий в двух функциях
2) не обнаружил подтипы
3) полагаю что в обоих случаях параметрический

S>>как это?
S>>

S>>#define ID x = (x)
S>>template <class T> T id(const T& v) { return v; }
S>>

S>>Разве такие определения не позволяют использовать их однородно для различных типов?

K>Сравнивать разновидности полиморфизма — свойства системы типов — без обсуждения типизации я вообще считаю бессмысленным.
Это не мешает вам рассуждать об присутствии разновидности полиморфизма. И я так и не понял, какой вы вкладываете смысл в слово "типизация". Ниужели type checking? Вот, нашел вашу фразу (вырвал из контекста)

ПП — это статическая типизация.

По поводу нее я тоже категорически не согласен.

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

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

S>>Если может превращается, а может и не превращается, то о каком ПП речь? ПП должен работать одинаково для всех типов. И если там для какого-то типа заложены знания что нечто ужасное превратится в MyStruct, а для другого не превратится, то это уже не ПП.

VE>

VE>template <class C>
VE>void foo(C const & x)
VE>{
VE>  x.Foo(); // << %(
VE>}
VE>

VE>Это ПП?
Уже только x.Foo(); говорит что это не ПП.

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

S>Уже только x.Foo(); говорит что это не ПП.

Не совсем. То, что это не ПП, говорит хотя бы template <class T>
Ибо ну кто мешает сделать template <> ...?

Но даже несмотря на это хотелось бы посмотреть на какой-нибудь пример с так называемым "ПП" кроме T & id(T & arg) { return arg; }.

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

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

S>>Уже только x.Foo(); говорит что это не ПП.

VE>Не совсем. То, что это не ПП, говорит хотя бы template <class T>
VE>Ибо ну кто мешает сделать template <> ...?
Никто не мешает. Но пока известно что это не сделано в неком множестве исходников конкретной программы, имеем право рассматривать другие причины сомневаться в присутствии ПП в неком куске кода, например, ad-hoc полиморфные выражения, вызовы перегруженных функций...

VE>Но даже несмотря на это хотелось бы посмотреть на какой-нибудь пример с так называемым "ПП" кроме T & id(T & arg) { return arg; }.
их можно привести потенциально бесконечное число:

template<class T, class X>
T & Const(T & arg, X&) { return arg; }

А вот с реально полезными примерами чистого ПП не так весело. Впрочем, если ограничиться в рассмотрении некоторыми хорошими типами (с копированием, присваиваниями и т.п.), то множество полезных примеров резко расширяется, но это уже будет bounded полиморфизм.

ME>скажем, можно вспомнить мемоизацию результата чистой функции -- она мутирует данные, но тем не менее не мешает чистоте; с другой стороны, если компилятор не сможет отловить ошибку программиста в *этом* сценарии (когда, скажем, по ошибке из кэша выдается мемоизированный результат не для данной функции, а для другой) -- то это неполноценность языка

Верифируемое множество кода всегда отстает от множества кода, которое выдает правильный результат.
Соответственно, возникает вопрос: можно ли разрешать программисту писать код, которые не полностью верифицируем компилятором, но программист мамой клянется, что он выдает правильный результат?

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

V>Мое определение чистоты сильно короче. Чистая ф-ия возвращает один и тот же результат на одних и тех же аргументах.

Не очень хорошее определение (оно неустойчивое: с одной стороны — одно считает чистым, с другой стороны — тоже самое считает не чистым).
Это определение лучше(более обобщенная форма), чем следующий вариант:

> Evaluation of the result does not cause any semantically observable side effect or output, such as mutation of mutable objects or output to I/O devices

это тоже неустойчивое определение.

По этим определениям получается, что, например, sin x становится грязной функцией, как только в язык добавляется возможность измерять температуру процессора (или считывать счетчик выполненных процессором команд)

Чтобы определение чистоты было устойчивым — необходимо еще фиксировать множество операций для которого определяется чистота функции.

sin x чистая функция относительно множества математических операций, и нечистая относительно операций читающих состояние процессора или "состояние времени" (sin x при одном и том же x — может выполняться разное кол-во времени)

Функция, мемоизирующая свой результат при первом вызове является чистой функцией с точки зрения почти всех операций, и не является чистой функцией с точки зрения следующих операций: проверка результат функции уже вычислен или еще нет, сколько памяти отъела программа

Сложный пример для понимания: функция random — нечистая функция с точки зрения операций чтения счетчика random-а и операций завязанных на конкретное значение результата random-а, но random — чистая функция с точки зрения всех остальных операций. В частности, это проявляется в следующей композиции: is-number(random()), которая является чистой функцией уже с точки зрения почти всех операций.

K>Под параметрическим полиморфизмом я понимаю общепринятое определение. Т.е:
K>1) Воможность написать однородный (работающий одинаково для любого типа) код
K>2) Типизировать этот код обобщенным типом, содержащим переменные, которые конкретизируются применением обобщенного типа к конкретному (или другому обобщенному, если ПП первоклассный, т.е. импредикативный)

следующие функции по этому определению полиморные или нет? и почему?

bool IsInt32Enumerable<T>(IEnumerable<T> items)
{
  if (typeof(T) == typeof(int))
    return true;
  return false;
}
int Count<T>(this IEnumerable<T> items)
{
  var collection = items as ICollection<T>;
  if (collection != null)
    return collection.Count;
  return items.Aggregate(0, (a, _) => a + 1);
}

основной вопрос: можно ли строго определить, что такое "работающий одинаково для любого типа"?

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

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

VE>Скажите пожалуйста, а switch-case для enum в Си++ — это тоже динамическая типизация?

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


V>>Ты мне покажи вот так:
V>>main' :: Integer -> Integer -> a -> b -> Integer
V>>Потом подай на a и b одинаковые типы извне. Вот это и будет настоящий ПП, а не тот, которым вы хотите незаслуженно обозвать систему типов Хаскеля.

VE>Не понял. Что должна делать такая функция? Ругаться при компиляции на разные типы? Или молча жрать все? Тогда в чём замысел?

Например том, чтобы она смогла быть применена в таком контексте, где a и b могут выводиться как одни и те же типы, а могут и нет. Речь идет о возможностях техники навроде static_if в С++. Возможностей Хаскеля для сравнимой реализации такой техники недостаточно, т.к. нет аппарата compile-time вычислений.

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

DG>на практике удобнее и эффективнее второе, и этим хаскель не удобен. например, чистый внешний вызов без танцев с бубном нельзя обернуть в чистую haskell-функцию.

Какие танцы? unsafePerformIO и есть "мамой клянус".

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

DG>Сложный пример для понимания: функция random — нечистая функция с точки зрения операций чтения счетчика random-а и операций завязанных на конкретное значение результата random-а, но random — чистая функция с точки зрения всех остальных операций. В частности, это проявляется в следующей композиции: is-number(random()), которая является чистой функцией уже с точки зрения почти всех операций.

is-number = const true?

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

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

VE>>Скажите пожалуйста, а switch-case для enum в Си++ — это тоже динамическая типизация?

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

Тогда if-else тоже динамическая типизация.

VE>>Не понял. Что должна делать такая функция? Ругаться при компиляции на разные типы? Или молча жрать все? Тогда в чём замысел?

V>Например том, чтобы она смогла быть применена в таком контексте, где a и b могут выводиться как одни и те же типы, а могут и нет.

Зачем?
Тем более, что это не ПП, а речь-таки о нём шла.

V>Речь идет о возможностях техники навроде static_if в С++. Возможностей Хаскеля для сравнимой реализации такой техники недостаточно, т.к. нет аппарата compile-time вычислений.

Во-первых, как это нету?
Во-вторых, можно пример, когда static_if не является сам по себе костылём?

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

V>>В каких разных? Продемонстрируй плиз разные пространства имен для конструктора АлгТД и для одноименного идентификатора метки типа в конструкции ПМ некоего значения, созданного с помощью этого конструктора.
K>Я говорил про имя типа и имя конструктора.

Я задал вполне конкретный уточняющий вопрос в ответ на твое отрицание. Т.е. ты или соглашаешься или приводишь своё отрицание целиком.


V>>Эээ... колега, а что вообще могло бы означать "упаковка другого типа" для АлгТД?
K>Вот и мне интересно. Это ведь вы утверждаете, что конструкторы АлгТД — типы.

Чего-чего?

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

K>Дескриминатор-то он, разумеется, проверяет в рантайме. А тип "запакованного" значения — нет. О чем и весь этот разговор.

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


K>>>Ну, может и можно сказать, что конструктор типа "упаковывает" типа по аналогии с тем, как конструктор "упаковывает" значение. Вот только конструкторы типов в рантайме не матчатся (в рантайме их нет).
V>>А как конструкторы могут матчиться?
K>Ну вот, приехали. А что, что-то может матчиться кроме конструкторов?

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


V>>Ведь конструктор — это ф-ия.
K>Совсем не обязательно. В ocaml, например, конструктор функцией не является.

А чем является конструктор алгТД в Caml?


K>Но даже если всякий конструктор — функция, то все равно не всякая функция — конструктор.

А это при чем? Интересует только первая часть фразы.


V>>Может матчиться лишь некое ID размеченного объединения, то бишь матч всегда идет по ЗНАЧЕНИЮ
K>Правильно. Имя конструктора и есть этот ID.

Т.е. ты таки решил согласиться, что имя функции-конструктора используется в кач-ве метки типа в одном из контекстов (в ПМ)? Бо этот ID — это по-определению рантайм-метка типа, завернутого в АлгТД.


V>>в данном случае это значение метки типа. Т.е. можно сказать, что идет матч по типу завернутого значения.
K>Это значение к метке типа не имеет никакого отношения. Т.е. так сказать нельзя.

Я не услышал объяснения наличия какой-то другой метки типа, к которой эта не имеет отношения. Есть только эта и никакой больше.

K>

K>-- так можно
K>data FooBar = Foo Int | Bar Int
K>-- так нельзя
K>data Foo = Foo Int | Foo Bool 
K>

K>т.е. в рантайме проверяются не типы. ч.т.д.

При чем тут рантайм, если у тебя ошибка компиляции во втором случае? Не хочешь привести сообщение об ошибке компиляции?


V>>Угу, ты повторно налегаешь на подтипирование, хотя я его не упоминал.
K>Постоянно упоминаете, когда говорите о проверке метки типа в рантайме.

Да, но только техника подтипирования здесь не при чем. Подтипирование вроде бы предполагает совместимость типов, а определение АлгТД этого не требует, хоть и не запрещает в некоей реализации.

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


V>>Я догадываюсь, что ты намекаешь на реализацию наподобие АлгТД в Немерле, но я-то здесь при чем?
K>Не намекаю. Я объясняю, что является типом в хаскеле, а что не является.

Речь была о метке типа АлгТД, а не о том, что является типом, а что нет. Например, сигнатура ф-ии — является вполне конкретным типом в дотнете, и этот тип проверяется в compile-time при создании делегатов, но для этого типа не существует дескриптора типа, в отличие от подтипов Object. Т.е. не все типы должны обязательно должны иметь метки в рантайм. В С++ тоже, dynamic_cast работает не для всех типов, а только для некоторого класса пользовательских, имеющих виртуальные ф-ии.

K>Тип — это не всякое множество, а множество, пренадлежность к которому может проверить тайпчекер. Статически.

Ну так техника АлгТД нужна как раз чтобы обойти такое ограничение, т.е. чтобы сложить несколько типов в один "мешок", и протащить мимо таких проверок. Помню твою цепетильность — протаскивается значение, разумеется. В этом случае проверяется лишь то, чтобы в этот мешок не попало значение постороннего типа, а только из объявленного в ограничениях варианта. Затем этот мешок надо раскрыть в рантайм и применить такую проверку уже к содержимому де-факто, что и делается в конструкции ПМ. Естествено, что для работоспособности всей схемы необходимо закодировать признак типа вместе с данными. В схеме АлгТД этот признак существует явно, согласно определению АлгТД.


V>>data List a = Nil | Cons a (List a)
V>>Для значения дескриминатора Nil_tag хранится tuple(/*empty*/), для значения Cons_tag хранится tuple(a, List<a>). Оба тупла и есть хранимые значения. Но сии значения-туплы имеют тип, как ни крути.
K>Туплы имеют тип. Но этот тип не находится с алгтд в отношениях подтипирования.

Я уже не первый раз спрашиваю. Можешь, интереса ради, целиком раскрыть свою мысль насчет подтипирования? Я действительно не понимаю, при чем тут АлгТД и подтипирование (ну кроме как в плане одной из возможных техник реализации).

Я когда-то натыкался на мозгоправство, что мол конструкторы АлгТД — это конструкторы данных, а не конструкторы типов. Большей ереси я еще не слышал. Результатом, возвращаемым этим конструктором, будет именно значение целевого типа АлгТД, а не какого-то еще особенного типа данных.


V>>И да, от техники подтипирования в том же Немерле такая схема по-сути не отличается. Хоть ты и додумал за меня малость, насчет подтипирования, но происходящие в обоих случаях проверки типов при паттерн-матчинге — это суть проверки значения некоей метки. Вся разница лишь в том, что в Хаскеле метка представлена "унутре" интегральным значением, а в Немерле — адресом (сылкой) на дескриптор типа. По идее, тоже интегральным значением (адреса).

K>В хаскеле (ghc) эта "метка" как раз и представлена ссылкой на дескриптор блока памяти и (в случае небольшого числа конструкторов) тегом в указателе на блок.

Необязательно. Некоторые типы данных он "знает в лицо" и метка типа представлена интегральным значением, скажем так, заведомо ограниченного мн-ва, т.е. мн-ва ограниченной разрядности. Речь о char или int. Более того, если АлгТД имеет всего один конструктор, то метки может не быть вообще, т.к. "кот в мешке" заведомо один. Эту технику можно использовать для объявления уникального типа тулпа для прикладных целей, т.к. обычный алиас тупла не вводит уникальный тип, т.е. бесполезен для использования тайпчекера для прикладных целей.



K>>>Ну так boost::variant это не сумма, а объединение — чего вы от него хотите. variant< int, bool > это int или bool.
V>>Не так, это еще хранимый признак типа, как и положено. Поэтому это или container<0, int> или container<1, bool>. Т.е. в плане хранения — дотягивают. Они недотягивают в момент диспетчеризации по конкретным хранимым типам, бо для одного и того же типа будет вызвана одна и та же ветка диспетчеризации
K>Вот вы и описываете разницу между сабтайпингом (boost::variant) и алгебраическим типом. Еще одно различие. Через параметр типа variant< int, bool > можно передать и int и bool. Потому, что любые значения этих типов являются также и значениями вариантного типа. Это и называется "отношение подтипирования". Между типами "упакованными" в сумму и суммой такого отношения нет. Через параметр типа Either Int Bool нельзя передать ни значение типа Int, ни значение типа Bool. Только Either Int Bool.


Ээээ... похоже, ты не понимаешь, что есть подтипирование. Ты не можешь передать int туда, где ожидается variant<int, bool>. Ты можешь подать только variant<int, bool>. Это в Немерле возможен такой трюк, правда ни Boolean ни Int32, ни какой другой имеющийся тип использовать в такой сумме не выйдет. Нужно будет объявлять пользовательские типы прямо в варианте, которые подтипы некоего MyVariant. Причем, обязательно ссылочные.


V>>Тем более, что обсуждаемый пример можно переписать на АлгТД и обойтись без классов типов.
K>Нельзя. Потому, что нам нужны тайплевел вычисления, а не рантайм-проверка.

Можно, добавив фиктивные тайлевел вычисления, не участвующие в рантайм-вычислениях. Я имел ввиду организацию рекурсивного типа. Сейчас эта рекурсия выполнена на полиморфном аргументе, а можно было сделать явно на алгТД.


V>>Для тега алгТД место в рантайме таки требуется.
K>Никакие "Теги" АлгТД в рантайме не хранятся. Есть ссылка на InfoTable. У каждого вида лайаута данных в памяти — своя таблица.

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


V>>Или ты считаешь, что процедура сравнения тега размеченного объединения и распаковка затем хранимого значения чем-то отличается от динамической типизации? Это абсолютно такое же кол-во телодвижений за ту же стоимость.
K>То, является что-то типизацией или не является не определяется стоимостью. Типизация — это проверка типа. Если мы проверяем значения на совпадение с BoxInt, true или 0 — это не проверка типа потому, что все это не типы. Не всякая проверка — проверка типа.

Разве вот это не проверка типа:
if(typeof(T) == typeof(int)) {...}

Это ровно тоже самое, что происходит в ПМ, с поправкой на ветер, т.е. на механику Хаскеля. И даже больше — я привел проверку, которая могла быть вполне статической.


V>>Именно. А приводимый пример фактически надуманный, т.к. что там проверять-то?, коль списки формируются параллельно.
K>Ну так то, что списки формируются параллельно и проверяется.



K>Ну так смысл проверки типов в том, чтоб проверять соответствие функции типу, которым ее проаннотировали. Если функция не будет строить списки параллельно — будет ошибка компиляции.

Не спорю, но при чем тут полноценный ПП?


V>>Угу, как возражение, что при вызове ф-ий используется неявное ПМ привел явную реализацию на ПМ. Поздравляю.
K>Привел реализацию в которой явно видно, что есть проверка счетчика для прерывания рекурсии, а никакого "выбора функции из группы" нет.

Выбор есть. Просто ты не понимаешь термина "выбор функции из группы". Одноименные ф-ии в одной области видимости составляют группу ф-ий. В С++ выбор происходит статически для обычных ф-ий или динамически для виртуальных. В Хаскеле почти любая ф-ия может быть выбрана статически или динамически, через неявный ПМ. Как этот ПМ происходит — ты примерно и показал. С чем спорил тогда?


K>Да, смешно читать, что человек может нафантазировать про тайпклассы, не зная, как они работают.
V>>Каким образом? Чтобы выбор сделать, надо отказаться от боксированного представления, т.е. заранее знать, где конец списка.
K>Не нужно знать, где конец списка. Мы начинаем построение с Nil — это статически известно. выбираем одну функцию и подставляем ее вместо функции тайпкласса. Во всех остальных случаях будет функция для Cons — одна и та же — подставлем ее. Все, вся диспетчерезация закончилась на этапе компиляции.

И куда мы "подставляем" ф-ию в данные? Ф-ия в данные подставляется через адрес, что и называется диспетчеризация. Или же через аналог неявно вставленного if — и это тоже есть диспетчеризация. Техника исполнения не принципиальна.

Я тебя спросил — покажи как это работает в рантайм? Ведь вызываемая затем ф-ия scalarProduct — рекурсивная, а глубина рекурсии заведомо неизвестна. Т.е. я понимаю твои предположения, если полностью раскрутить и переписать рекурсию, просчитав всё с конца списка. Давай тогда добавим побочный эффект в код scalarProduct, чтобы избежать этого. Думаю, добавление IO не должно сломать тайпчекер.

Более того, сами списки могли быть попеременно составлены из разных "сегментов", например из float и т.д., и для каждого сегмента мог быть определена своя рекурсивная реализация scalarProduct. Как будет работать в этом случае? Твои предположения? Или если есть возможность — сгенери хасклеем сишный код (вроде так умеет), посмотрим на происходящее.


K>Ну так в этом проверка типа и заключается. Если в функции не будет "черным по белому сказано", что списки одинаковой длины — будет ошибка компиляции.

Для формируемых параллельно списков, это, прямо скажем, небольшая прикладная ценность. А как только не параллельно — так сразу перестает работать.


V>>Ты мне покажи вот так:
V>>main' :: Integer -> Integer -> a -> b -> Integer

K>Тут написано, что типы могут быть одинаковыми, а могут и раными — все равно. Что это проверяет-то?

Не надо проверять main', не он ведь целевой. Пусть проверяется scalarProduct. Т.е. пусть тело main' скомпиллируется только если в compile-time подать на a и b одинаковые типы.


V>>Ну коль Cons a параметризируется типом Cons a', то у нас выходит, скажем, де-факто параметрический рекурсивный тип в примере.

K>Отличная шутка! А любая функция, у которой область определения — подмножество области значений — "де-факто рекурсивная"? А то ведь ее можно так применить f(f(х))

Такое применение — это и есть де-факто рекурсия. В примере акцент не на том, что тип бъявлен как рекурсивный, а что рекурсия вышла де-факто, потому что N заведомо неизвестен. Вроде мы уже пару раундов назад согласились с тем, что раз N заведомо неизвестен, то карта данных в памяти может быть только рекурсивной и никак иначе.

Ну и опять же, на С++ пытались реализовать именно на технике такой де-факто рекурсии, а не на честном рекурсивном типе. Т.е. попытка была нерелевантна с твоей т.з.? Смысл было тогда обсуждать С++ реализацию?


K>>>Дескриминаторов типа в Хаскеле просто не существует
V>>True, False, Cons, Nil — вот тебе существующие в рантайм дискриминаторы, хранимые вместе с данными.
K>Это и есть данные. Не типы.

Это метки типов АлгТД, как бы это не разрывало твой шаблон.


V>>Это конструкторы АлгТД в одном контексте и теги АлгТД, то бишь теги хранимого типа — в другом, например в конструкции ПМ.
K>Еще раз. Медленно. Теги конструктора и теги типа — разные вещи.

В смысле, по разному устроены в конкретном компиляторе? Не важно ни разу.


K>И в конструкции ПМ никакие типы не проверяются. Тип там один — тип матчимого АлгТД. Проверяется статически.

Ну да, тип "мешка" проверяется статически, что сказать-то хотел? А тип содержимого — динамически, увы.


V>>А что, тебя смущает вырожденный случай размеченного объединения навроде Bool?
K>Ничем не смущает. Меня смущает, что вы True и False считаете типами.

Это метки типов. Типов пустых туплов. Я вижу, что таки минималистичность синтаксиса Хаскеля, т.е. вызов ф-ий без аргументов и даже без пустых скобок, тебя смущает. Например, что есть True? Это никакое не значение вне контекста ПМ, это вызов одного из конструкторов типа Bool. Осталось помедитировать над тем, что есть вызов конструктора типа.

DG>>Сложный пример для понимания: функция random — нечистая функция с точки зрения операций чтения счетчика random-а и операций завязанных на конкретное значение результата random-а, но random — чистая функция с точки зрения всех остальных операций. В частности, это проявляется в следующей композиции: is-number(random()), которая является чистой функцией уже с точки зрения почти всех операций.

VE>is-number = const true?

например, такая:

bool is-number(object value)
{
  return value is int || value is double;
}

или такая

bool is-number<T>(T value)
{
  return typeof(T) == typeof(int) || typeof(T) == typeof(double);
}

DG>>на практике удобнее и эффективнее второе, и этим хаскель не удобен. например, чистый внешний вызов без танцев с бубном нельзя обернуть в чистую haskell-функцию.

VE>Какие танцы? unsafePerformIO и есть "мамой клянус".

танцы в том, что компилятор проверяет или каждый чих на чистоту (без unsafePerformIO), или вообще чистоту не проверяет (с unsafePerformIO).

хотелось бы чтобы можно было зафиксировать — относительно каких операций чистота гарантируется и должна проверяться компилятором.

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


DG>>>Сложный пример для понимания: функция random — нечистая функция с точки зрения операций чтения счетчика random-а и операций завязанных на конкретное значение результата random-а, но random — чистая функция с точки зрения всех остальных операций. В частности, это проявляется в следующей композиции: is-number(random()), которая является чистой функцией уже с точки зрения почти всех операций.

Если я правильно понял мысль, композиция is-number(random()) остаётся грязной с т.з. операции чтения счётчика random, но становится чистой для функций, использующих значение всей этой композиции.

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

DG>танцы в том, что компилятор проверяет или каждый чих на чистоту (без unsafePerformIO), или вообще чистоту не проверяет (с unsafePerformIO).

Ну есть ещё ST, например.

DG>хотелось бы чтобы можно было зафиксировать — относительно каких операций чистота гарантируется и должна проверяться компилятором.

Можно пример в псевдокоде? Как предполагается это указывать?

Вот, например, Disciple, диалект Хаскеля с системой эффектов.

VE>композиция is-number(random()) остаётся грязной с т.з. операции чтения счётчика random, но становится чистой для функций, использующих значение всей этой композиции.

да

ps
более точно:

var rnd = new Random();
is-number(rnd.Next()); //грязная относительно счетчика rnd

is-number(new Random().Next()); //чистая относительно всех операций (кроме каких-то специфических связанных с состоянием исполнителя)

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

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


VE>>композиция is-number(random()) остаётся грязной с т.з. операции чтения счётчика random, но становится чистой для функций, использующих значение всей этой композиции.

DG>да

DG>ps
DG>более точно:
DG>

DG>var rnd = new Random();
DG>is-number(rnd.Next()); //грязная относительно счетчика rnd

DG>is-number(new Random().Next()); //чистая относительно всех операций (кроме каких-то специфических связанных с состоянием исполнителя)
DG>

DG>ззы
DG>вообще смысл в том, что как только переходим от черно-белого мышления(чистая/грязная) к полутоновому(чистая относительно определенного множества операций), то можно формализованно утверждать, что при композии грязь не только постоянно растёт, но и может пропадать при определенных замыканиях (или других инкапсуляциях)

Ну так в этом смысле у Haskell не только либо чистота, либо нет чистоты.
Вышеозначенный пример можно и в Haskell переписать.
В одном случае будет ST-ссылка на внешний счётчик, во втором — монада State.
Другое дело, что текущими средствами в Haskell не доказать (нет зависимых типов), что при любом значении состояния во втором случае (State) результат будет один и тот же.

С другой стороны, если например определить isNumber так, то можно пользоваться "мамой клянус"

class IsNumber a where
  isNumber :: a -> Bool

instance IsNumber Int where
  isNumber _ = True

needNoState :: (RandomGen g, Random a) => State g a -> a
needNoState _ = undefined

isNumber (needNoState rnd)

VE>Можно пример в псевдокоде? Как предполагается это указывать?

указывать их, конечно, не хочется. хочется чтобы они вычислялись автоматически

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

VE>Можно пример в псевдокоде? Как предполагается это указывать?

вообще, что интересует? нотация, какая-то часть семантики?

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

VE>Тогда if-else тоже динамическая типизация.

Если при этом проверяется внутреннее устройство данных, то бишь их тип — несомненно.


VE>>>Не понял. Что должна делать такая функция? Ругаться при компиляции на разные типы? Или молча жрать все? Тогда в чём замысел?

V>>Например том, чтобы она смогла быть применена в таком контексте, где a и b могут выводиться как одни и те же типы, а могут и нет.

VE>Зачем?
VE>Тем более, что это не ПП, а речь-таки о нём шла.

V>>Речь идет о возможностях техники навроде static_if в С++. Возможностей Хаскеля для сравнимой реализации такой техники недостаточно, т.к. нет аппарата compile-time вычислений.
VE>Во-первых, как это нету?

Так что нету. Потому что нет параметризации типов константами и нет compile-time диспетчеризации по этим константам и нет частичного или явного инстанциирования шаблонных типов для конкретных комбинаций аргументов. Есть только такое инстанциирование для ф-ий.


VE>Во-вторых, можно пример, когда static_if не является сам по себе костылём?

Ха. Тогда любая статическая система типов — это костыль сам по себе, т.к. это способ перенести ограничения прикладной логики на компилятор. Я могу спросить в ответ привести пример, когда классы типов Хаскеля не являются костылем? Вот это аналогично. static_if покрывают возможности ограничений, вводимых классами типов, + еще позволяют сверху наложить кучу других ограничений. На сегодня, используя boost::type_traits — выразить как ограничения фактически любые отношения м/у типами или мемберами типов в системе типов С++.