VE>Правильно ли я понимаю, что можно глядя на память понять, int там или unsigned int?
не вижу как связана верности/неверность этого утверждения и предыдущее утверждение.
DG>>раз необходимо делать выбор правильной версии операции — это уже означает, что есть что-то разное (или разная семантика операции, или разная семантика хранения в памяти)
VE>Операции разные, очевидно. Причём можно обе применять. Сам по себе int или unsigned int не определяет, какое там число (ну только "на словах"). А вот операция сравнения уже несёт такую информацию, так как определена по-разному в зависимости от интерпретации того, что ей передают.
что в твоем утверждение означает "можно применять"?
если я тебе передаю 8 байт и говорю — это два числа, раздели одно на другое, пожалуйста.
означает ли это что что ты их можешь делить как хочешь: как int/uint/float?
VE>По-моему, вы ставите лошадь впереди телеги. Тип несёт информацию о множестве допустимых значений, а как это хранить, выбирает реализация. Разумеется, вводя новые типы, вы основываете их на уже имеющихся, и реализация имеет механизм, позволяющий ей выбрать способ хранения нового типа. Но это не отновится к свойствам типизации как таковой, а побочный эффект от того, что тип накладывает ограничения.
тип отделяется от реализации (или сужение понятия типа до семантической составляющей) происходит только в чисто математических языках, таких как haskell.
и такого подхода недостаточно, как только например решаются вопросы эффективного выполнения, или использования одних и тех же типов данных разными языками.
VE>Таким образом нам либо придётся согласиться, что if (x == 0) — это динамическая типизация,
давай согласимся, что да, если это выполняется в runtime.
данный if отделяет два типа друг от друга: 0 и не 0.
VE> либо что выбор типа надо рассматривать в рамках той системы, о которой идёт речь (тогда в Си, разумеется, if (x == 0) не выбирает никакого типа, так как в Си не существует типа (x:int){x=0})
не удобный переход, в частности, тогда невозможно
провести параллели между типами в разных языках,
два языка не могут работать с одной и той же памятью и т.д.
зы
наука нас учить, что систему невозможно полностью понять находясь внутри системы, обязательно необходим выход в надсистему.
невозможно понять что такое тип находясь внутри только haskell-а(или только C), необходим выход в надсистему. Если рассмотреть, что такое тип одновременно с точки зрения haskell, C и python-а, работающих над одними и теми же данными, уже можно выйти на понятие типа.
Здравствуйте, DarkGray, Вы писали:
VE>>Правильно ли я понимаю, что можно глядя на память понять, int там или unsigned int?
DG>не вижу как связана верности/неверность этого утверждения и предыдущее утверждение.
Я ссылался на "необходимость реинтерпретации памяти", из которой следует взаимнооднозначное соответствие между типом и представлением в памяти (ибо иначе никакой реинтерпретации может и не понадобиться). Фраза не твоя, но разговор пошёл оттуда.
DG>что в твоем утверждение означает "можно применять"?
Не отвечаю, так как речь всё о том же была. Что разные типы могут лежать в памяти одинаково.
И разница между int и float не больше и не меньше, чем между (x:int){x=0} и (x:int){x>10}
VE>>Таким образом нам либо придётся согласиться, что if (x == 0) — это динамическая типизация,
DG>давай согласимся, что да, если это выполняется в runtime. DG>данный if отделяет два типа друг от друга: 0 и не 0.
Разумеется, речь о runtime. Проблема в том, что с системе типов Си++ нет таких типов, как "0" и "не 0". Поэтому в данном случае это не динамическая типизация, тип остаётся тот же. Однако если смотреть на Си++ через призму другой системы типов, это будет динамической типизацией.
Аналогично и в Haskell, выбор между вариантами АлгТД не меняет тип. То, что, глядя на это под каким-то другим углом с другой системой типов, начинает вдруг прорисовываться общность с проверкой типа runtime, типизацию динамической не делает.
DG>не удобный переход, в частности, тогда невозможно DG> провести параллели между типами в разных языках, DG> два языка не могут работать с одной и той же памятью и т.д.
Почему невозможно?
DG>зы DG>наука нас учить, что систему невозможно полностью понять находясь внутри системы, обязательно необходим выход в надсистему. DG>невозможно понять что такое тип находясь внутри только haskell-а(или только C), необходим выход в надсистему. Если рассмотреть, что такое тип одновременно с точки зрения haskell, C и python-а, работающих над одними и теми же данными, уже можно выйти на понятие типа.
Смотреть на типы с т.з. haskell, C и python — это не выйти в надсистему, а перейти в другую систему и при этом пытаться применить термины из одной системы с другой.
А вот если построить обобщённую систему, то различие в том, что в python тип один — dynamic. С т.з. python различий между строкой и числом не больше, чем между 10 и 0 с т.з. Haskell. В том же Haskell есть тип Dynamic, пара TypeRep и ссылка. Мы туда можем запихнуть строку и число, но x :: Dynamic и y :: Dynamic — это два значения одного и того же типа. А вот fromDyn x :: String и fromDyn y :: Int уже разных.
DM>>>Ccылаясь на TAPL Пирса, педивикия подсказывает: DM>>>In computer science, a type system may be defined as "a tractable syntactic framework for classifying phrases according to the kinds of values they compute".
DG>>во-первых: это определение type system, а не type
DM>Ну так речь шла о типизации, а не о типе.
если в понятие типа упоминается о способе хранения в памяти, а в более сложном понятии (типизация или type system) — этой составляющей нет, то можно сделать вывод, что определение сложного понятия как минимум не полное.
DG>>, во-вторых: это ужасное определение: определение должно определять понятие через более простые, а в данном случае — определение элементарного понятия "type system" идет через такиие неопределяемые понятия как: syntactic, framework, classifying, phrases, kind, compute, according. DG>>можно получить строгое формализованное определение всех перечисленных понятий?
DM>Можно. А нужно?
строго необходимо, если стоит задача получить корректное описание реальности. Если стоит задача покидаться ничего не значащими фразами из википедии, то не нужно
DM>Это одна структура в Си, содержащая внутри union. Она трактуется по-разному в зависимости от значения определенного поля.
здесь неявно подразумевается, что одна структура в C — это строго один математических тип.
из какого определения это следует?
DM>Я и говорю, подходов к определению может быть много.
определения все одинаковые?, или можно их классифицировать чем они лучше/хуже по тем или иным признакам?
пока ты копируешь определения из википедии — никакого сознания нет, есть лишь тот самый автомат из китайской комнаты, который механически подставляет необходимую ссылку на википедию, когда встречает ключевые слова.
сознание определяют как умение выстраивать логические цепочки и гибкое адаптирование к контексту.
при копировании определения из вики — ни первого, ни второго — нет.
DG>он внутри dummy_id как был так и остался, а поверх него навернут параметриче
DG>int dummy2(array<test> items) = items.Select(item => dummy_id(item)).Sum();
Как выше уже писали ничего ни изменится, dummy_id каким был таким и останется,
да и с чего ему меняться он же всегда принимает не полиморфный а конкретный тип
test.
VE>>>Правильно ли я понимаю, что можно глядя на память понять, int там или unsigned int?
DG>>не вижу как связана верности/неверность этого утверждения и предыдущее утверждение.
VE>Я ссылался на "необходимость реинтерпретации памяти", из которой следует взаимнооднозначное соответствие между типом и представлением в памяти (ибо иначе никакой реинтерпретации может и не понадобиться). Фраза не твоя, но разговор пошёл оттуда.
давай чуть вернемся.
изначально было твой вопрос: VE> Какая связь типов с памятью?
который я интерпретировал, что ты утверждаешь, что нет связи между типами и представлением в памяти
сейчас ты перешел к: взаимооднозначное соответствие между типом и представлением в памяти.
как связаны между собой: наличие/отсутствие взаимоднозначного соответствия между типами и представлением в памяти и утверждением, что нет связи между типом и представлением в памяти?
DG>>он внутри dummy_id как был так и остался, а поверх него навернут параметриче
DG>>int dummy2(array<test> items) = items.Select(item => dummy_id(item)).Sum();
FR>Как выше уже писали ничего ни изменится, dummy_id каким был таким и останется, FR>да и с чего ему меняться он же всегда принимает не полиморфный а конкретный тип FR>test.
потому что для данного кода можно сгенерить следующий код, который будет эффективнее и в нем не будет динамической типизации(кроме проверки на конец последовательности внутри Sum):
int dummy_id_int(int x) {return x;}
int dummy_id_float(float x) {return -1;}
int dymmy_id_string(string x) {return -2;}
int dummy2_int(array<int> items) = items.Sum();
int dummy2_float(array<float> items) = -1 * items.length;
int dummy2_string(array<string> items) = -2 * items.length;
[1, 2, 3].dummy2_int();
["1", "2", "3"].dummy2_string();
можно и вызовы dummy2_* развернуть, но для более явного примера, будем считать,
что длина и значения массивов не известны на этапе компиляции,
но тип элементов известен и он одинаковый для всех элементов внутри каждого массива
FR>Как выше уже писали ничего ни изменится, dummy_id каким был таким и останется, FR>да и с чего ему меняться он же всегда принимает не полиморфный а конкретный тип FR>test.
Это утверждение неявно использует допущение, что описание функции в ЯП и генеренный для нее код соотносится как 1 к 1.
Такое допущение сильно упрощает действительность, и и является неверным и опасным.
VE>Разумеется, речь о runtime. Проблема в том, что с системе типов Си++ нет таких типов, как "0" и "не 0".
что ты вкладываешь в "есть тип или нет типа в языке"?
какие необходимые, достаточные и желательные условия необходимы, чтобы можно было сказать, что в ЯП Zzz есть тип Xxx?
Здравствуйте, D. Mon, Вы писали:
VE>>>Спорят с тем, что это что-то вроде динамической типизации. Проблема в том, что термин "типизация" тут как-то не определили. V>>Определили. Это проверка/тестирование типа в рантайм.
DM>Это фиговое и неправильное определение. DM>Типизация — это навешивание на каждое выражение в программе некоторого ярлыка-типа. Можем в компайл-тайме навесить достаточно конкретные типы на все — получили статическую типизацию. Не можем и вынуждены навешивать один неконкретный ярлык dynamic — получили динамическую.
Речь была о динамической типизации в рамках статически-типизированных языков. И с какой радости dynamic должен быть один? Это нигде не ограничивается, кроме как в реализации некоторых языков. Например, в С++ таких корневых dynamic может быть бесчисленное мн-во.
V>>Да и о чем спорить? По-определению АлгТД — это такой тип данных, в который упаковываются значения других типов. Вариант, он и в Африке вариант.
DM>Это фиговое и неправильное определение, ведь "внутри" может оказаться он сам, не только "другие типы". DM>
DM>data Tree a = Leaf | Node a (Tree a) (Tree a)
DM>
Вот, популярная ошибка. В общем виде такая структура в статически-типизированном языке представима только через боксирование (уже доказано чуть выше по ветке, почему именно так и никак иначе). Поэтому хранится не само значение типа, а его боксированное представление. Т.е. еще раз более обще (не обязательно ограничиваясь АлгТД): рекурсивный тип в общем случае НЕ МОЖЕТ хранить значение собственного типа, он может хранить только боксированное значение собственного типа.
DM>Вариант так умеет?
Ес-но умеет: make_recursive_variant. Через точно такую же технику, ес-но.
Здравствуйте, VoidEx, Вы писали:
V>>Ну это ты далеко зашел в рассуждениях. Естественно, на любом тьюринг-полном языке можно написать некий интрепретатор другого тьюринг-полного языка с его системой типов, отличной от исходной. Этот случай обсуждать заведомо неинтересно.
VE>Крайний случай неинтересно, но так как мы уже встали на шаткую тропинку, называя диспатч по вариантам АлгТД "динамической типизацией", тогда хотелось бы разобраться, где именно находится та граница. А для этого надо чётко формалировать это понятие.
Классная беседа.
Тогда нафига классы типов вообще нужны?
V>>Дело в том, что С++ static_if в большинстве случаев не нужен, он удобен лишь для диагностики, остальное система типов С++ разруливает и так. Т.е. всё, что может быть описано через static_if, может быть описано и без него или даже не описано совсем, а получится "по факту". Т.е. это не костыль, а сахар. VE>enable_if, надо полагать, тоже "всего лишь сахар"?
Да, коль и так требуемый результат достижим через имеющуюся систему типов. Для случая классов типов в Хаскеле — не достижим.
V>>А вот классы типов — натуральный костыль, без которого многие трюки в Хаскеле просто не взлетят.
VE>Например?
Например, обсуждаемый пример, где Nil и Cons — это совершенно независимые типы, а не конструкторы одного АлгТД. И где де-факто рекурсия была сделана на полиморфном аргументе, а не рекурсивном АлгТД. Т.е. классы типов позволяют использовать в алгоритмах независимые типы.
V>>А костыль это потому, что изначально в языке отсутствовала концепция контрактов/интерфейсов.
VE>Классы из Haskell98 полностью заменяются обычными АлгТД. Более того, они обычные АлгТД и есть. Это как раз примитивнейший сахар, в отличие от static_if, который либо есть, либо нету, и ничем не заменить.
Мне только что доказывали, что это не так. Хотя я именно настаиваю, что "унутре" реализация классов-типов может быть реализована на той же технике, что АлгТД. Почему и просил распечатку сишного промежуточного кода примера.
V>>И вот ее заменяет этот недокостыль. Исключительно из-за скудной системы типов, где все пользовательские типы данных — это АлгТД.
VE>Классы типов — это АлгТД.
Таки нет. АлгТД имеет вполне конкретное определение. А тот факт, что классы типов конкретно в Хаскеле, с его, скажем так, особенностью представления модулей, вполне можно выразить через неявные АлгТД — это частность, которая может исчезнуть при другом представлении модулей. Просто сейчас компиляторам доступен "исходник" (пусть даже в распаршенном виде) всех используемых модулей, что можно в процессе компиляции статически сгенерить АлгТД по всем инстансам класса.
Здравствуйте, DarkGray, Вы писали:
VE>>Я ссылался на "необходимость реинтерпретации памяти", из которой следует взаимнооднозначное соответствие между типом и представлением в памяти (ибо иначе никакой реинтерпретации может и не понадобиться). Фраза не твоя, но разговор пошёл оттуда.
DG>давай чуть вернемся.
Давай.
DG>изначально было твой вопрос: VE>> Какая связь типов с памятью?
Нет, изначально было то, на что я задал такой вопрос. И я даже процитировал.
DG>который я интерпретировал, что ты утверждаешь, что нет связи между типами и представлением в памяти
Утерял контекст, а потом интерпретировал.
DG>сейчас ты перешел к: взаимооднозначное соответствие между типом и представлением в памяти.
Здравствуйте, DarkGray, Вы писали:
DG>если в понятие типа упоминается о способе хранения в памяти
Ничего там не упоминается. Сишный int можно хранить хоть boxed. Система типов (и сами типы) останется той же. Другое дело, что стандарт описывает не только систему типов.
VE>>Разумеется, речь о runtime. Проблема в том, что с системе типов Си++ нет таких типов, как "0" и "не 0".
DG>что ты вкладываешь в "есть тип или нет типа в языке"? DG>какие необходимые, достаточные и желательные условия необходимы, чтобы можно было сказать, что в ЯП Zzz есть тип Xxx?
Очевидно, возможность статически проверить принадлежность в такому типу.
DG>>не удобный переход, в частности, тогда невозможно DG>> провести параллели между типами в разных языках, DG>> два языка не могут работать с одной и той же памятью и т.д.
VE>Почему невозможно?
если ты говоришь, что каждая type system полностью независима от другой, и что в типе не указано как он хранится в памяти, то невозможно с map<string, array<int>> работать из haskell-я, из C++ и из питона, обращаешь к представлению данного типа в памяти напрямую.
DG>>зы DG>>наука нас учить, что систему невозможно полностью понять находясь внутри системы, обязательно необходим выход в надсистему. DG>>невозможно понять что такое тип находясь внутри только haskell-а(или только C), необходим выход в надсистему. Если рассмотреть, что такое тип одновременно с точки зрения haskell, C и python-а, работающих над одними и теми же данными, уже можно выйти на понятие типа.
VE>Смотреть на типы с т.з. haskell, C и python — это не выйти в надсистему, а перейти в другую систему и при этом пытаться применить термины из одной системы с другой.
при выходе в надсистему появляется обобщенный Type (будем его писать с большой буквы для однозначности), которые включает в себя C-тип, Haskell-тип, python-тип, ATS-тип и т.д
Соответственно Type включает в себя все возможности, которые были у C/Haskell/python/ats-типов и т.д.:
если C-тип умеет описывать как данные хранятся в памяти, значит и Type умеет,
если Haskell умеет описывать параметрические типы (функциональные типы и т.д.), значит и Type умеет,
если ATS делит типы на те, которые переносятся в runtime и те, которые не переносятся, значит и Type тоже такое умеет,
если Haskell умеет скрывать детали реализации (способ хранения типа в памяти), а типы C(или тем более asm) этого не делают — значит Type умеет и так, и так — в зависимости от необходимости (или угла рассмотрения)
и т.д.
DG>потому что для данного кода можно сгенерить следующий код, который будет эффективнее и в нем не будет динамической типизации(кроме проверки на конец последовательности внутри Sum):
В моем коде нет динамической типизации.
Рантаймное ветвление при ПМ есть, почему ты и vdimas называете это динамической типизацией я не понимаю,
хотя признаюсь всю ветку внимательно не читал.
DG>можно и вызовы dummy2_* развернуть, но для более явного примера, будем считать, DG>что длина и значения массивов не известны на этапе компиляции, DG>но тип элементов известен и он одинаковый для всех элементов внутри каждого массива
Мне кажется ты не понимаешь что в том коде который привел я (и по его мотивам D. Mon)
нет разных типов и нет полиморфизма.
Есть один единственный тип:
type test = Int of int | Float of float | String of string
и фукция dummy_id мономорфна и работает с этим типом а функция dummy2 которую привел
D. Mon с массивами этого типа, а не с массивами int, float или string. Так что такая
развертка которую ты хочешь просто невозможна.
DG>Это утверждение неявно использует допущение, что описание функции в ЯП и генеренный для нее код соотносится как 1 к 1. DG>Такое допущение сильно упрощает действительность, и и является неверным и опасным.
Генеренный код в данном случае делает ровно то что описывает ЯП а именно статически типизированную
неполиморфную функцию.
Какое отношение боксирование имеет к динамической типизации?
VE>>Без них всё ок.
V>Классная беседа. V>Тогда нафига классы типов вообще нужны?
Чтобы не передавать Eq a явно. Правда, для этого вовсе не обязательно надо было городить классы типов.
В любом случае, ни о какой "скудности системы типов" и "трюках, которые не взлетят без классов типов" речи вообще не идёт.
V>Да, коль и так требуемый результат достижим через имеющуюся систему типов. Для случая классов типов в Хаскеле — не достижим.
Ну-ка, что, например, недостижимо в Хаскеле без классов типов?
V>Например, обсуждаемый пример, где Nil и Cons — это совершенно независимые типы, а не конструкторы одного АлгТД. И где де-факто рекурсия была сделана на полиморфном аргументе, а не рекурсивном АлгТД. Т.е. классы типов позволяют использовать в алгоритмах независимые типы.
Этот пример переписывается без использования классов типов один в один.
V>Мне только что доказывали, что это не так. Хотя я именно настаиваю, что "унутре" реализация классов-типов может быть реализована на той же технике, что АлгТД. Почему и просил распечатку сишного промежуточного кода примера.
Не знаю, кто вам что доказывал, но если этот пример таки написать на Си, у вас там будут те же самые проверки в том же объёме. Cons у вас будет не шаблоном, а struct Cons { int value; void * p; } и т.п.
Статическую проверку можно будет наложить шаблоном и кастами void* <-> T*
На исходном Си++ примере же у нас кодогенерация, которая не даёт тех же возможностей, что и Haskell, но зато избавлена от проверок. Ну дак и на TemplateHaskell это можно сделать точно так же. Без проверок.
Итого: либо оба примера работают, как хотел МигМит, с одинаковым кол-вом проверок, либо оба не используют проверки, как Си++, но и никакой вводимой длины списка не будет, а только определённая в compile-time.
V>Таки нет. АлгТД имеет вполне конкретное определение. А тот факт, что классы типов конкретно в Хаскеле, с его, скажем так, особенностью представления модулей, вполне можно выразить через неявные АлгТД — это частность, которая может исчезнуть при другом представлении модулей. Просто сейчас компиляторам доступен "исходник" (пусть даже в распаршенном виде) всех используемых модулей, что можно в процессе компиляции статически сгенерить АлгТД по всем инстансам класса.
Это шутка что ли или непонимание?
foo :: Eq a -> a -> a -> Bool
foo (Eq eq neq) x y = eq x y
Где тут используются "особенности представления модулей"?
Eq самый обыкновенный ADT с одним конструктором.
Давайте-ка я перепишу:
foo :: (a -> a -> Bool, a -> a -> Bool) -> a -> a -> Bool
foo (eq, neq) x y = eq x y
Что теперь? Туплы и ФВП у нас работают тоже благодаря особенностям представления модулей?
