в stack.yaml только resolver

пакет причем Chris Done

@quetzal ^

мм?

если кому не лень

https://github.com/chrisdone/jl

попробуйте собрать у себя

может у меня что-то

нужно было тех кто защищал стек позвать

я позвал

а чего не jq?

я давно хотел jl попробовать, но не выпадала возможность

вот сейчас нужно

и засада

пойду за jq

@anpryl версия из гита у меня new-build-ом собралась

это надо новый кабал накатывать?

интересно до какого года он будет new

2025 ?

@anpryl я думаю тот что у тебя есть подойдет

скорее всего проблема в чем-то другом

cabal install все поставил

наверное Chris не собирал стэком

надо чтоли issue открыть

fpco ребята не собирают стеком

лучшая реклама

на колбасной фабрике работаешь - колбасу не кушаешь

а чем собирают fpco ?

думаю что стеком

stack/cabal ghci прикольные

Kirill я помню я когда-то говорил тебе что посмотрю и сделаю минимальный пример похожий на https://ruhaskell.org/posts/theory/2016/01/06/serialization-with-deptypes.html это все ещё актуально?

я только сейчас вспомнил

Ну да, хочется избавиться от повторения, или узнать насколько чревато такое избавление

а синглетоны для Symbol у нас есть?

пока как-то лень было их втаскивать :)

а, ты про вообще :)

да

блин засада какая-то

ладно попробую закрыто сначала

Господа, прошу не закидывать палками и больно не пинать, но у меня вопрос по инструментарию. Есть удобный способ смотреть определения библиотечных функций? Сейчас использую VS Code и несколько неудобно разбираться в новом, бегая между hackage и редактором.

https://github.com/haskell/haskell-ide-engine

интерессуют именно определения библиотечных функций?

это немножечко странно

правда у меня почему-то не заработал этот hie

haskell-ide-engine должен показать их типы (и в светлом будущем документацию)

но определения-то зачем?

Да типы, типы, всё так

и документацию

вообще плагин под IDEA всё делает, но эта штука однозначно медленнее, чем VS Code /Atom/ иже с ними

для vscode еще haskero есть

И haskelly. Только у них есть жуткий недостаток - если в коде ошибка, то все подсказки из библиотек ломаются

haskell-ide-engine должен показать их типы (и в светлом будущем документацию)

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

и под виндой не работает.

судя по всему

Господа, прошу не закидывать палками и больно не пинать, но у меня вопрос по инструментарию. Есть удобный способ смотреть определения библиотечных функций? Сейчас использую VS Code и несколько неудобно разбираться в новом, бегая между hackage и редактором.

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

и под виндой не работает.

сейчас под виндой не работает ghc-mod и следовательно зависящий от него hie, но в ghc-mod-е это вроде на днях поправили, значит скоро и в hie должны

ну и сгенеренная стеком документация под виндой не работает (на винде путь к ее местонахождению другой)

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

Понятненько, тернистый, однако, путь

К недавней дискуссии

На днях в хаскеляч залетел фанат Idris'а. Замечу, что любые попытки построить тьюринг-полный язык с тотальным подмножеством, основанном на MLTT, должны вызывать справедливый интерес haskell-коммьюнити, а чаты по идрису и хаскелю в значительной мере пересекаются. Естественно в дискуссии всплывал вопрос о целесообразности ленивой стратегии редукции. Кроме стандартных аргументов в духе "это сложно и не нужно" всплыл ещё один, претендующий на объективность и достоверность. Утверждалось, что ленивая стратегия редукции -- основная причина сложности построения денотационной семантики хаскеля, основанной на теории категорий. Но так ли это? По языку программирования мы хотим построить такую категорию, что каждому типу будет соответствовать объект категории, а каждой функции из A в B -- соответствующую стрелку. При этом мы хотим, чтобы функциям f,g :: A-> B соответствовали одинаковые стрелки тогда и только тогда, когда для любого a из A f(a) = g(a) Сложность наступает как только мы берём тьюринг-полный язык. Ведь далеко не все функции останавливаются! Как приравнять функции, которые работают бесконечно долго? Есть два выхода из этой ситуации. Оба работают только для языков с энергичной редукцией. Первый -- просто выкинуть нетотальные функции из категории, сделать вид что их просто нет. Естественно при этом теряется всякая доказательная сила рассуждений об этом языке с помощью теории категорий, ведь о частичных функциях мы не может сказать вообще ничего. Второй -- "добавить" внутрь типа специальный элемент _|_ и сказать, что дополнить f(a) = _|_, если она f(a) не останавливается. Так мы получим корректное равенство на стрелках, но что будет, если мы начнём над этой категорией рассматривать эндофункторы и интерпретировать их в терминах computer science? Ничего хорошего: ведь мы можем легко переводить тотальные функции в нетотальные и наоборот, информация о том кто из них кто абсолютно теряется. Мы столкнулись с той же проблемой, что и в первом случае, но подошли с ней с другой стороны. Резюмируя: корректной категориальной денотационной семантики не может быть ни у одного тьюринг-полного языка. Но что же делать со всеми наработками в этой области? Ведь на практике они работают. Чуть позже я постараюсь сделать наброски ответа на него

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

то есть для теорката любые две стрелки ∀ α β. α → β неразличимы

что же значит "При этом мы хотим, чтобы функциям f,g :: A-> B соответствовали одинаковые стрелки тогда и только тогда, когда для любого a из A f(a) = g(a)"

не ну как, это не совсем так

Не, в 1-теории категорий множество стрелок Hom(A,B) это множество :)

Есть более хитрые образования, где Hom(A,B) группоид, чум или симплициальное множество, но всё это уже higher category theory

то есть для теорката любые две стрелки ∀ α β. α → β неразличимы

На самом деле категория, в которой две стрелки одного вида не различимы, это poset aka частично упорядоченное множество с точностью до эквивалентности объектов. Это ты (0,1)-категорию придумал

Добрый вечер. У меня возник чисто теоретический вопрос. Если я не ошибаюсь, то использование только чистых функций позволяет делать параллелизм без особых проблем для программиста. А что будет если использовать не просто чистые функции, а те, которые могут принимать аргументы в любом порядке? Конкретно интересует: 1. Как изменится система типов 2. Даст ли это какой-нибудь выигрыш 3. Любую ли чистую функцию можно свести к чистой коммутативной или для этого нужны какие-то ограничения на чистые функции 4. Есть ли материалы по этой теме, если она не является совершенно абсурдной, разумеется

Добрый вечер. У меня возник чисто теоретический вопрос. Если я не ошибаюсь, то использование только чистых функций позволяет делать параллелизм без особых проблем для программиста. А что будет если использовать не просто чистые функции, а те, которые могут принимать аргументы в любом порядке? Конкретно интересует: 1. Как изменится система типов 2. Даст ли это какой-нибудь выигрыш 3. Любую ли чистую функцию можно свести к чистой коммутативной или для этого нужны какие-то ограничения на чистые функции 4. Есть ли материалы по этой теме, если она не является совершенно абсурдной, разумеется

В хаскеле у любой функции один аргумент. Если ты говоришь о каком-нибудь гипотетическом ML'е с типами функций AxB -> T, то между таким типом и BxA -> T есть изоморфизм, т.е в определённом смысле порядок аргументов в принципе не важен. А что тебя сподвигло на мысли о порядке аргументов?

В хаскеле у любой функции один аргумент. Если ты говоришь о каком-нибудь гипотетическом ML'е с типами функций AxB -> T, то между таким типом и BxA -> T есть изоморфизм, т.е в определённом смысле порядок аргументов в принципе не важен. А что тебя сподвигло на мысли о порядке аргументов?

Недавно познакомился с unsafePerformIO который при не очень аккуратном обращении меняет порядок аргументов и, вроде как, может запортить результат даже чистой функции и получится не то, что ожидалось Ну. Например функция вычитания (-) :: Int -> Int -> Int при этом a - b /= b - a в общем случае

не меняет он порядок аргументов никогда

это какое-то... я даже не знаю откуда предположение

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

т.е. (trace "foo" a) - (trace "bar" b)

нету гарантии, что вы увидишь foo bar или bar foo

Pavel ^

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

нету гарантии, что вы увидишь foo bar или bar foo

ну вот и мы получаем либо foo bar или bar foo и если мы захотим это снова заиспользовать и передать в функцию, то мы уже не знаем какой порядок, что есть плохо :с почему функции будут делать глупое? то есть класс чистых функций по мощности выполнимых задач эквивалентен чистым коммутативным? и типы же тоже должны измениться ведь получается невозможным делать типы отличающиеся от вида X -> ... -> X -> Y или я неправ?

> ну вот и мы получаем либо foo bar или bar foo > и если мы захотим это снова заиспользовать и передать в функцию, то мы уже не знаем какой порядок, что есть плохо :с это глупость, независимо от того вычислится первым a или b они передадутся в функцию в правильном порядке