бесконечность что ли

да, похоже

а, ну да, бесконечность гарантированно

тут же для выражения типа используют его мощность. У универсума мощность - алеф нуль

а ⊤ принадлежит себе?

хз, в идрисе есть Type 1, который содержит в себе Type, потом Type 2, который содержит Type 1

аналогично в hott: U, U_1, U_2

тип Type может зависеть от числа в idris?

?

а, у них в faq есть

короче, написал функцию, которая отдает тип аргумента

getType : (a : ty) -> Type getType _ {ty} = ty

лол просто

Это Idris?

да

подкасты о функциональщине https://www.fpcasts.com/

и есть что-нибудь ок?

(скорей всего англоязычный подкаст наискучнейшая трата времени)

и есть что-нибудь ок?

на вкус и цвет. мне например ок этот 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 я не могу

но получить третий нельзя же

В агде по уровням можно даже forall делать

но получить третий нельзя же

Это как? Тогда его просто нет же. Или там хитрое падение иерархии?

Да просто нет синтаксиса такого для получения, или я не знаю

Идрис все Type n к Type приводит

А самому n указать нельзя, увидеть я его смог только через :t Type

ну просто у тебя коснтрукция Type 1 интерпретируется как вызов конструктора Type c параметром

а у меня продолжаются проблемы с зависимыми типами в хаскелле

data AIResult a where AIResult :: SAIIntent b -> AIMeta -> (ActionToParam b) -> AIResult b

singletons [d| data AIIntent = IntentTask |]

но я не понимаю как написать функцию которая будет возвращать тип AIResult a

потому что у меня всегда выскакивает ошибка про rigid variable, из чего я делаю вывод, что у переменной a типе AIResult ограничение, что это kind AIIntent

а в возвращаемом значении — это просто *, но как связать ее я не понимаю. В Idris такое обычно решается зависимой парой, в хаскелле я нашел в гисте какую-то имплементацию но пока не уверен, что она мне поможет

ЧЯДНТ?

Я ничего не понял, но может какой PolyKind, чтобы заменить * на какой-нибудь полиморфный AIResult (a :: k)

Из A |= not not A

это классическая логика?

Не понимаю, чем не устраивает монадическая модель сайд-эффектов?

World->(World, a)

Это никак не мешает редукции лямбда термов.

это классическая логика?

нет, классическая это когда наоборот not (not A) => A

|= это же entails

то есть тоже самое

я правильно понимаю что в хаскелле есть 2 типа функций: те которые генерируют thunk'и и те которые форсят вычисление этих thunk'ов? ведут ли себя эти два типа как потоки в ситуации производитель-потребитель? т.е. очевидно что форсящая функция требует от thunk'а столько сколько нужно ей. но может ли thunk ей "вежливо отказать" (как потребитель производящий данные медленее, чем их поглощает потребитель)?

как отказать? данные будут производиться, коли запрошены

как отказать? данные будут производиться, коли запрошены

а если их пока нет

потребитель будет ждать

ну например есть функция читающая файл и обрабатывающяя его. причем вторая намного быстрее первой

ага

значит ждать

производитель-потребитель — в случае ленивости, пожалуй, плохой подход

для чтения файла одновременно с с обработкой правильнее использовать не лень, а какое-нибудь сопроцедурное решение, например, streaming, pipes, conduit

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

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

спасибо

учту

а ленивость оставить для чистых вычислений

может кто-нибудь объяснить как получить compiled form в Krivine's machine? Или может кто-нибудь знает хороший источник, где нормально объясняют имплементацию машины?

А кто-нибудь в курсе чем отличается 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)." Не распарсил фразу до скобок.

если есть структура в которой есть общие части, например let x= 1:x

то appendCompact её компактно расположит, и то, что x общий будет сохранено

а appectCompactNoShare - разойдётся

или если есть дерево где есть 2 одинаковые ветки (одна и та же ссылка), то в случае appendComapctNoShare они будут полностью сериализованы

с Share там будет ссылка

т.е. меньше размер посылаемой структуры, но сложнее строить

А, все. Понял, спасибо :-)

Ща пишу либу для преобразования вигнера-вилли, и там GC жестит.

@HaskellMouse ты уже с настройками GC игрался?

-A, -n

они очень неудачные по дефолту

Сейчас будет очень плохо сформулированные вопросы :с 1) Существует ли возможность в идрисе создать биекцию между значениями и типами т.е. 42 :: Num 42, например? 2) Существует ли возможность автоматизировать это создание? 3) Существует ли возможность при этом всём сохранить человечность кода?

Сейчас будет очень плохо сформулированные вопросы :с 1) Существует ли возможность в идрисе создать биекцию между значениями и типами т.е. 42 :: Num 42, например? 2) Существует ли возможность автоматизировать это создание? 3) Существует ли возможность при этом всём сохранить человечность кода?

А чего не в чатик по идрису?

Синглтоны хочешь?

А чего не в чатик по идрису?

такой есть на русском?

Конечно. Правда завсегдатаи с этим чатом сильно пересекаются: https://t.me/joinchat/AAAAAD9SWO_tLd7rJ9S7Ig

Синглтоны хочешь?

не совсем хочу, чтобы когда я делаю вот так: pls : Num a -> Num b -> Num (a + b) pls = + мне можно было бы выводить тип по реализации, а не реализацию по типам

Конечно. Правда завсегдатаи с этим чатом сильно пересекаются: https://t.me/joinchat/AAAAAD9SWO_tLd7rJ9S7Ig

спасибо

идрис же выводит тип по реализации, минимум чтобы проверить

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

это ж не haskell какой-нить, где это может рабоать

идрис же выводит тип по реализации, минимум чтобы проверить

но например sort : List a -> List a reverse : List a -> List a, а мне хотелось бы узнать возможность биекции реализация <-> тип

это невозможно в общем случае

с другой стороны типы функций недостаточные для описания

например если сделать sort :: UniqueList a -> AscendingUniqueList a

но например sort : List a -> List a reverse : List a -> List a, а мне хотелось бы узнать возможность биекции реализация <-> тип

Ты хочешь зафиксировать для типа определённый элемент?

то тогда любая функция которая имеет такой тип будет сортировкой

при этом как известно из практики существует много разных сортировок отличающихся сложностью

любая подходит

то тогда любая функция которая имеет такой тип будет сортировкой

да и тогда множество реализаций разобьётся на классы эквивалентности, как и множество типов

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