Здравствуйте, D. Mon, Вы писали:
DM>Это фиговое и неправильное определение, ведь "внутри" может оказаться он сам, не только "другие типы". DM>
DM>data Tree a = Leaf | Node a (Tree a) (Tree a)
DM>
DM>Вариант так умеет?
Если под вариантом имеется в виду упоминавшийся выше boost::variant то умеет http://www.boost.org/doc/libs/1_49_0/doc/html/variant/tutorial.html#variant.tutorial.recursive
Он вообще в принципе все почти возможности АТД эмулирует, конечно местами громоздко и коряво,
но включая даже паттерн матчинг с статистическим контролем полноты распаковки, для этого
правда нужно писать отдельный класс реализующий перегруженные операторы для всех типов
входящих в вариант:
DG>я больше говорил в разрезе, что если брать ПМ как он реализован в том же Haskell-е, то он будет генерить тормозной код, не сильно лучше, чем какая-нибудь динамика аля питон.
Если брать OCaml, в котором примерно похожий на Хаскель ПМ, реализуется очень эффективно,
например такой (бессмысленный) код:
type test = Int of int | Float of float | String of string
let dummy_id = function
| Int n -> n
| Float _ -> -1
| String _ -> -2
let _ = Printf.printf "%d\n" (dummy_id (Int 4))
превращается
camlPm_tst__dummy_id_65:
.L103:
movq %rax, %rbx
movzbq -8(%rbx), %rax
cmpq $1, %rax
je .L101
jg .L100
.L102:
movq (%rbx), %rax
ret
.align 4
.L101:
movq $-1, %rax
ret
.align 4
.L100:
movq $-3, %rax
ret
То есть всего несколько ассемблерных инструкций, вполне близко к тому во что компилируют
switch C++ компиляторы.
DG>соответственно, на основе этих condition-ов для выражения isEven(rnd * 2) вообще вычисляется, что его post-condition: true DG>и что соответственно его можно заменить целиком на true при компиляции
В общем, как я понимаю, предлагается использовать механизм доказательства теорем для доказательства независимости от какой-то грязи.
DG>в этом коде Get.result = F(x, _cache, Zzz.My) и соответственно чистота(Get.result) = чистота(x) && чистота(_cache) && чистота(Zzz.My). x — чистая переменная, т.к. readonly, Zzz.My — чистая по определению, остался _cache. DG>_cache — может быть в двух состояниях: или null, или результат Zzz.My. Нулевое состояние _cache снаружи наблюдать(обнаружить) невозможно, т.к. для метода get: F(x, null, Zzz.My) == F(x, != null, Zzz.My), а других способов получить доступ к _cache нет.
При этом грязь, имхо, лучше вводить через типы. Если формализовать и выделить виды грязи, то убирание чистоты сведётся к написанию функции вида SomeDirt a -> a.
Здравствуйте, vdimas, Вы писали:
V>Ну это ты далеко зашел в рассуждениях. Естественно, на любом тьюринг-полном языке можно написать некий интрепретатор другого тьюринг-полного языка с его системой типов, отличной от исходной. Этот случай обсуждать заведомо неинтересно.
Крайний случай неинтересно, но так как мы уже встали на шаткую тропинку, называя диспатч по вариантам АлгТД "динамической типизацией", тогда хотелось бы разобраться, где именно находится та граница. А для этого надо чётко формалировать это понятие.
V>А что не так без них?
Без них всё ок.
V>Дело в том, что С++ static_if в большинстве случаев не нужен, он удобен лишь для диагностики, остальное система типов С++ разруливает и так. Т.е. всё, что может быть описано через static_if, может быть описано и без него или даже не описано совсем, а получится "по факту". Т.е. это не костыль, а сахар.
enable_if, надо полагать, тоже "всего лишь сахар"?
V>А вот классы типов — натуральный костыль, без которого многие трюки в Хаскеле просто не взлетят.
Например?
V>А костыль это потому, что изначально в языке отсутствовала концепция контрактов/интерфейсов.
Классы из Haskell98 полностью заменяются обычными АлгТД. Более того, они обычные АлгТД и есть. Это как раз примитивнейший сахар, в отличие от static_if, который либо есть, либо нету, и ничем не заменить.
V>И вот ее заменяет этот недокостыль. Исключительно из-за скудной системы типов, где все пользовательские типы данных — это АлгТД.
Здравствуйте, vdimas, Вы писали:
DG>>>а почти весь ПМ (при условии, что есть несколько веток) в это и транслируется. VE>>Любая программа содержит условные переходы, но динамической типизацией это называть было бы крайне странно. VE>>Поэтому первостепенной задачей было бы как раз решить, что же такое динамическая типизация.
V>Это такое условное ветвление, целью которого является выбрать ветку алгоритма, умеющего работать с неким конкретным устройством значения (т.е. с неким конкретным типом).
И if именно это и делает. Не путайте то, какие байтики лежат, с типом. В случае указателя конкретное устройство значения одно и то же — указатель, но тип тем не менее разный.
V>Т.е. имеем следующее: в compile-time пишем алгоритмы под все возможные (или уникально обрабатываемые) типы, ожидаемые в некоей точке алгоритма, а в рантайм через ветвление выбираем одну из веток алгоритма, согласно фактически поданному типу значения.
V>Для работоспособности этой схемы обязательно нужен некий механизм реинтерпретации памяти. Например, в C# это приведение типов as или через (Type1), в С++ через dynamic_cast или через reinterpret_cast, еще через встроенный рантайм-полиморфизм, в ML-языках через паттерн-матчинг.
Какая связь типов с памятью?
Вот тут, например, о каком мезанизме реинтерпретации памяти вообще в принципе может идти речь?
VE>>То, что при наличии разных вариантов у АлгТД происходит ветвление — это динамическая типизация в той же мере, что и ветвление по 0 и не 0 в факториале.
V>Нет.
Да.
Я вас удивлю, но (x:int){x==0} — это тип. У него ровно одно значение. И if это проверяет, а затем работает с этим типом.
Formally, a type can be defined as "any property of a programme we can determine without executing the program"
Вы же почему-то под типом подразумеваете какое-то внутреннее представление. Мол, что (x:int){x==0}, что (x:int){x>0}, один чёрт int, 4 байта, да? Ну так и указатель любой 4 (или 8) байта, ан нет, типы-то разные!
Здравствуйте, samius, Вы писали:
S>Здравствуйте, VoidEx, Вы писали:
VE>>Классы типов — это АлгТД. S>Можно развернуть мысль?
Можно.
module Equal (
) where
import Prelude hiding (Eq(..))
data Eq a = Eq {
equal :: a -> a -> Bool,
notEqual :: a -> a -> Bool }
boolEq :: Eq Bool
boolEq = Eq eq neq where
eq True True = True
eq False False = True
eq _ _ = False
neq x y = not $ eq x y
intEq :: Eq Int
intEq = Eq eq neq where
eq 0 0 = True
eq 0 x = False
eq x 0 = False
eq x y = eq (pred x) (pred y)
neq x y = not $ eq x y
foo :: Eq a -> a -> a -> a -> Bool
foo (Eq eq neq) x y z = eq x y || eq y z
test1 = foo boolEq True False False
test2 = foo intEq 0 2 5
Здравствуйте, VoidEx, Вы писали:
VE>Здравствуйте, samius, Вы писали:
S>>Здравствуйте, VoidEx, Вы писали:
VE>>>Классы типов — это АлгТД. S>>Можно развернуть мысль?
VE>Можно.
VE>
VE>data Eq a = Eq {
VE> equal :: a -> a -> Bool,
VE> notEqual :: a -> a -> Bool }
VE>
Ясно. Это вполне ожидаемо, я лишь упустил из виду что record это частный случай АлгТД.
DM>Типизация — это навешивание на каждое выражение в программе некоторого ярлыка-типа. Можем в компайл-тайме навесить достаточно конкретные типы на все — получили статическую типизацию. Не можем и вынуждены навешивать один неконкретный ярлык dynamic — получили динамическую.
навешивание типа на выражение — это определение статической типизации, а не типизации вообще.
тип int от string в скриптах отличается? каким образом?
по твоему определению получается что различных типов в скриптах вообще нет.
Здравствуйте, DarkGray, Вы писали:
DM>>Типизация — это навешивание на каждое выражение в программе некоторого ярлыка-типа. Можем в компайл-тайме навесить достаточно конкретные типы на все — получили статическую типизацию. Не можем и вынуждены навешивать один неконкретный ярлык dynamic — получили динамическую.
DG>навешивание типа на выражение — это определение статической типизации, а не типизации вообще.
Ccылаясь на TAPL Пирса, педивикия подсказывает:
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>тип int от string в скриптах отличается? каким образом?
Механикой работы статического типа dynamic. C т.з. компилятора они могут не отличаться. Для какого-нибудь похапе это все zvalue.
DG>по твоему определению получается что различных типов в скриптах вообще нет.
Есть один — dynamic. Но я согласен, это не единственный и возможно не самый лучший подход к определению.
если брать типы вообще, а не только внутри какого-то одного языка, то одна из задач типа — определить как данные хранятся в памяти.
можно, например, вспомнить чем тип BSTR отличается от типа WCHAR* — и то, и другое unicode строка, но вот хранение в памяти разное.
с информационной точки зрения тип задает следующие виды информации:
1. фиксирование кол-ва поддерживаемых вариантов
2. описание способа хранения в памяти (в тексте и т.д.)
3. набор поддерживаемых операций
4. информацию об отличии типов друг от друга (обычно это отражает ту информацию, которая остается во внешнем мире за границей программы)
short/int/long/big-integer — отличаются по первому пункту
int/network-int, WCHAR*/BSTR, list/array — отличаются по второму пункту
bool/enum{on/off} — отличаются по третьему пункту
enum{on/off}, enum{много/мало} — отличаются по четвертому пункту
VE>>Какая связь типов с памятью?
DG>если брать типы вообще, а не только внутри какого-то одного языка, то одна из задач типа — определить как данные хранятся в памяти. DG>можно, например, вспомнить чем тип BSTR отличается от типа WCHAR* — и то, и другое unicode строка, но вот хранение в памяти разное.
Взять, например int и unsigned int.
И хранятся одинаково, и кол-во вариантов одинаковое.
Отличие у них только в операции, выбираемой по умолчанию при перегрузке. Т.е. x < y выберет либо unsigned_less либо signed_less в зависимости от.
Можно вообще все unsigned int на int поменять (и наоборот), только придётся ручками указывать, какой именно мы less хотим.
Т.е. они по сути оба strong typedef на одно и то же. Собственно, можно как раз про strong typedef и вспомнить. Неужто они определяет способ хранения в памяти, вводя новый тип?
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".
во-первых: это определение type system, а не type, во-вторых: это ужасное определение: определение должно определять понятие через более простые, а в данном случае — определение элементарного понятия "type system" идет через такиие неопределяемые понятия как: syntactic, framework, classifying, phrases, kind, compute, according.
можно получить строгое формализованное определение всех перечисленных понятий?
DG>>тип int от string в скриптах отличается? каким образом?
DM>Механикой работы статического типа dynamic. C т.з. компилятора они могут не отличаться. Для какого-нибудь похапе это все
zvalue.
т.е. весь мир сужен только до задач решаемых компилятором? почему и зачем?.
с точки зрения интерпретатора типы int и string отличаются? например, с точки зрения освобождения памяти? и с точки зрения вызова правильной версии полиморфной операции + (которая по разному складывает числа и строки).
я правильно понимаю, что ты считаешь, что в c# типы есть, а когда ровно с теми же .net-данными(классами, числами и т.д.) работает ironpython, то все типы сразу куда пропадают?
DM> Для какого-нибудь похапе это все zvalue.
так это однородный тип? или у него есть явные подтипы? например: zvalue-number, zvalue-string, zvalue-dictionary
DG>>по твоему определению получается что различных типов в скриптах вообще нет.
DM>Есть один — dynamic. Но я согласен, это не единственный и возможно не самый лучший подход к определению.
ps
даже в вики такие определения:
1) Тип (от греч. τυπος — отпечаток, форма, образец) — единица расчленения изучаемой реальности в типологии
2) Тип данных определяет множество значений, набор операций[1], которые можно применять к таким значениям, и, возможно, способ реализации хранения значений и выполнения операций. Любые данные, которыми оперируют программы, относятся к определённым типам.
3) Тип (сорт) — относительно устойчивая и независимая совокупность элементов, которую можно выделить во всём рассматриваемом множестве (предметной области).[2]
4) In computer programming, a data type is a classification identifying one of various types of data, such as floating-point, integer, or Boolean, that determines the possible values for that type; the operations that can be done on values of that type; the meaning of the data; and the way values of that type can be stored
pps
Языки с неявным определением типов. Казалось бы, BASIC является примером языка без типов. Однако это строго типизированый язык: в нём различаются строковые типы (добавляется символ $), массивы (добавляется []) и числовые типы (ничего не добавляется).
VE>>>Какая связь типов с памятью?
DG>>если брать типы вообще, а не только внутри какого-то одного языка, то одна из задач типа — определить как данные хранятся в памяти. DG>>можно, например, вспомнить чем тип BSTR отличается от типа WCHAR* — и то, и другое unicode строка, но вот хранение в памяти разное.
VE>Взять, например int и unsigned int. VE>И хранятся одинаково, и кол-во вариантов одинаковое.
хранятся они по разному — у одного первый бит отвечает за знак, у другого знак подразумевается не явно.
как минимум это проверяется через операцию конвертации в строковое представление.
более формально: функция которая выводит тип int/uint правильно на экран (в строковое представление) должна принимать минимум 4байта+1бит информации. 4 байта определяют кол-во вариантов самого типа, а доп. 1 бит является идентификатором типа.
или другими словами, невозможно написать корректную функцию переводящую int/uint из одного способа хранения в другой (из байтового представления в строковое), если она принимает на вход не больше 4 байт информации.
для строгости стоит рассмотреть наборы операций:
int/uint хранятся одинаково с точки зрения unchecked операций +/-/*/'/' (можно написать функцию, которая корректно обработает тип int/uint и принимающую только 4 байта информации), но с точки зрения checked-операций, они уже хранятся по разному (необходим +1бит информации для того, чтобы отличить одно от другого)
VE>Отличие у них только в операции, выбираемой по умолчанию при перегрузке. Т.е. x < y выберет либо unsigned_less либо signed_less в зависимости от.
раз необходимо делать выбор правильной версии операции — это уже означает, что есть что-то разное (или разная семантика операции, или разная семантика хранения в памяти)
VE>Можно вообще все unsigned int на int поменять (и наоборот), только придётся ручками указывать, какой именно мы less хотим. VE>Т.е. они по сути оба strong typedef на одно и то же. Собственно, можно как раз про strong typedef и вспомнить. Неужто они определяет способ хранения в памяти, вводя новый тип?
по видимому ты хотел спросить: определяет ли typedef новый(отличный от предыдущего) способ хранения в памяти, вводя новый тип?
нет, "typedef x type-expr;" не задает обычно нового способа хранения, но при этом она определяет каким образом x будет хранится в памяти — эта информация берется из типа указанного в type-expr.
Здравствуйте, DarkGray, Вы писали:
VE>>>>Какая связь типов с памятью?
DG>>>если брать типы вообще, а не только внутри какого-то одного языка, то одна из задач типа — определить как данные хранятся в памяти. DG>>>можно, например, вспомнить чем тип BSTR отличается от типа WCHAR* — и то, и другое unicode строка, но вот хранение в памяти разное.
VE>>Взять, например int и unsigned int. VE>>И хранятся одинаково, и кол-во вариантов одинаковое.
DG>хранятся они по разному — у одного первый бит отвечает за знак, у другого знак подразумевается не явно.
Правильно ли я понимаю, что можно глядя на память понять, int там или unsigned int?
DG>для строгости стоит рассмотреть наборы операций: DG>int/uint хранятся одинаково с точки зрения unchecked операций +/-/*/'/' (можно написать функцию, которая корректно обработает тип int/uint и принимающую только 4 байта информации), но с точки зрения checked-операций, они уже хранятся по разному (необходим +1бит информации для того, чтобы отличить одно от другого)
Ага! Т.е. одинаковость хранения не от типа зависит, да? Вот и я о чём.
DG>раз необходимо делать выбор правильной версии операции — это уже означает, что есть что-то разное (или разная семантика операции, или разная семантика хранения в памяти)
Операции разные, очевидно. Причём можно обе применять. Сам по себе int или unsigned int не определяет, какое там число (ну только "на словах"). А вот операция сравнения уже несёт такую информацию, так как определена по-разному в зависимости от интерпретации того, что ей передают.
DG>по видимому ты хотел спросить: определяет ли typedef новый(отличный от предыдущего) способ хранения в памяти, вводя новый тип? DG>нет, "typedef x type-expr;" не задает обычно нового способа хранения, но при этом она определяет каким образом x будет хранится в памяти — эта информация берется из типа указанного в type-expr.
По-моему, вы ставите лошадь впереди телеги. Тип несёт информацию о множестве допустимых значений, а как это хранить, выбирает реализация. Разумеется, вводя новые типы, вы основываете их на уже имеющихся, и реализация имеет механизм, позволяющий ей выбрать способ хранения нового типа. Но это не отновится к свойствам типизации как таковой, а побочный эффект от того, что тип накладывает ограничения.
Мы можем с успехом написать такую реализацию, которая будет strong typedef хранить иначе, например, xor'я каждый байт каким-нибудь ключом (сгенерированным от имени typedef'а). Типизация останется абсолютно той же, а детали реализации останутся лишь деталями реализации. То, что эти детали используют информацию о типах и типы таким образом косвенно влияют на способ хранения — дело десятое.
В общем-то, мы уже далеко отошли от изначальной темы. Речь шла о том, что типизация будет динамическая, если происходит выбор типа и реинтерпретация памяти.
Я уточнил, что
1. банальное сравнение с константой есть выбор типа
2. выбор типа не означает реинтерпретацию памяти
Таким образом нам либо придётся согласиться, что if (x == 0) — это динамическая типизация, либо что выбор типа надо рассматривать в рамках той системы, о которой идёт речь (тогда в Си, разумеется, if (x == 0) не выбирает никакого типа, так как в Си не существует типа (x:int){x=0})
Но тогда и в Haskell при выборе АлгТД не происходит выбора типа, так как тип один и остаётся тем же, а реинтерпретации памяти вполне может и не быть, например в случае Bool или Either Int 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
Ну так речь шла о типизации, а не о типе.
DG>, во-вторых: это ужасное определение: определение должно определять понятие через более простые, а в данном случае — определение элементарного понятия "type system" идет через такиие неопределяемые понятия как: syntactic, framework, classifying, phrases, kind, compute, according. DG>можно получить строгое формализованное определение всех перечисленных понятий?
Можно. А нужно?
DG>img
Я недавно видел отличное определение: натуральные числа — это объект категории Пеано, представляющий singleton функтор I. Или просто инициальный объект в категории Пеано.
DG>>>тип int от string в скриптах отличается? каким образом? DM>>Механикой работы статического типа dynamic. C т.з. компилятора они могут не отличаться. Для какого-нибудь похапе это все zvalue. DG>т.е. весь мир сужен только до задач решаемых компилятором? почему и зачем?
Нет. Потому и затем, что типизация особенно актуальна именно там.
DG>с точки зрения интерпретатора типы int и string отличаются? например, с точки зрения освобождения памяти?
Не более, чем разные значения одного типа. Собственно, про параллель с алгебраиками тут уже много писали.
DG>я правильно понимаю, что ты считаешь, что в c# типы есть, а когда ровно с теми же .net-данными(классами, числами и т.д.) работает ironpython, то все типы сразу куда пропадают?
В разных язаках разные системы типов, разумеется. C#, Python и MSIL — три разных языка с разными системами типов.
DM>> Для какого-нибудь похапе это все zvalue. DG>так это однородный тип? или у него есть явные подтипы? например: zvalue-number, zvalue-string, zvalue-dictionary
Это одна структура в Си, содержащая внутри union. Она трактуется по-разному в зависимости от значения определенного поля.
DG>даже в вики такие определения:
Я и говорю, подходов к определению может быть много.
Здравствуйте, DarkGray, Вы писали:
FR>>Если брать OCaml, в котором примерно похожий на Хаскель ПМ, реализуется очень эффективно,
DG>как при этом раскроется: DG>
let dummy2 items = Array.map dummy_id |> Array.fold_left (+) 0 in
dummy2 [|Int 1; Int 2; Int 3|];
dummy2 [|String "1"; String "2"; String "3" |]
Причем никто не мешает вызвать
dummy2 [|String "1"; Int 2; Float 3.0 |]
Это ведь массив значений одного типа test.
Никакой специализации компилятор не сделает, на эффективность dummy_id твой код не повлияет, там внутри по-прежнему будет по 2 if'a.
DG>как только появляется смешивание ad-hoc полиморфизма с параметрическим, то вся эффективность пропадает
