но щас визу пулей делают

греческую делают за 1.5 дня

мне греческую сделают если у меня нету туда поездки?

у меня ближайшая на территорию испании планируется

ну тут как

теоретически, к ним бы надо заехать. практически - кто его знает, что будет, если не заехать

им авиабилеты не нужны для визы. нужна бронь отеля

т.е. в общем-то это вариант взять испанскую и если получится - заехать в munich

если регистрация открыта конечно

конечно

и наоборот тоже работает

мы как раз ездили в испанию с испанской визой, но через германию

вот я так хочу, наверное

блин было бы оно на 2 дня раньше вообще бы идеально было

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

а всё-таки хаскель даёт бесценный опыт, даже для других языков... сейчас сижу и пишу шаблонный фолд для дерева геометрических фигур, это на nvcc++ 🤠

хотя бы этим и ценен : ]

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

страдать это да

особенно хорошо потом страдается в си

в попытках эмулировать hof

кортежи

и что-то типизировать путем обертывания в структуры

я страдаю от отсутствия паттерн-матчинга

сейчас фигуры у меня помечены enum class, но это убого

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

Именно, что страдать :(

хотя уже несколько раз натыкался на Mach7, но как-то не хочется его тыкать

Хм, если представить сумму типов как множество пар, где первый элемент - метка, а второй - значение (типа (Left, 10), (Right, "hello")), то это вполне себе зависимый тип, где тип второго элемента пары зависит от значения первого, он же сигма. А такое представление я взял не из головы, как минимум так выглядит размеченая сумма на вики

Почему это логичная? Знак '=>' это логический вывод, где список классов играет роль контекста, а тип -- вывода. Конструкция Г_1 |- Г_2 |- A бессмысленна

Знак => это имплиситный аргумент в функцию, неявный аналог ->

Или это логическая импликация

В обоих случаях каррирование смысл имеет

у меня ближайшая на территорию испании планируется

О! Можно локальный "митап" 🍻 замутить если Мадрид запланирован и время/желание будет 🙂

Контекст логического выражения это, конечно, в определённом смысле имписитная логическая импликация, но каррировать тем менее выводимость нельзя :)

@antontrunov я на острова испанские, так что на континентальной части не буду : /

как нить в другой раз = )

ок =)

Контекст логического выражения это, конечно, в определённом смысле имписитная логическая импликация, но каррировать тем менее выводимость нельзя :)

Ты откуда-то взял, что => это |-

я вообще ничего не могу сказать про |-, а про => вот вполне

1 способ смотреть на => в том, что он как ->, только аргумент неявный

2 способ в том, что это логическая импликация

в обоих случаях каррирование имеет место

Что такое "неявный аргумент"? Это какое-то неформальное понятие

Это значит, что аргумент будет при вызове функции составлен механизмом instance search

Второе неверно, потому что -> это логическая импликация, а => соединяет разнородные сущности

то есть будет поиск словаря

Второе неверно, потому что -> это логическая импликация, а => соединяет разнородные сущности

=> соединяет одинаковые сущности: тип слева, тип справа

особенно хорошо потом страдается в си

а мог бы просто на раст перейти

нельзя просто взять и перейти на раст:)

=> соединяет одинаковые сущности: тип слева, тип справа

Не тип, а констрейнт

если мы не про домашние проекты говорим

Не тип, а констрейнт

А разница?

Ну типа констрейнт имеет одни свойства, тип — другие

Constraint и Type эквивалентны, у меня есть инъекции в обе стороны

Был даже пропозал сделать Constraint ~ Type, потому что в GHC Core это так

Разных свойств там только в том, кто может слева от => оказаться

нельзя просто взять и перейти на раст:)

можно и нужно

Фантомное различие

можно и нужно

делись историей успеха

нет проектов на си

можно и нужно

Он не ленивый

Он не ленивый

си тоже

но в расте есть встроенные ленивые структуры

раст слишком молод

его нет под нестандартные платформы, например

какая тебе нужна?

кластеры, gpu

Раст > си

кластеры, gpu

конкретно

давай для начала cuda

это конкретно?

Constraint и Type эквивалентны, у меня есть инъекции в обе стороны

Не очень понятно как зафигичать аналог equality constraint в Type

давай для начала cuda

есть Arrayfire

давай для начала cuda

А есть у хаскеля?

Эм-м-м, Refl

это конкретно?

Ты не куде много чего делаешь?) Или ты каждый день бек рей трейсинг в риал тайм генеришь?)

Не очень понятно как зафигичать аналог equality constraint в Type

https://hackage.haskell.org/package/base-4.10.0.0/docs/Data-Type-Equality.html#t::-126-:

А есть у хаскеля?

тут чел предложил перейти с си на раст, а не с хаскеля на раст

плюсы есть под каждую табуретку вот

rustc может в PTX компилировать