расскажи мне, как связаны типы A и B, каким образом они изоморфны

и прими аксиому унивалентности всем сердцем

потом мы это легко свяжем в доказательный код

сделай sealed trait определи все варианты

гм, ну пусть будет sealed trait A trait B extends A trait C extends A def foo(b: B): C = ???

а asInstanceOf - это неполная функция

она ничего не доказывает

гм, ну пусть будет sealed trait A trait B extends A trait C extends A def foo(b: B): C = ???

ты совсем не понимаешь, что такое замкнутое семейство, да?

она ничего не доказывает

ну как же на уровне тех же имплиситов доказывает оно свалится в рантайме, но проверку пройдет

ну как же на уровне тех же имплиситов доказывает оно свалится в рантайме, но проверку пройдет

если она может свалится в рантайме, это значит, что твоё доказательство - мусор

ты совсем не понимаешь, что такое замкнутое семейство, да?

не хочу гуглить сейчас напиши тогда сниппет)

не хочу гуглить сейчас напиши тогда сниппет)

сниппет чего? доказательства изоморфности типов в твоей голове?

извини, забыл майнд-контроллер в другом телеграмме

если она может свалится в рантайме, это значит, что твоё доказательство - мусор

очень строгое утверждение может быть, это у меня хак типа тех, что rudogma использует для правки мозгов идее, но _случайно_ провытал какую-то ветку — код будет компилироваться и даже иногда работать

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

очень строгое утверждение может быть, это у меня хак типа тех, что rudogma использует для правки мозгов идее, но _случайно_ провытал какую-то ветку — код будет компилироваться и даже иногда работать

Сабин и все остальные используют asInstanceOf не как доказательную базу, а как вправление мозгов скаловскому компилятору, система типов которого пока слабовата

сниппет чего? доказательства изоморфности типов в твоей голове?

в котором патматом доказыватся сводимость несводимых типов

в котором патматом доказыватся сводимость несводимых типов

Я перестаю тебя понимать. Твоё утверждение о паттерн-матчинге касалось какого-то конкретного случая, в котором доказывалось то, что вообще говоря неверно?

всегда считал, что именно по причине "универсального доказательства" null является жестким надругательством над системой типов (а каст из той же оперы, как я понимаю)

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

А ты, видимо, что-то другое...

ну я про то, что "сигнатура функции — теорема, а её реализация — доказательство"

я здесь прицепился к слову "универсальное" :)

ну я про то, что "сигнатура функции — теорема, а её реализация — доказательство"

Да вот для этого паттерн-матчинг хорошо подходит

патмат не является универсальным доказательстом чего угодно (в смысле, на уровне типов) и вообще там куча проверок "на дурака" в виде isInstanceOf

А вот для доказательства эквивалетности неэквивалентных типов - не очень хорошо

Как и что угодно другое

то, что патматом можно доказывать, я не спорю)

очень строгое утверждение может быть, это у меня хак типа тех, что rudogma использует для правки мозгов идее, но _случайно_ провытал какую-то ветку — код будет компилироваться и даже иногда работать

эм. я не использую хаки без доказательств) оно у меня не может свалится в рантайме)

я "обманываю" идею "честно" )

эм. я не использую хаки без доказательств) оно у меня не может свалится в рантайме)

ну я для примера :) вдруг кто-то другой попробует так же, но не все ветки докажет

Ок. я сагрился на спор, в котором мне нет места, я застёгиваю кобуру и ухожу

та просто недоопределенные понятия спора — о разном говорили самая популярная причина для неконструктивных дискуссий)

https://twitter.com/contrarivariant/status/883805540203102208

ну тоже не оч красиво выходит, хотелось бы как нить избежать asInstanceOf

кароч я пас, идею не вразумить

тем более что она впринципе права)

кароч я пас, идею не вразумить

я знаю решение

открываешь https://github.com/JetBrains/intellij-scala и фиксишь

Кул стори

Я как-то один раз открыл, с тех пор заикаюсь

Тут как бы идея то права

Она просит А а я ей пихаю какую то фигню

с чего она права то

Option... не может быть A ?

Там в каждом кейсе свой возвращаемый тип

То что дженерик стирается собственно и даёт этому компилиться как я понимаю

покажи целиком

Щас нет кода под рукой

То что дженерик стирается собственно и даёт этому компилиться как я понимаю

опачки. это как так. сначало же проверка типов идет) ты же не хочешь сказать, что тайп еражуре позволит скомпилиться такому коду val list:List[String] = List(1,2,3,4) )

Нуууу нет, не могу придумать логичного объяснения этому)

чему тайп еражуре способствует, так это компиляции вот такого val list2:List[String] = List(1,2,3).asInstanceOf[List[String]] и оно в рантайме не упадет

val list3:Set[String] = List(1,2,3).asInstanceOf[Set[String]] - а вот это упадет в рантайме, потому что топлевел тип не совпадает) List != Set

ппц все в скала плагине упорядочено через одно место)

ппц все в скала плагине упорядочено через одно место)

как будто жетбрейнсы когда-то отличались ох**тельной архитектурой и изяществом)

да я в шоке

проще взять и написать свои скала плагин)

точно, то ли дело эклипс!

мне интересно, насколько реально скала мета заюзать для скала плагина

Было пару дней назад в твиттере

мне интересно, насколько реально скала мета заюзать для скала плагина

там уже исопльзуется частично скаламета

частично

мне интересно, насколько реально скала мета заюзать для скала плагина

А так разве можно?

а я про выкинуть нахер все из идеи)

https://github.com/JetBrains/intellij-scala/tree/idea172.x/src

А так разве можно?

можно

ха

ERROR: S client not available

https://github.com/raulraja

коммитил)

можно

Но ведь у компилятора своё апи, а у меты своё

Но ведь у компилятора своё апи, а у меты своё

а у идеи свое, прикинь)

Ну так об этом и речь

Но ведь у компилятора своё апи, а у меты своё

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

а важно то, что скаламета - не выводит типы

Scala macros будет выводить

идее и не нужен вывод типов, у них свои механизм

хотя я хз, я ток смотрю этот код

решил собрать idea плагин, все повисло)

слава jb!

решил собрать idea плагин, все повисло)

не ты первый, не ты последний)

вы так плюётесь, ну не пользуйтесь тогда )

Да, атом всё умеет

Конечно шутка

Здесь все такие шутники

Надорвёшь живот

вы так плюётесь, ну не пользуйтесь тогда )

ну ты скажешь. если так рассуждать - придется и от семок отказаться)

ну ты скажешь. если так рассуждать - придется и от семок отказаться)

ну оно опен-сорс, платить за это не заставляют, не нравится - можно зайти улучшить

Kirill сегодня от семок отказаться, а завтра с кортов встать? ну уж нет)

Kirill иди попробуй улучшить, ага

в смысле? для вас сделали бесплатно с открытым исходным кодом, вы ноете

ну оно опен-сорс, платить за это не заставляют, не нравится - можно зайти улучшить

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

в смысле? для вас сделали бесплатно с открытым исходным кодом, вы ноете

наговнокодили ты хотел сказать

ну так не пользуйся, раз наговнокодили

да я итак в виме пишу)

ну так не пользуйся, раз наговнокодили

не нравится критика - не читай)

я и не автор чтобы не читать критику, критика-то здравая, есть за что, просто такая безапеляционность в отношении oss удивляет

запустил fast tests - уже полтора часа жду)