тотальность это отсутствие жоп

зацикливание разновидность жопы

Ну да) это значит то, что хаск не нормальная категория сет

Ну начнем с того, что типы /= сеты

Продолжим тем, что если не игнорировать боттомы, то про Хаскель вообще математически трудно рассуждать и мало что можно сказать

Вот тот же y комбинатор это есть разновидность жопы

Нет

ну вообще вроде да, фикспоинт это разновидность жопы

Y/fixpoint это unrestricted recursion

Сам Карри это говорил

Что это некий парадокс

это только значит, что через него можно выразить боттомы

но не значит, что любое его использование дает боттом

https://gitlab.anu.edu.au/mu/mu-client-ghc

попробую и здесь спросить дано: data A = forall (b :: B) . SingI b => A (F b) как из (a :: A) извлечь (f :: F b)? у меня пока получилось только через SingI построить A -> B, то есть из (a :: A) я могу узнать (b :: B) лежащего внутри объекта, а значит, точно знаю тип (F b)

знать знаешь, но как ты значение построишь. если F это не функтор или т.п.?

так вот надо не построить, а извлечь

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

я использую экзистенциальный тип в роли суммы

есть мимимальный код?

лень все писать самому, чтоб поиграться

попробую написать сегодня

а как это работает?

а туплю

@cblp_su а можешь сигнатуру того ,что ты хочешь написать написать?

ну или F хотя бы что такое

@cblp_su а можешь сигнатуру того ,что ты хочешь написать написать?

вот я сам завис на этом вопросе

потому, что я попытался мин пример сделать и или решение тривиальное

но тогда и F и B тривиальные и там и без SingI сработает

но у тебя наверное дургой случай

например, если B ~ Nat то не сработает

ну или что-то плохо перечислимое

F в данном конкретном случае — data family, где каждый инстанс — простая data из чисел, списков и прочих простых штук

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

что ты называешь тривиальным решением?

в принципе, я могу взять Union F UniverseB, по нему матчить тоже не очень сахар, но я хотя бы знаю, как

проще минимальный пример, а то у меня явное ощущение, что я не то решаю

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

@cblp_su Я чего-то может не так понял, но по фрагменту кода выше чтобы извлечь F b из A надо просто запатеррнматчить

Потому что внутри A как раз и лежит F b

да

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

т.е. там в зависимости от b будут разные данные

Так для этого там SingI b, по которому можно матчить

ну вот да, по нему матчить и в каждой ветке раскрывать f правильно

(примерно то, что я называл тривиальным решением)

А вообще здесь A это зависимая пара (b :: B, F b) по сути

Поэтому и операций можно ожидать соответствующих. Извлечь первый компонент, извлечь второй компонент. Матчить по первому, чтобы получить type refinement по второму.

Σ B F

для этого обязательно положить B явным полем? data A = forall (b :: B) . A (Sing b) (F b) что-то такое?

Sing или SingI — все одно и то же

нет

из SingI можно получить явный Sing через метод sing

а наоборот через withSingI

со ScopedTypeVariables легко забиндить типа так: foo (A (fb :: F b)) = case sing :: Sing b of ...

я бы написал kk :: F B -> Sing B ; kk _ = sing но наверняка можно со scopedtypevariables

@int_index чепятает быстрее

да и поточнее

и там внутри многоточия будет b ~ B42?

Приветствую. А есть ли возможность отключить возможность ввода опций рантайма при запуске?

Гугл сходу не знает :-(

-rtsopts={none,some,all} ?

@cblp_su { SB42 -> ... ; SB41 -> ...}

свой hs_main если только сделать

@qnikst -rtsopts=none не будет работать?

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ffi-chap.html#using-your-own-main

не знаю, давай попробуем

мне казалось оно все равно будет на -RTS ... смотреть

qnikst@qwork ~ $ ghc 1.hs -rtsopts=none [1 of 1] Compiling Main ( 1.hs, 1.o ) Linking 1 ... qnikst@qwork ~ $ ./1 -RTS -h foo qnikst@qwork ~ $ ./1 +RTS -h 1: RTS options are disabled. Link with -rtsopts to enable them.

аналогично

т.е. отлючены, но парсер смотит

а это не то, что хочет топикстартер достичь?

нельзя даже —help сделать

не знаю

Rinat ^^

Хмм

Сек :-)

Работает, спасибо!

Я пробовал вообще убрать rtsopts

Но не сработало, а rtsopts=none делает именно то, что нужно :-)

а вообще это кто-то юзает? https://hackage.haskell.org/package/machines-0.6.3 я помню в универе были автоматы Мили, Мура

https://github.com/Copilot-Language/Copilot

Вот последнее интересно! Потыкаю, спасибо)

машинки медленные

pipe vs conduits vs streamings vs machines vs iteratee?

@qnikst а кто быстрый?

Кметт сам сказал https://stackoverflow.com/a/17282019/3042847 ...

пайпы кондуиты стриминг

зато в машинках много разнообразия)

что делают авторы пурскриптовых пакетов? просто портируют хаскельные (особо не напрягаясь) и как там так и тут нет ни одного примера! https://github.com/purescript-contrib/purescript-machines

что делают авторы пурскриптовых пакетов? просто портируют хаскельные (особо не напрягаясь) и как там так и тут нет ни одного примера! https://github.com/purescript-contrib/purescript-machines

Меня сначала сильно удивлял подход пурскрипта к документации, но потом привык

Их пакеты ограничиваются подробной документацией по методам

Причём чтобы их увидеть нужно самому догадаться зайти в pursuit и щёлкнуть на саб-модули. Не самый интуитивный вариант) Ну и примеров обычно да, нема

а какой прок от инструмента если нет примеров его использования? я потратил много времени на recursion-schemes (были бы примеры, было бы проще (только тривиалы с cata,ana,para) а сложнее уже ничего нет)

а какой прок от инструмента если нет примеров его использования? я потратил много времени на recursion-schemes (были бы примеры, было бы проще (только тривиалы с cata,ana,para) а сложнее уже ничего нет)

ну потому что иногда это единственный инструмент, который есть

а какой прок от инструмента если нет примеров его использования? я потратил много времени на recursion-schemes (были бы примеры, было бы проще (только тривиалы с cata,ana,para) а сложнее уже ничего нет)

Хз-, может подразумевают, что всё будет понятно из типа в доке

Причём в простых случаях даже так и есть Но вообще не круто конечно

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

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