Здравствуйте, vdimas, Вы писали:
DM>>Типизация — это навешивание на каждое выражение в программе некоторого ярлыка-типа. Можем в компайл-тайме навесить достаточно конкретные типы на все — получили статическую типизацию. Не можем и вынуждены навешивать один неконкретный ярлык dynamic — получили динамическую. V>Речь была о динамической типизации в рамках статически-типизированных языков. И с какой радости dynamic должен быть один?
Я не говорю, что должен. Это лишь пример.
V>>>Да и о чем спорить? По-определению АлгТД — это такой тип данных, в который упаковываются значения других типов. Вариант, он и в Африке вариант. DM>>Это фиговое и неправильное определение, ведь "внутри" может оказаться он сам, не только "другие типы".
data Tree a = Leaf | Node a (Tree a) (Tree a)
V>Вот, популярная ошибка. В общем виде такая структура в статически-типизированном языке представима только через боксирование (уже доказано чуть выше по ветке, почему именно так и никак иначе). Поэтому хранится не само значение типа, а его боксированное представление.
Ну так и сам тип Tree a — такой же точно боксированный, если уж вдаваться в эти тонкости. Поэтому слева и справа от = тип один и тот же упоминается. Так что ошибка у тебя.
Здравствуйте, VoidEx, Вы писали:
VE>>>Чтобы не передавать Eq a явно. Правда, для этого вовсе не обязательно надо было городить классы типов. V>>А что можно? VE>implicit arguments
А придумать синтаксис, чтобы не конфликтовал с имеющимся?
Классы типов Хаскеля хороши тем, что идут в синтаксисе как бы "сбоку", предоставляя затем доступ к своему механизму так же как обычным ф-иям.
V>>Я имел ввиду, что компилятор "видит" все инстансы классов типов из зависимых модулей. VE>Считайте, что они импортируются неявно. Система типов от этого не страдает.
Это если рассматривать систему типов в отрыве от путей ее реализации... Мне во всей этой беседе как раз был интересен момент реализации обсуждаемых св-в системы типов (ПП) и именно для случая статически-компилируемых языков.
Кстати, как раз выяснили в процессе обсуждения, что для полноценного ПП требуется вывод типов чуть помощнее, близкий по мощности к зависимым типам.
VE>Типы Base * и Child * — разные. Не Base и Child, а именно Base * и Child *. Где тут реинтепретация памяти?
Будет различная интерпретация числового значения адреса. Т.е. что касается адресной арифметики С++, то числовые значения адреса ЗАВИСЯТ от их типов, в отличие от С:
Т.е. сравнение указателей, например, происходит в зависимости от типов указателей, а не просто от внутреннего их числового представления.
В общем, адресная арифметика С++ такова, чтобы транзитивно протянуть зависимости от типа указателя до необходимой интерпретации памяти по этому указателю. Для base2Ptr будет сделано числовое смещение адреса относительно childPtr, чтобы указатель попал на область памяти типа Base2 в теле типа Child.
V>>Почему нет, если речь идет непосредственно об этом представлении? Например, когда мы обсуждаем компилятор статически-типизируемого языка, а не некий интерпретатор.
VE>Потому, что тогда мы придём к вырожденному случаю: при любом ветвлении программа ведёт себя с памятью по-разному.
Если представление памяти гарантировано одинаково, то нет. Твой факториал и сравнение на 0 и 1 тому пример, т.к. в Хаскеле целые числа — это случай выродженного алгТД, где значение алгТД представлено только значением дискриминатора. Т.е. преставление остатка значения варианта всегда будет пустой тупл, не требующий никакой интерпретации. А если представление в памяти разное, то я процесс приведения неизвестного устройства значения к известному и называю динамической типизацией для случая статически типизированного языка. Чем тебе не нравится приведение ссылочных типов в дотнете, например, или dynamic_cast в С++? Чем же отличается матч АлгТД?
VE>Т.е. проверка на if (x == 0) меняет её работу с памятью, т.е. приводит к различной её интерпретации.
если x — дискриминатор варианта, а затем происходит работа с непустым телом варианта соответствующего типа для x==0, то несомненно.
Почему на Хаскеле нельзя реализовать свою некую самописную систему алгебраических типов, а на С/С++ можно? Наверно потому, что Хаскель упрятал в себя технику реинтерпретации памяти, требуя от кода некий контракт, в виде конструкции ПМ, а в С/С++ эта техника доступна и позволяет реализовать АлгТД тысячами способов?
Например, бустовский variant абсолютно типобезопасен и так же требует некий контракт для матча дискриминатора варианта, это т.н. static visitor. Хотя конкретный метод визитора выбирается конечно динамически. Прямо как ветка ПМ.
VE>И именно поэтому важно не то, что с памятью работают иначе (ибо это всегда так), а то, как на это дело наложена система типов.
Есть мнение, что система типов — это лишь инструмент для разметки памяти под данные и связи кода с данными.
А при полном отсутствии хоть какого-нибудь вида полиморфизма, как в чистом С или ассемблере, система типов нужна только для разметки памяти. (В ассемблерах есть простые типы данных, а в некоторых даже составные)
V>>И да, содержимое АлгТД, кроме вырожденных случаев (на которые тебя упорно тянет), невозможно определить ДО выполнения. Именно поэтому в ПМ по дискриминатору АлгТД более одной ветки, под все необходимые случаи, возможные в рантайм. А ведь в реальности многие из этих веток могут быть "мертвыми", т.е. не быть вызванными ни разу. Как тебе такое "property of a programme we can determine without executing the program"?
VE>Мёртвыми могут быть ветки и в банальном Си. Иногда компилятор это даже умеет определять и оптимизировать. К типизации это отношения не имеет.
Имеет согласно твоего определения. Т.е. статически компилятор не способен узнать тип завернутого в алгТД значения. Способен только через техники суперкомпиляции, а в этой технике никакой системы типов уже нет. ЧТД.
VE>Или что, назовём динамической типизацией лишние if, когда согласно алгоритму в этот if мы никогда не попадём (но при этом выяснить это в compile-time = решить проблему останова)?
Правильно мыслишь. Поэтому система с зависимыми типами более мощная, что позволяет экономить некоторые из этих if, т.к. для кое-каких ограничений проблему останова решать необязательно, чтобы узнать требуемую ветку в compile-time.
VE>>>Мол, что (x:int){x==0}, что (x:int){x>0}, один чёрт int, 4 байта, да?
V>>Да, значение дискриминатора (т.е. некое его представление) само имеет некий тип, а что? Тебя смущает, что этот тип тебе не доступен в общем случае? ИМХО, лишь для того, чтобы не ограничивать способ реализации. Но для случая встроенных интегральных типов Хаскеля — доступен. Т.е. для некоего мн-ва встроенных типов, для которых объявлено, что они являются АлгТД, прямо в спецификации указан способ представления дискриминаторов этих АлгТД. Теперь полегчало?
VE>Чего? Ты читаешь, что я пишу? Причём тут АлгТД вообще? VE>Давай перепишу иначе: VE>(x:int){x > 10} и (x:int) { 10 * x + 23 < 2332 } — это разные типы. Но по-твоему получается, что нет. VE>Нотация (x:t){f(x)} означает, что x принадлежит подмножеству t такому, что выполняется f(x). Это тип. Никакой f не вычисляется в runtime и даже не существует. VE>Типы разные, представление — абсолютно одинаковое.
Дык, уточняй, что речь уже не о Хаскеле. Я откуда по двум скобкам пойму, что ты там пишешь?
Если ты начал говорить о зависимых типах, то вот тебе и ограничения области действия, которые вполне решают проблему останова. Т.е. нет смысла тащить признак типа в рантайм, коль в рантайм он заведомо не будет проверяться.
Здравствуйте, D. Mon, Вы писали:
V>>Вот, популярная ошибка. В общем виде такая структура в статически-типизированном языке представима только через боксирование (уже доказано чуть выше по ветке, почему именно так и никак иначе). Поэтому хранится не само значение типа, а его боксированное представление.
DM>Ну так и сам тип Tree a — такой же точно боксированный, если уж вдаваться в эти тонкости.
А вот это как раз необязательно, когда речь идет об иммутабельной системе типов, вроде обсуждаемой SystemF. Это может быть само значение, а не ссылка. И умение делать подобную оптимизацию составляет одну из характеристик ML-языков.
ИМХО, то, что некоторые языки не различают ссылочных типов и обычных вносит некоторую путаницу, как value/ref-типы дотнета. Т.к. ссылку на значение начинают считать за само значение. Это абсолютно верно в иммутабельной среде с т.з. значений, согласен, но типы при этом разные!
Т.е. компилятор берет приведение типов из ссылочных в обычные на себя прозрачно для программиста. А подробности всплывают только тогда, когда требуется обеспечить интероперабельность.
VE>Невозможность надо доказывать. То, что пока не привели такого определения, не означает, что его нет. VE>Например, навскидку, динамическая типизация: VE>Каждому типу a ставится в соответствие множество типов T свободных по a таких, для каждого t : T существуют примитивные параметрически полиморфные (с ограничением по множеству T) функции VE>
VE>cast : a -> t
VE>dynamicCast : t -> Maybe a
VE>
VE>При этом выполняется VE>
VE>backCast : a -> Prop
VE>backCast x = dynamicCast (cast x : t) === Just x
VE>
VE>Уточнение: сводобных по a означает, что t : T не содержит в своем выражении тип a. Т.е. например Either a b туда не подходит.
ок
теперь возьмем блок кода TResult F(TSource) такой, что:
1. содержит if
2. if нередуцируем (нельзя переписать данный блок кода так, чтобы он не содержал if-а)
3. код чистый
4. с точки зрения теории множеств, каждый тип есть множество значений
5. обозначим множество значений которое приходит на вход F как MSource, которое передается в block1 как MSource1, в block2 как MSource2 (это можно сделать, так как predicate — чистая функция, и одно и тоже значение из MSource, всегда будет строго попадать или в block1, или в block2)
6. из п.2(функция нередуцируема) множество MSource1 строго меньше MSource
7. из теории множеств следует, что наличие множеств MSource1 и MSource, где MSource1 является строгим подмножеством MSource задает однозначным образом следующие функции отличные от тривиальных
где тип TSource соответствует множеству MSource, тип TSource1 множеству MSource1
что и требовалось доказать, что каждый if в коде однозначно задает набор функций аналогичный набору функций при динамической типизации
соответственно, каждый if в коде образует динамическую типизацию.
Здравствуйте, vdimas, Вы писали:
DM>>Ну так и сам тип Tree a — такой же точно боксированный, если уж вдаваться в эти тонкости.
V>А вот это как раз необязательно, когда речь идет об иммутабельной системе типов, вроде обсуждаемой SystemF. Это может быть само значение, а не ссылка. И умение делать подобную оптимизацию составляет одну из характеристик ML-языков.
Тогда стоит рассмотреть и оптимизацию, когда значение АлгТД, состоящее из одного дискриминатора, хранится небоксированным. В общем, это уже тонкости реализации, к теории типов имеющие мало отношения.
V>ИМХО, то, что некоторые языки не различают ссылочных типов и обычных вносит некоторую путаницу, как value/ref-типы дотнета. Т.к. ссылку на значение начинают считать за само значение. Это абсолютно верно в иммутабельной среде с т.з. значений, согласен, но типы при этом разные!
Зависит от того, что считать типом. По-моему, типы одинаковые.
DM> По-твоему, всякое определение должно включать в себя определения и подробности всех используемых терминов? Это нереально. Человечество придумало другой способ, получше: использовать лишь названия терминов, определения которых даются отдельно.
Мало ли что там придумало человечество, еретиков сжигать тоже оно придумало, и в целом неплохо работало...
Важно не что человечество придумало, а что зафиксировано в научном подходе, а в научном подходе требуется, чтобы все используемые определения можно было однозначно восстановить и при этом требуется, чтобы после восстановления не было циклов.
Соответственно я тебя спрашиваю:
1. каким образом я могу восстановить используемые термины в твоем определении?
2. при попытках восстановления твоего определения я столкнулся с петлями, когда, например, type system определяется через classifying, а classyfing через несколько шагов определяется через type system. что мне с этим делать?
DM>Ок, займусь завтра. Только как бы это не вылилось в просьбы с твоей стороны дать определения всем-всем словам русского и английского языков, так мы нескоро закончим. Я (как и цитируемый в вики Пирс) надеялся на наличие у собеседников каких-то общих знаний, но видимо зря.
попробуй. только скорее всего не получится, навскидку type system является аксиоматическим понятием (как точка, множество или время) и не может быть определено, а может быть лишь описано для понимания через набор свойств.
отмечу что деление на определяемые понятия и на аксиоматические понятия очень важное, потому что во втором случае однозначного определения на самом деле нет и соответственно на него нельзя ссылаться при последующих логических построениях.
для аксиоматических понятий можно вводить лишь свойства и на них ссылаться.
DG>>можно ли при этом сгенерировать более эффективный код? хотя бы руками?
DM>В том конкретном случае, когда все аргументы известны при компиляции, можно суперкомпиляцией сразу получить программу, выводящую ответ, все вычисления выкинув.
позже я специально подчеркнул что я рассматриваю вариант, когда длина массивов и значения не известны на момент компиляции, а появляются в runtime-е. Это позволяет тот же пример сделать более выпуклым.
Здравствуйте, DarkGray, Вы писали:
DG>1. каким образом я могу восстановить используемые термины в твоем определении? DG>2. при попытках восстановления твоего определения я столкнулся с петлями, когда, например, type system определяется через classifying, а classyfing через несколько шагов определяется через type system. что мне с этим делать?
1,2: почитать учебник по теории типов, например. Тот же TAPL.
DM>>Ок, займусь завтра. Только как бы это не вылилось в просьбы с твоей стороны дать определения всем-всем словам русского и английского языков, так мы нескоро закончим. Я (как и цитируемый в вики Пирс) надеялся на наличие у собеседников каких-то общих знаний, но видимо зря.
DG>попробуй. только скорее всего не получится, навскидку type system является аксиоматическим понятием (как точка, множество или время) и не может быть определено, а может быть лишь описано для понимания через набор свойств.
Я не вижу оснований считать систему типов подобным понятием. Это такая же определябельная конструкция, как группа, кольцо, моноид, коалгебра и т.д.
Здравствуйте, DarkGray, Вы писали:
DG>>>можно ли при этом сгенерировать более эффективный код? хотя бы руками?
DM>>В том конкретном случае, когда все аргументы известны при компиляции, можно суперкомпиляцией сразу получить программу, выводящую ответ, все вычисления выкинув.
DG>позже я специально подчеркнул что я рассматриваю вариант, когда длина массивов и значения не известны на момент компиляции, а появляются в runtime-е.
Тогда кроме инлайнинга и кое-какого fusion'a (удаления промежуточных массивов или списков) там ничего ненаоптимизируешь.
DG>>пока ты копируешь определения из википедии — никакого сознания нет, есть лишь тот самый автомат из китайской комнаты, который механически подставляет необходимую ссылку на википедию, когда встречает ключевые слова. DG>>сознание определяют как умение выстраивать логические цепочки и гибкое адаптирование к контексту. DG>>при копировании определения из вики — ни первого, ни второго — нет.
DM>Во-первых, не надо путать сознание (consciousness) и интеллект/разум (intelligence), это очень разные вещи.
я их не путаю, я утверждаю, что первое невозможно без второго
и соответственно, на основе бритвы оккамы утверждаю, что если индивидуум не демонстрирует второе, то значит у него нет первого.
DM> Во-вторых, когда я цитирую википедию, я опираюсь на общую базу знаний и надеюсь, что используемые там слова собеседникам известны. В противном случае коммуникация крайне трудна.
этого не достаточно для коммуникации.
для успешной коммуникации слова должны быть не только известы, но и однозначно восстановимы до необходимый точности.
например, что такое красный всем известно, но невозможно однозначно вне контекста ответить на вопрос "Это красный?", когда человек показывает на фигуру цвета pink, orange, rose, ruby, rgb(255, 10, 0) и т.д.
DM> В-третьих, китайская комната как раз показывает, что даже демонстрация выстраивания логических цепочек не позволяет определить наличие "настоящего" разума. Зато логические ляпы вроде твоего позволяют показать недостаток разумности.
Есть подвох. Из теории информации следует, что для того, чтобы отличить логические ошибки от проблем при коммуникации (неточность при кодировании/декодировании, отличия в используемых словарях и т.д.) требуются специальные алгоритмы и большое кол-во попыток.
Если ты при коммуникации эти алгоритмы не используешь, то как ты отличаешь одно от другого?
Здравствуйте, vdimas, Вы писали:
V>А если представление в памяти разное, то я процесс приведения неизвестного устройства значения к известному и называю динамической типизацией для случая статически типизированного языка. Чем тебе не нравится приведение ссылочных типов в дотнете, например, или dynamic_cast в С++? Чем же отличается матч АлгТД?
В ПМ (для ML семейства) нет "приведения неизвестного устройства значения к известному" это тупо выбор _заранее_ известных вариантов.
Отличие от dynamic_cast принципиальное в рантайме ПМ ничего ни ищет, ни сравнивает типы, просто банально выполняет switch.
Если грубо перевести все на условный си получим:
enum {Type1_id, Type2_id, Type3_id};
struct Type1 {};
struct Type2 {};
struct Type3 {};
struct AlgTD
{
int type;
union
{
Type1 type1;
Type2 type2;
Type3 type3;
// ....
};
};
void tst(AlgTD x)
{
switch(x.type)
{
case Type1_id:
// ...break;
case Type2_id:
// ...break;
case Type3_id:
// ...break;
}
}
И никакой динамической типизации, только простейшее ветвление.
Здравствуйте, DarkGray, Вы писали:
DG>что и требовалось доказать, что каждый if в коде однозначно задает набор функций аналогичный набору функций при динамической типизации DG>соответственно, каждый if в коде образует динамическую типизацию.
Так с тобой-то я не спорю. Я-то как раз того же мнения. Чтоб либо динамическая типизация — любое ветвление, либо тогда АлгТД тоже не динамическая типизация. Мне же vdimas говорит, что if (x == 0) в Си — не динамическая типизация.
DM>Тогда кроме инлайнинга и кое-какого fusion'a (удаления промежуточных массивов или списков) там ничего ненаоптимизируешь.
вот есть следующий библиотечный код
type test = Int of int | Float of float | String of string
let dummy_id = function
| Int n -> n
| Float _ -> -1
| String _ -> -2
let dummy2 = function(ienumerable<test> items) = items.Select(item => dummy_id(item)).Sum();
и стоит задача написать(сгенерить) функцию main, которая на вход принимает последовательность байт (с возможностью random-доступа) вида:
network-int32 len;
последовательность<длина len, тип элемента network-int32> int-array;
network-int32 len2;
последовательность<длина len2, элемент float(4байта)> float-array;
network-int32 len3;
последовательность<длины len3,
элемент test,
элемент test хранится как строка(4байта длины + unicode string),
подтип int хранится как десятичная строка,
подтип float хранится как строка вида digit*[.digit*],
подтип String как строка,
отображение из строки в нужный подтип делается по лучшему совпадению:
строка из десятичных чисел - int,
digit*[.digit*] - float,
другое - String
>
len3 string-array;
и выводит на консоль результат:
dummy2(int-array);
dummy2(float-array);
какой самый эффективный вариант такой функции можно написать/сгенерить?
эффективность программы оценивается как (меньше — лучше): размер программы в байтах + 1e5 * кол-во тактов выполнения функции main
DG>>что и требовалось доказать, что каждый if в коде однозначно задает набор функций аналогичный набору функций при динамической типизации DG>>соответственно, каждый if в коде образует динамическую типизацию.
VE>Так с тобой-то я не спорю. Я-то как раз того же мнения. Чтоб либо динамическая типизация — любое ветвление, либо тогда АлгТД тоже не динамическая типизация. Мне же vdimas говорит, что if (x == 0) в Си — не динамическая типизация.
согласен ли ты с утверждением, что статическая типизация: это когда в исходнике if есть (в том или ином виде: ПМ, overloading и т.д.), а в генеренном коде if-а нет?
FR>Отличие от dynamic_cast принципиальное в рантайме ПМ ничего ни ищет, ни сравнивает типы, просто банально выполняет switch.
если все типы известны при генерации кода (новые типы после генерации не подгружаются, или при подгрузке новых типов происходит перегенерация кода), то dynamic_cast — это тоже банальный switch
Видимо, абстрактные примеры воспринимаются сложнее, поэтому перейду к конкретике.
Возьмём CPS-трансформацию, все АлгТД при этом исчезают. Исчезает ли динамическая типизация?
А теперь примеры:
1. Простой if-else
bool readFromConsole() { ... }
void test()
{
bool x = readFromConsole();
if (x)
foo(10);
else
bar("bar");
}
readFromConsole :: IO (Either Int String)
readFromConsole = do
x <- ...
if x then Left 10 else Right "bar"
test = do
v <- readFromConsole
case v of
Left x -> foo x
Right s -> bar s
readFromConsole :: (Int -> IO r) -> (String -> IO r) -> IO ()
readFromConsole left right = do
x <- ...
if x then left 10 else right "bar"
test = readFromConsole foo bar
2. Накопление результата списка
template <class It, class F>
F for_each(It b, It e, F f)
{
for (; b != e; ++b)
f(*b);
return f;
}
std::list<int> l = { 1, 2, 3 };
void test()
{
int r = 10;
for_each(l.begin(), l.end(); [&r] (int x) { r += x; });
}
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl f v [] = v
foldl f v (x:xs) = foldl (f v x) xs
l :: [Int]
l = [1, 2, 3]
test = foldl (+) 10 l
data ListAlgebra a r = ListAlgebra r (a -> r -> r)
foldList :: (a -> b -> a) -> a -> ListAlgebra b a
foldList f v = ListAlgebra nil cons where
nil = v
cons x xs = f xs x
l :: ListAlgebra Int r -> r
l (ListAlgebra nil cons) = cons 1 (cons 2 (cons 3 nil))
test = l (foldList (+) 10)
Look! No ADT!
В каких случаях, на твой взгляд, есть динамическая типизация, в каких нет, и почему?
Здравствуйте, DarkGray, Вы писали:
DM>>Во-первых, не надо путать сознание (consciousness) и интеллект/разум (intelligence), это очень разные вещи.
DG>я их не путаю, я утверждаю, что первое невозможно без второго DG>и соответственно, на основе бритвы оккамы утверждаю, что если индивидуум не демонстрирует второе, то значит у него нет первого.
А это ещё надо доказать. Связь между интеллектом и сознанием весьма и весьма туманна.
VE>А это ещё надо доказать. Связь между интеллектом и сознанием весьма и весьма туманна.
если не ударяться в мистику, то никакого тумана там нет.
сознание = способность ставить и решать задачи, а способность ставить и решать задачи определяется способностью применять интеллект (или другими словами, чем выше интеллект, тем более широкий круг задач поддается решению и тем более эффективно они решаются)
в частности, selfhood который часто включают в сознание, это для агента постановка и эффективное решение задачи:
1) декомпозиции мира по степени управляемости агентом
2) декомпозиция мира по степени зависимости от него поведения агента
Прямо как ветка ПМ.
