хотя баги там есть такие, что лицорука, да

мы используем хаскельную обёртку вокруг ansible, например

Вот вы извращенцы. А чего бы не просто через ssh-клиент?

Я это сейчас на Э-ке пишу, песня просто.

интересно кстати, devops haskell кто-нибудь видел?

У нас девопс в основном на nix, но есть немного на Haskell https://github.com/input-output-hk/iohk-ops/blob/ea594d09d217381d62c057f4a5742a494dddb827/iohk/CardanoCSL.hs

Прикольно

Когда-то мне тут советовали сервант, но я испугался не смотря даже на него и взял Скотти. А зря, сервант действительно крут и достаточно и при этом просто работает

$ ps aux |grep xmo den 21720 1.1 0.1 1074307988 28352 ? Sl авг10 111:19 /home/den/.xmonad/taffybar den 21721 0.0 0.7 1073930920 117500 ? S авг10 4:49 /home/den/.xmonad/xmonad-x86_64-linux Только сейчас заметил. Это норм? =)

Занятно. Посмотрел на сервере, где backend крутится - то же самое

значит норма

оччень странно

Я это сейчас на Э-ке пишу, песня просто.

а темплейтинг чем делаешь (или не делаешь)?

@verrens что именно не нравится?

1T виртуальной памяти? нормально

1T виртуальной памяти? нормально

кстати, я разобрался что за проблема у меня была с out of memory при сборке при наличии свопа. причина была в отключеном LPAE на 32 битной системе.

вот я голову поломал тогда!

а темплейтинг чем делаешь (или не делаешь)?

Пока регуляркой, а там erlydtl подцепить недолго.

А насчет офисного чата. Это тот еще баян. Называется - зачем на работу перся?

Есть какая-то возможность делать kind synonyms?

типа kind Type = *

да, словом type

type Type = * Not in scope: type constructor or class `*' Operator applied to too few arguments: *

@kana_sama Посмотри, как это сделано здесь: https://www.stackage.org/haddock/lts-9.1/base-4.9.1.0/Data-Kind.html#t:Type

а лучше import Data.Kind (Type) и не морочьте голову

@kana_sama Посмотри, как это сделано здесь: https://www.stackage.org/haddock/lts-9.1/base-4.9.1.0/Data-Kind.html#t:Type

сам смотрел? там весьма заковыристо сделано: -- | The kind of types with values. For example @Int :: Type@. type Type = TYPE 'LiftedRep -- | A backward-compatible (pre-GHC 8.0) synonym for 'Type' type * = TYPE 'LiftedRep

если вопрос был в том, как делать синонимы, то ответ @chshersh максимально точен

в модуле можно посмотреть как это сделано

поскольку у нас нету информации является ли пример выше конечной задачей @kana_sama

или это минимальный пример

а лучше import Data.Kind (Type) и не морочьте голову

ага, так и сделал

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

в модуле можно посмотреть как это сделано

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

Type не синоним для TYPE 'LiftedRep o.O?

и *

ну вообще для синонима кайндов требуется TypeInType

значит я чего-то не понимаю

Type определяется не через синоним для *

не могу проследить

@cblp_su вообще я согласен, у мне трюк оттуда сходу не удалось повторить

в старых версия библиотеки heist была полезная функция (##) :: Text -> s -> Splices s, которая в более новых версиях библиотеки пропала. никто не подскажет альтернативу?

@teenage_mutant_ninja_turtle предположу, что имеется в виду: https://hackage.haskell.org/package/map-syntax-0.2.0.2/docs/Data-Map-Syntax.html#v:-35--35-

Как говорится в Heist.SpliceAPI Deprecated: Use Data.Map.Syntax from the map-syntax package instead

Так что ## из map-syntax должна подойти, ибо type Splices s = MapSyntax Text s и (##) :: k -> v -> MapSyntax k v

Aleksey, спасибо!

Что означает Refl? То есть это сокращение от Reflection? Тогда как это связано с равенством типов?

Опечатка, да, исправил

Это не связано с reflection

это от слова reflexive (https://en.wikipedia.org/wiki/Reflexive_relation)

а, все, спасибо, теперь понятно, с этим термином знаком

Опечатка, да, исправил

Не знаю как хаскеле В идрисе это тип который означает равенство Refl : a -> a Refl x = x и его название от свойства рефлексивности

@int_index, а как это связано с рефлексивностью? по-моему, это как раз рефлексия, то есть перенос информации из типов в значения

Нет

Это связано с рефлексивностью напрямую, потому что любой тип равен сам себе

Refl это witness для рефлексивности равенства

@int_index, а как это связано с рефлексивностью? по-моему, это как раз рефлексия, то есть перенос информации из типов в значения

Отношение равенства является отношением эквивалентности А для него характерны три свойства симметричность, рефлексивность и транзитивность

Refl это witness для рефлексивности равенства

Что такое witness?

Пруфтёрм

Отношение равенства является отношением эквивалентности А для него характерны три свойства симметричность, рефлексивность и транзитивность

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

Refl это witness для рефлексивности равенства

а вот это имеет смысл

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

x = x это рефлексивность по своему определению

Пруфтёрм

спасибо

x = x это рефлексивность по своему определению

спасибо, но @int_index уже объяснил всё

спасибо, но @int_index уже объяснил всё

Угу

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

это называется relevance

Не знаю как хаскеле В идрисе это тип который означает равенство Refl : a -> a Refl x = x и его название от свойства рефлексивности

там не так немного data (=) : a -> a -> Type where Refl : (=) x x

Ну и в тотальном языке с axiom K вполне можно Refl делать нерелевантным (но не в Haskell)

ну и = инфиксный

там не так немного data (=) : a -> a -> Type where Refl : (=) x x

да я неправ

угу

Отношение равенства является отношением эквивалентности А для него характерны три свойства симметричность, рефлексивность и транзитивность

симметричность и транзитивность там есть: sym : {left:a} -> {right:b} -> left = right -> right = left sym Refl = Refl trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c trans Refl Refl = Refl

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

Если игнорировать боттомы, то надо понимать, что Refl это просто () в рантайме, а оттого он ничего "в программу" не передеает

симметричность и транзитивность там есть: sym : {left:a} -> {right:b} -> left = right -> right = left sym Refl = Refl trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c trans Refl Refl = Refl

про sym — знал а вот про trans — нет спасибо буду иметь в виду

да, если брать идрис, то доказательства он везде старается стирать

Если игнорировать боттомы, то надо понимать, что Refl это просто () в рантайме, а оттого он ничего "в программу" не передеает

да, моё предположение было далеко от реальности

да, если брать идрис, то доказательства он везде старается стирать

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

http://docs.idris-lang.org/en/latest/reference/erasure.html

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

Для производительности делается

Вот DH так не сможет, кстати.

Поэтому есть все шансы, что DH-код будет медленнее, чем наивный код без пруфов

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

а имеет смысл доказательства оставлять прямо в реализации в таком случае?

в DH есть

какой, если это замедляет код?

Такой, что ты не можешь написать let x = x in x :: (Int :~: Bool)

Точнее, можешь, но уйдешь в цикл на матчинге, а не получишь unsafeCoerce

Тоталити-чекер нам ведь никто не обещал завезти.

а спасибо

Интересно а тотальность и ленивость могут быть вместе?

Разумеется

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

Для тотальных программ ленивость/строгость — это просто разные стратегии вычисления. А с корекурсией можно и типичный юзкейс ленивости с бесконечными структурами покрыть

Ну это понятно, но в лени может быть не так

Вот например боттом

Или зацикливание