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

конечно

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

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

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

блин было бы оно на 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 компилировать

особенно если не тащить stl или че там выкидывают

А в целом любой констрейнт можно в Type перенести, есть Dict :: Constraint -> Type https://hackage.haskell.org/package/constraints-0.9.1/docs/Data-Constraint.html#t:Dict

особенно если не тащить stl или че там выкидывают

давай следующую платформу

Раз все компилится в жс, го все на жс)))

которая тебе нужна

давай следующую платформу

сейчас я почитаю про твой Arrayfire

nvptx64-nvidia-cuda

я правильно понял, что это либа НАД кудой? с биндингами в любой удобный язык

короче батарейки для раста/etc на куде

как NumPy или SciPy для питона

очень похоже на то

в таком случае, мне нужно, разумеется, не это

nvptx64-nvidia-cuda

^

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

^^^^

nvptx64-nvidia-cuda

почитал. ну начинания хорошие, но пока это выглядит несерьезно. собственно разбирал вот этот пример https://github.com/japaric/nvptx/blob/master/examples/add.rs заявлено, что это сложение двух векторов на GPU претензий собственно две, но обе принципиальные 1. как я вижу, все операции, связанные с GPU, находятся в блоке unsafe. Но зачем тогда раст? 2. так и не понял, где они определяют сам kernel add. По всей видимости, берут из кишок библиотеки, причём загружают функцию по её имени через строку (лол)? в таком случае этот пример ничего не демонстрирует, т.к. мне интересно написание кода kernel-функций и device-функций на раст, а не эти игрульки.

если я чего-т не понял, то пожалуйста

почитал. ну начинания хорошие, но пока это выглядит несерьезно. собственно разбирал вот этот пример https://github.com/japaric/nvptx/blob/master/examples/add.rs заявлено, что это сложение двух векторов на GPU претензий собственно две, но обе принципиальные 1. как я вижу, все операции, связанные с GPU, находятся в блоке unsafe. Но зачем тогда раст? 2. так и не понял, где они определяют сам kernel add. По всей видимости, берут из кишок библиотеки, причём загружают функцию по её имени через строку (лол)? в таком случае этот пример ничего не демонстрирует, т.к. мне интересно написание кода kernel-функций и device-функций на раст, а не эти игрульки.

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

насчет второго не шарю

насчет второго не шарю

ну как я изначально и предположил, они просто наклепали кучу полезных для линейки/диплёрнинга/обработки сигналов/etc функций и дали к ним доступ из раста (с хоста). Это называется библиотека. Такие есть под любой язык, вот прям совсем под любой, и даже под сами плюсы. Хотя фича компиляции в ptx прикольная, не спорю. Но поддержкой куды растом это назвать сложно. В таком смысле и питон поддерживает куду... Моя же работа заключается в написании таких библиотек. Так что, увы, только б-гмерзкие плюсы. Но за ссылочку спасибо.

*всё, прекращаю офтоп

Да нет

ты смешал первую и вторую либу что ли

Продолжай

ты смешал первую и вторую либу что ли

я не очень понял вопрос... Но в их репе я не нашёл, как писать кернелы и девайсы на расте, везде только рулёж уже написанными (кем и на чём?) кернелами с хоста

ну твое первое сообщение про arrayfire а ответ про nvptx