Alexander
@cblp_su вообще я согласен, у мне трюк оттуда сходу не удалось повторить
Anonymous
в старых версия библиотеки heist была полезная функция (##) :: Text -> s -> Splices s, которая в более новых версиях библиотеки пропала. никто не подскажет альтернативу?
Aleksei (astynax)
@teenage_mutant_ninja_turtle предположу, что имеется в виду: https://hackage.haskell.org/package/map-syntax-0.2.0.2/docs/Data-Map-Syntax.html#v:-35--35-
Aleksei (astynax)
Как говорится в Heist.SpliceAPI Deprecated: Use Data.Map.Syntax from the map-syntax package instead
Aleksei (astynax)
Так что ## из map-syntax должна подойти, ибо
type Splices s = MapSyntax Text s
и
(##) :: k -> v -> MapSyntax k v
Anonymous
Aleksey, спасибо!
кана
Что означает Refl? То есть это сокращение от Reflection? Тогда как это связано с равенством типов?
кана
Опечатка, да, исправил
Vladislav
Это не связано с reflection
Vladislav
это от слова reflexive (https://en.wikipedia.org/wiki/Reflexive_relation)
кана
а, все, спасибо, теперь понятно, с этим термином знаком
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
Опечатка, да, исправил
Не знаю как хаскеле
В идрисе это тип который означает равенство
Refl : a -> a
Refl x = x
и его название от свойства рефлексивности
Cheese
@int_index, а как это связано с рефлексивностью? по-моему, это как раз рефлексия, то есть перенос информации из типов в значения
Vladislav
Нет
Vladislav
Это связано с рефлексивностью напрямую, потому что любой тип равен сам себе
Vladislav
Refl это witness для рефлексивности равенства
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
@int_index, а как это связано с рефлексивностью? по-моему, это как раз рефлексия, то есть перенос информации из типов в значения
Отношение равенства является отношением эквивалентности
А для него характерны три свойства
симметричность, рефлексивность и транзитивность
Vladislav
Пруфтёрм
Cheese
Отношение равенства является отношением эквивалентности
А для него характерны три свойства
симметричность, рефлексивность и транзитивность
да, но разве рефлексивность что-то даёт нам тут?
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
да, но разве рефлексивность что-то даёт нам тут?
x = x
это рефлексивность по своему определению
Cheese
я просто думал, что это "рефлексия" в том смысле, информация о типе передаётся из компилятора в программу
Vladislav
это называется relevance
Alex
Не знаю как хаскеле
В идрисе это тип который означает равенство
Refl : a -> a
Refl x = x
и его название от свойства рефлексивности
там не так немного
data (=) : a -> a -> Type where
Refl : (=) x x
Vladislav
Ну и в тотальном языке с axiom K вполне можно Refl делать нерелевантным (но не в Haskell)
Alex
ну и = инфиксный
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
угу
Alex
Отношение равенства является отношением эквивалентности
А для него характерны три свойства
симметричность, рефлексивность и транзитивность
симметричность и транзитивность там есть:
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
Vladislav
я просто думал, что это "рефлексия" в том смысле, информация о типе передаётся из компилятора в программу
Если игнорировать боттомы, то надо понимать, что 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 — нет
спасибо
буду иметь в виду
Alex
да, если брать идрис, то доказательства он везде старается стирать
Cheese
Если игнорировать боттомы, то надо понимать, что Refl это просто () в рантайме, а оттого он ничего "в программу" не передеает
да, моё предположение было далеко от реальности
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
да, если брать идрис, то доказательства он везде старается стирать
что значит стирает доказаельства?
Alex
http://docs.idris-lang.org/en/latest/reference/erasure.html
Vladislav
Значит он не передает пруфтермы, а довольствуется фактом их наличия
Vladislav
Для производительности делается
Vladislav
Вот DH так не сможет, кстати.
Vladislav
Поэтому есть все шансы, что DH-код будет медленнее, чем наивный код без пруфов
Vladislav
а в Idris, гипотетически, добавить какое-то доказательство может быть бесплатным с точки зрения рантайма
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
а имеет смысл доказательства оставлять прямо в реализации в таком случае?
Vladislav
в DH есть
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
какой, если это замедляет код?
Vladislav
Такой, что ты не можешь написать let x = x in x :: (Int :~: Bool)
Vladislav
Точнее, можешь, но уйдешь в цикл на матчинге, а не получишь unsafeCoerce
Vladislav
Тоталити-чекер нам ведь никто не обещал завезти.
ᛏᚺᛖ ᛚᛖᛋᛒᛁᚨᚾ ᛗᚨᚾ ᚷᛁᚱᛚ 🐝
а
спасибо
Зигохистоморфный
Интересно а тотальность и ленивость могут быть вместе?
Vladislav
Разумеется
Alex
тотальность типа гарантирует, что каким порядком ни вычисляй, получишь одно и то же
Vladislav
Для тотальных программ ленивость/строгость — это просто разные стратегии вычисления. А с корекурсией можно и типичный юзкейс ленивости с бесконечными структурами покрыть
Зигохистоморфный
Ну это понятно, но в лени может быть не так
Зигохистоморфный
Вот например боттом
Зигохистоморфный
Или зацикливание
Vladislav
Это не результат ленивости
Alex
тотальность это отсутствие жоп
Alex
зацикливание разновидность жопы
Зигохистоморфный
Ну да) это значит то, что хаск не нормальная категория сет
Vladislav
Ну начнем с того, что типы /= сеты
Vladislav
Продолжим тем, что если не игнорировать боттомы, то про Хаскель вообще математически трудно рассуждать и мало что можно сказать
Зигохистоморфный
Вот тот же y комбинатор это есть разновидность жопы
Vladislav
Нет
Alex
ну вообще вроде да, фикспоинт это разновидность жопы
Vladislav
Y/fixpoint это unrestricted recursion
Зигохистоморфный
Сам Карри это говорил
Зигохистоморфный
Что это некий парадокс
Vladislav
это только значит, что через него можно выразить боттомы
Vladislav
но не значит, что любое его использование дает боттом
Зигохистоморфный
https://gitlab.anu.edu.au/mu/mu-client-ghc
Cheese
попробую и здесь спросить
дано: data A = forall (b :: B) . SingI b => A (F b)
как из (a :: A) извлечь (f :: F b)?
у меня пока получилось только через SingI построить A -> B, то есть из (a :: A) я могу узнать (b :: B) лежащего внутри объекта, а значит, точно знаю тип (F b)
Alexander
знать знаешь, но как ты значение построишь. если F это не функтор или т.п.?
Cheese
так вот надо не построить, а извлечь
Cheese
и даже если функтор, я не смогу построить ровно то, что там лежит
Cheese
я использую экзистенциальный тип в роли суммы
Alexander
есть мимимальный код?
Alexander
лень все писать самому, чтоб поиграться