кана
это первый пост в моем канале
Anonymous
то есть Either (a, b) Void, к примеру, не считается?
кана
Either (a, b) Void это то же самое, что и (a, b)
кана
a*b + 0 = a*b
Anonymous
есть где почитать про использование алгебры для типов?
a66ath
В TAPL?
Anonymous
крууто, а как ⊤ выражается?
кана
мб какой тип-универсум, типа Type в идрисе
кана
forall a. a
Anonymous
бесконечность что ли
кана
да, похоже
кана
а, ну да, бесконечность гарантированно
кана
тут же для выражения типа используют его мощность. У универсума мощность - алеф нуль
Anonymous
а ⊤ принадлежит себе?
кана
хз, в идрисе есть Type 1, который содержит в себе Type, потом Type 2, который содержит Type 1
кана
аналогично в hott: U, U_1, U_2
Anonymous
тип Type может зависеть от числа в idris?
кана
Anonymous
🤔
Anonymous
а, у них в faq есть
кана
короче, написал функцию, которая отдает тип аргумента
кана
getType : (a : ty) -> Type
getType _ {ty} = ty
кана
кана
лол просто
a66ath
Это Idris?
кана
да
Sergey
подкасты о функциональщине https://www.fpcasts.com/
Влод
и есть что-нибудь ок?
Влод
(скорей всего англоязычный подкаст наискучнейшая трата времени)
Sergey
и есть что-нибудь ок?
на вкус и цвет. мне например ок этот http://typetheorypodcast.com/2014/08/episode-1-peter-dybjer-on-type-theory-and-testing/
Евгений
хз, в идрисе есть Type 1, который содержит в себе Type, потом Type 2, который содержит Type 1
Три уровня Type в 2k17? о.о
кана
их бесконечно, судя по книге
Евгений
А, ну ок
кана
достать что-то больше Type 1 я не могу
Anonymous
но получить третий нельзя же
Евгений
В агде по уровням можно даже forall делать
Евгений
но получить третий нельзя же
Это как? Тогда его просто нет же. Или там хитрое падение иерархии?
кана
Да просто нет синтаксиса такого для получения, или я не знаю
кана
Идрис все Type n к Type приводит
кана
А самому n указать нельзя, увидеть я его смог только через :t Type
Viacheslav
ну просто у тебя коснтрукция Type 1 интерпретируется как вызов конструктора Type c параметром
Viacheslav
а у меня продолжаются проблемы с зависимыми типами в хаскелле
Viacheslav
data AIResult a where
AIResult :: SAIIntent b -> AIMeta -> (ActionToParam b) -> AIResult b
Viacheslav
singletons [d|
data AIIntent = IntentTask
|]
Viacheslav
но я не понимаю как написать функцию которая будет возвращать тип AIResult a
Viacheslav
потому что у меня всегда выскакивает ошибка про rigid variable, из чего я делаю вывод, что у переменной a типе AIResult ограничение, что это kind AIIntent
Viacheslav
а в возвращаемом значении — это просто *, но как связать ее я не понимаю. В Idris такое обычно решается зависимой парой, в хаскелле я нашел в гисте какую-то имплементацию но пока не уверен, что она мне поможет
Viacheslav
ЧЯДНТ?
кана
Я ничего не понял, но может какой PolyKind, чтобы заменить * на какой-нибудь полиморфный AIResult (a :: k)
Andrei
Не понимаю, чем не устраивает монадическая модель сайд-эффектов?
Andrei
World->(World, a)
Andrei
Это никак не мешает редукции лямбда термов.
Anonymous
|= это же entails
Anonymous
то есть тоже самое
melvin
я правильно понимаю что в хаскелле есть 2 типа функций: те которые генерируют thunk'и и те которые форсят вычисление этих thunk'ов? ведут ли себя эти два типа как потоки в ситуации производитель-потребитель? т.е. очевидно что форсящая функция требует от thunk'а столько сколько нужно ей. но может ли thunk ей "вежливо отказать" (как потребитель производящий данные медленее, чем их поглощает потребитель)?
Cheese
как отказать? данные будут производиться, коли запрошены
Cheese
потребитель будет ждать
melvin
ну например есть функция читающая файл и обрабатывающяя его. причем вторая намного быстрее первой
melvin
ага
melvin
значит ждать
Cheese
производитель-потребитель — в случае ленивости, пожалуй, плохой подход
Cheese
для чтения файла одновременно с с обработкой правильнее использовать не лень, а какое-нибудь сопроцедурное решение, например, streaming, pipes, conduit
Cheese
там уже можно управлять энергичностью порождения и потребления
Cheese
или взять очередь и к ней обращаться из разных нитей, если хочется параллельности
melvin
спасибо
melvin
учту
Cheese
а ленивость оставить для чистых вычислений
Alexandr
может кто-нибудь объяснить как получить compiled form в Krivine's machine? Или может кто-нибудь знает хороший источник, где нормально объясняют имплементацию машины?
Anonymous
А кто-нибудь в курсе чем отличается appendCompactNoShare от appendCompact? Написано: "This function differs from appendCompact in that it will not preserve internal sharing in the passed in value (and it will diverge on cyclic structures)." Не распарсил фразу до скобок.
Alexander
если есть структура в которой есть общие части, например let x= 1:x
Alexander
то appendCompact её компактно расположит, и то, что x общий будет сохранено
Alexander
а appectCompactNoShare - разойдётся
Alexander
или если есть дерево где есть 2 одинаковые ветки (одна и та же ссылка), то в случае appendComapctNoShare они будут полностью сериализованы
Alexander
с Share там будет ссылка
Alexander
т.е. меньше размер посылаемой структуры, но сложнее строить
Anonymous
А, все. Понял, спасибо :-)