мнезия, конечно спорный момент

Почему?

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

??

Нет type erasure - нет parametric polymorphism. Кому-то это неважно (жава), кто-то на это рассчитывает (хаскель, скала, идрис)

Scala полагается на type erasure в том смысле, что в некоторых местах из-за этого самого type erasure приходится городить кривые костыли, которых без затирания типов городить было бы не нужно.

Например?

Эх, Шарик, нифига ты не понял, учи английский. Там всего лишь сахар для колбасы вроде

def handleObject(animal):
	if animal is Dog:
		animal.pet()
	elif animal is Cat:
		animal.kick()
	elif ...

Нет type erasure - нет parametric polymorphism.

Наоборот. Есть type erasure - нету parametric polymorphism. Потому что нельзя написать (forall a.a -> ...) -> .... (по сути из всех существующих ЯП, такую функцию потенциально можно написать только в net-языках). Но если ограничиться first-rank, то все в порядке, конечно.

Например когда делается case по какому-нибудь List[Int], очевидно же.

Што.

См. хаскель: type erasure есть, rank-n polymorphism есть.

Зачем?

Все примеры isInstanceOf, которые я видел, ограничиваются потугами динамических петушков написать что-то на скале и трудами дебилов, которые не могут в sum-types.

Есть какой-нибудь нормальный юзкейс?

См. хаскель: type erasure есть, rank-n polymorphism есть.

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

Так что де-факто никакого type erasure в хачкиле нету. Но при этом и нормальной реализации параметрического полиморфизма тоже нету - костыль он и в африке костыль.

Понятно.

Есть какой-нибудь нормальный юзкейс?

Перехват исключений, например.

которые не могут в sum-types.

sum-types закрыты, по-этому не нужны.

Алсо, вообще любую человеческую интроспекцию type erasurew убивает. Так что вопрос сводится к «какие есть юзкейсы у интроспекции».

А в той же жабе все все вообще предельно хуево - даже инстанс класса-аргумента получить нельзя. Или массив с инстансом генерика создать. Я уж не говорю про врапперы для примитивных типов.

Перехват исключений

Можно обойтись экзистенциальным типом.

sum-types закрыты, по-этому не нужны.

Ясно.

Можно обойтись экзистенциальным типом.

В каком смысле? Я про:

try {} catch {case x: MyYobaExtension[Huy] => ..., case x: MyYobaExtenstion[Pizda] => ...}

из-зав type erasure до пизды дело никогда не дойдет.

Ясно.

Хотя, конечно, если перед нами убогий недоязык без сабтайпинга, то тогда нужны. На безрыбье и рак - рыба.

try {} catch {case x: MyYobaExtension[Huy] => ..., case x: MyYobaExtenstion[Pizda] => ...}

С такой трудной задачей даже убогий недоязык с type erasure справиться может: https://gist.github.com/anonymous/6511606

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

Сори, надо наверное пару экстеншенов включить, но компилятор должен подсказать какие.

С такой трудной задачей даже убогий недоязык с type erasure справиться может:

MyYobaException a deriving (Show, Typeable)

Слишком толсто. Какой, блять, erasure, если у тебя Typeable стоит? Собственно, в скалке тоже так же и делают кейзы по какому-нибудь List[Int] - добавляют typeable-style костылем информацию о типе руками.

Все еще непонятно, зачем ломать параметрический полиморфизм

Не знаю. А кто ломает? Я о починке говорю.

что вполне реализуется на экзистенциальных типах.

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

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

Какой, блять, erasure, если у тебя Typeable стоит?

Все типы стерты

Так у тебя и не будет никаких екзистенциальных типов, если есть erasure.

Што.

А кто ломает?

Возможность достать тип ломает. Если (a -> a) так-то id, а если a :: Int, то умножает аргумент на 2, нахрен такой полиморфизм нужен?

По-этому в хаскеле и слеплен костыль с неявной передачей тайпкласса,

Куда уж явнее (exists a. Exception a => ...) ?

Все типы стерты

Ты совсем тупой? Typeable как раз добавляет типы. Каким образом у тебя будет typeof работать, если во время рантайма типы стерты, а во время компиляции - неизвестны?

Што.

Если нет информации о типе в рантайме, то нельзя вызвать нужный инстанс тайпкласса, если он неизвестен в компайлтайме. Для rank-2 полиморфной функции (то есть для «внутренности» экзистенциального типа) в компайлтайме нужный инстанс неизвестен. В хачкиле эта проблема решается за счет того, что информация о типе (ссылка на таблицу виртуальных методов) тянется в виде неявного аргумента через все функциональные аппликации.

Возможность достать тип ломает.

Где ломает-то? ТЫ пример можешь привести?

Если (a -> a) так-то id, а если a :: Int, то умножает аргумент на 2

И в чем проблема? Где что сломано?

нахрен такой полиморфизм нужен?

Какой «такой»? Обычный полиморфизм.

Куда уж явнее (exists a. Exception a => ...) ?

Ты вообще понимаешь о чем речь? Вот у тебя есть тайпкласс, у него есть какой-то метод (ну например fmap у функтора), вот этот твой fmap принимает не только функцию a -> b с каким-то функтором, но еще и туда неявно передается ссылка на таблицу виртуальных методов. Так же как this в ООП языках. Только _совсем_ неявно (с this в ООП языках можно работать по крайней мере внутри).

tfr

Ты совсем тупой?

Допустим.

Typeable как раз добавляет типы

Нет. (forall a. Typeable a => ...) говорит о том, что с типом a можно работать через интерфейс Typeable, типы нигде не появляются, внутри так или иначе unsafeCoerce (с более или менее безопасным интерфейсом, пока инстанс Typeable не кривой).

ТЫ пример можешь привести?

Любая free теорема. Вот тебе примеров сколько хватит сил: http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi

И в чем проблема? Где что сломано?

Я рассчитываю, что функция с типом (a -> a) не изменяет аргумент, со сломанным полиморфизмом никаких гарантий нет. Зачем нужен полиморфизм без гарантий?

Ты вообще понимаешь о чем речь?

Да. Реализация может быть любой, разговор о семантике. Если правильная семантика позволяет определенную оптимизацию - отлично.

говорит о том, что с типом a можно работать через интерфейс Typeable, типы нигде не появляются

Для особо одаренных - Typeable как раз и подставляет типы в рантайме.

В языке без затирания просто все типы по дефолту реализуют Typeable.

Я рассчитываю, что функция с типом (a -> a) не изменяет аргумент

А с чего ты так расчитываешь? Почему ей нельзя изменять аргумент?

Любая free теорема.

Они не ломаются.

Зачем нужен полиморфизм без гарантий?

За тем же, зачем и полиморфизм с гарантиями. Все юзкейсы сохраняются. Алсо, тебя не смущает, что ad-hoc полиморфная функция для одного инстанса тайпкласса делает одно, а для другого - совсем другое?

Реализация может быть любой, разговор о семантике

Ну и я про семантику. По факту хаскель не затирает типы, т.к. если все типы затереть, то нельзя вызвать нужный инстанс для ранк-2 полиморфной ф-и.

Если правильная семантика позволяет определенную оптимизацию - отлично.

Шел 2013 год, хачкибляди пытались сэкономить на тайптаге... или я тебя не так понял? '

Typeable как раз и подставляет типы в рантайме.

??? Typeable - это библиотечная обертка над unsafeCoerce, ее и в стандарте-то нет.

В языке без затирания просто все типы по дефолту реализуют Typeable.

GHC 7.8 стирает типы, но при этом они все реализуют Typeable (с экстеншеном). Как так вышло?

А с чего ты так расчитываешь?

С того, что мне нравится по типу функции опеределять, чего она делать точно не может.

тебя не смущает, что ad-hoc полиморфная функция для одного инстанса тайпкласса делает одно, а для другого - совсем другое?

У них это в типе написано; против (DoubleIfInt a => a -> a) я ничего не имею.

Они не ломаются.

Конечно не ломаются

Guest79457> @free f :: a -> a
lambdabot> g . f = f . g

В гипотетическом хаскиле:

f :: a -> a
f (x :: Int) = 2 * x
f x = x

g :: Int -> Int
g x = x + 5

-- (f . g) 4 = 18
-- (g . f) 4 = 13

По факту хаскель не затирает типы

Если бы не затирал, то тип можно было бы достать.

??? Typeable - это библиотечная обертка над unsafeCoerce, ее и в стандарте-то нет.

Какая разница есть она в стандарте или нет? Факто в том, что это специальный костыль, который эмулирует отсутствие type erasure.

В языках без type erasure просто у каждого типа по дефолту есть инстанс Typeable.

GHC 7.8 стирает типы

GHC стирает типы, но не полностью (таблица тайпклассов остается)

но при этом они все реализуют Typeable (с экстеншеном).

И вот из-за type erasure приходится городить специальный костыль, благодаря которому делают вид, что type erasure нет. По-моему лучшего аргумента в пользу того, что затирание типов - зло, не придумаешь.

С того, что мне нравится по типу функции опеределять, чего она делать точно не может.

Ну определяй, ради бога.

У них это в типе написано; против (DoubleIfInt a => a -> a) я ничего не имею.

Так с чего ты взял, что a -> a - это только id? Параметрический полиморфизм сам по себе вообще беден, ничего полезного с ним делать нельзя. Уже приходится добавлять ad-hoc (тайпклассы теже), чтобы это можно было нормально использовать. И ad-hoc полиморфизм _уже_ все ломает - параметрически полиморфная функция - это тотальная функция из типов в термы, ad-hoc полиморфная - уже нетотальная. Полиморфная со стиранием - тотальная, но задается более свободно.

Если бы не затирал, то тип можно было бы достать.

Ты пойми простую вещь - информации о типах _много_. И GHC затирает, но не всю. Можно назвать это частичным затиранием.

Конечно не ломаются

И где что поломалось? Вообще с чего ты взял, что полиморфная функция должна удовлетворять твоим мокрым мечтаниям?

И вот из-за type erasure приходится городить специальный костыль,

Тогда любая библиотека - специальный костыль.

GHC стирает типы, но не полностью (таблица тайпклассов остается)

Ок, как внутри rank-2 (forall a. a -> ...) достать таблицу тайпклассов для a?

Так с чего ты взял, что a -> a - это только id?

Из типа. Еще undefined и const undefined.

Параметрический полиморфизм сам по себе вообще беден ничего полезного с ним делать нельзя.

??? Наоборот, из полиморфного типа можно извлечь гораздо больше информации, чем из мономорфного. Из ad-hoc полиморфного меньше, чем из параметрически полиморфного, но тем не менее (особенно, если автор не дебил и прочитал, каким законам его имплементация должна удовлетворять, ну или хотя бы описал, как именно не удовлетворяет).

Ad-hoc полиморфизм ломает теоремы (очевидно), но это видно в типе.

Вообще с чего ты взял, что полиморфная функция должна удовлетворять твоим мокрым мечтаниям?

С того, что программировать проще, когда не нужно отвлекаться на детали реализации каждого комбинатора, когда выполняются законы для простейших операций (ассоциативность, дистрибутивность, etc). Чем меньше нужно вникать в детали и больше законов выполняется, тем проще. Че как маленький.

Тогда любая библиотека - специальный костыль.

Любая библиотека, которая пытается криво исправить недочеты языка - костыль, все верно.

Ок, как внутри rank-2 (forall a. a -> ...) достать таблицу тайпклассов для a?

Она там есть и достать ее можно, так что это вопрос наличия reflection api - который затиранию типов ортогонален.

Из типа.

Что из типа? С чего ты взял, что функция типа a->a должна быть только id?

??? Наоборот, из полиморфного типа можно извлечь гораздо больше информации, чем из мономорфного.

При чем тут извлечение информации? Я говорю о полезной работе. Параметрический полиморфизм сам по себе не дает практически ни одного полезного юзкейса.

Ad-hoc полиморфизм ломает теоремы (очевидно), но это видно в типе.

Ну и ради бога, пусть ломает, пусть этого не видно - что в этом плохого? Все равно эти теоремы никому не нужны на практике.

С того, что программировать проще, когда не нужно отвлекаться на детали реализации каждого комбинатора

Не отвлекайся, кто тебя заставляет?

Чем меньше нужно вникать в детали и больше законов выполняется, тем проще.

При чем тут эти законы, если на практике они просто НЕ НУЖНЫ? А ни на что кроме ненужных законов твоя хуйня не влияет.

Зато человеческий полиморфизм и рефлексия делают возможными нужные на практике вещи, в отличии от твоих никому не всравшихся free theorems.

Любая библиотека, которая пытается криво исправить недочеты языка

Typeable не пытается исправить никакие недочеты языка. Это тулза, использующаяся в syb-style библиотеках, имплементации эксепшенов, etc. Здравый смысл подсказывает, что если X можно написать в виде библиотеки, то X не нужно хардкодить в язык.

Она там есть и достать ее можно

Шаришь.

С чего ты взял, что функция типа a->a должна быть только id?

Вообще говоря, это не я придумал: http://en.wikipedia.org/wiki/Curry–Howard_correspondence

Все равно эти теоремы никому не нужны на практике.
При чем тут эти законы, если на практике они просто НЕ НУЖНЫ?

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

Зато человеческий полиморфизм и рефлексия делают возможными нужные на практике вещи

Правда, до сих пор ни одного примера не было.

Правда, до сих пор ни одного примера не было.

Ага, а то что потом в том же хаскеле делают специальные костыли для того чтобы было «типа без type erasure» было это не пример, лол?

Typeable не пытается исправить никакие недочеты языка.

Как раз и пытается. Причем вполне конкретный недочет - type erasure. если type erasure нету - то и typeable нахуй не нужен.

что если X можно написать в виде библиотеки

Так нельзя, по крайней мере полноценно. Вот в хаскеле костылем сделано.

Вообще говоря, это не я придумал:

Ты какой-то слишком трудный. Я еще раз задам вопрос - с чего ты взял, что функция с типом a->a должна быть id? Это только одна уебищная модель. Если в реальном мире модель оказывается неприменима - то ее выкидывают нахуй. И вот только в CS пытаются переделать реальный мир.

Ну, кому-то может и не нужны, только при чем тут нормальные языки?

При том. нормлаьный язык - это при разработке которого обращают внимание на нужные фичи и кладут хуй на ненужные. Нормальная поддержка рефлексии нужна. free theorems - не нужны.

Кстати даже о free theorems - никакого другого примера кроме id ты так и не привел.

Множеству людей, например, очень нравится легкость рефакторинга в Хаскеле, большая часть из которого возможна благодаря законам/теоремам.

Так ты приведешь хоть один нормальный пример когда у тебя что-то там нарушилось? Имеется ввиду практически целесообразный пример. Примеры с id на разный лад к ним, естественно, не относятся, так как в реальности они никогда ни на что не повлияют.

если type erasure нету - то и typeable нахуй не нужен.

Да в общем-то, если type erasure нету, то и язык не нужен, че на Typeable останавливаться.

нельзя, по крайней мере полноценно.

Ну давай уже «практичный» пример из «реального мира», где нужно «полноценно», не томи.

с чего ты взял, что функция с типом a->a должна быть id?

Здравый смысл. Это, кстати, не CS, а логика.

Нормальная поддержка рефлексии нужна. free theorems - не нужны.

Ты все понял наоборот, к сожалению.

Так ты приведешь хоть один нормальный пример когда у тебя что-то там нарушилось?

Ну, если id ты уже освоил, то можно подняться на уровень выше.

Если поверить в fmap id = id (1 functor law), то «тривиальный» рефакторинг fmap f . fmap g = fmap (f . g) (2 functor law) - free theorem. Пример такой имплементации fmap в языке со сломанным полиморфизмом, что первый закон выполняется, а второй - нет, оставлю в качестве домашнего задания.

Если законы нарушены, полиморфизм не работает, то вместо рефакторинга придется заниматься вниканием в реализацию.

Да в общем-то, если type erasure нету, то и язык не нужен, че на Typeable останавливаться.

Что за хуйню ты несешь?

Ну давай уже «практичный» пример из «реального мира», где нужно «полноценно», не томи.

http://research.microsoft.com/en-us/um/people/simonpj/papers/hmap/

Здравый смысл. Это, кстати, не CS, а логика.

Ты читать не умеешь? Еще раз (уже даже со счета сбился, который раз) повторяю свой вопрос: «с чего ты взял, что функция с типом a -> a должна быть id?».

Если поверить в fmap id = id

При чем тут id? Я попросил реальный пример - то есть тот, который не сводится к id.

то «тривиальный» рефакторинг fmap f . fmap g = fmap (f . g) (2 functor law) - free theorem.

Замечательно, теперь тебе домашнее задание, объяснить, почему:

1. отсутствие затирания типов не ломает указанный закон

2. как его сломать при наличии type erasure, и почему он не ломается в хаскеле (нет, не из-за type erasure).

Если законы нарушены, полиморфизм не работает

Ты как-то сразу проскочил всю цепочку доказательства. С чего вдруг из-за того, что законы нарушены следует, что полиморфизм не работает? Практика показывает, что все прекрасно работает.

то вместо рефакторинга придется заниматься вниканием в реализацию.

Пример можно конкретный, где вместо рефакторинга приходится вникать в реализацию?