Количество функций считается как степень

0^0 = 1

как и любое x^0 = 1

поэтому функций Void -> a всегда 1 для любого a, и это absurd

а в случае Void -> Void просто absurd = id

как и любой другой a -> Void

const bottom?

Не про хаскель я говорю, нету undefined никакого

Да, речь-то не про Haskell

иначе везде +1 надо делать в алгебре, чтобы боттом учитывать

Не про хаскель я говорю, нету undefined никакого

понял, т.е. у тебя Void это пустой тип?

даже без боттома

Точнее, речь про идеализированный Haskell без боттомов (как и в любых рассуждениях такого уровня)

Void и задуман как пустой тип

@ind_index тогда поясни ещё раз, пожалуйста, почему функций Void -> Void одна штука

аргумент со степенью мне кажется формальным

точнее, лучше так вопрос поставлю

в противоречие с какими аксиомами я войду, если скажу, что функций с типом "пустой тип -> пустой тип" ноль штук, а не одна штука?

а, хм, я понял, почему

давай

я в одном своем посте представлял функцию как таблицу результатов. То есть имя тип data ABC = A | B | Cи функию isA : ABC -> Bool isA A = True isA _ = Falseможно составить таблицу (кортеж Bool ^ n, где n = |ABC|) -- A B C (True, False, False) То есть каждому i-ому значению типа ABC соответствует i-ый элемент этого кортежа. Для типа 0 -> 0 это пустой кортеж (), ведь каждому значению Void соответствует некоторое значение Void.

это () это и есть единичный тип

в противоречие с какими аксиомами я войду, если скажу, что функций с типом "пустой тип -> пустой тип" ноль штук, а не одна штука?

Это ты своим утверждением аксиому ввел

А я могу доказать ее противоречивость предоставив функцию id

я имею id :: forall a. a -> a, что мне мешает взять a = Void?

Я объясню вам сейчас интуитивно, что такое Void

функция действительно для каждого элемента Void отдает элемент Void

функция a -> Void написана быть не может, потому что она должна вернуть результат, которого не может быть (по определению Void) а если уж вам удалось в текущем контексте получить Void, то это значит, что текущий кусок кода в рантайме не выполнится никогда!

потому что нет ни одного способа ему этот Void предоставить

а оттого функция Void -> a как бы говорит "вызови меня если сможешь, я тебе дам взамен что угодно, любое a"

Да только вызвать ты ее не сможешь, а потому функция может ничего и не делать

любую функцию можно определить переобором конструкторов, например, если на вход (), то f () = ... если на вход Bool, то f True = ... f False = ... если на вход Maybe a, то f Nothing = ... f (Just a) = ... а если на вход Void, то f

что записывается как f = \case{} в Haskell и как f () вместо f = ... в Agda

Например, если я имею Either Void (), то я могу сконструировать только Right (), но никогда никакого Left ... не будет в жизни, не сконструирую никак

а потом функция, которая хочет принять Either Void (), может писать f (Left e) = absurd e

и в рантайме этого codepath и не будет никогда

потому что это абсурд, будто кто-то нам Void передал

Я не очень понимаю про что вы говорите, вы про какой-то фиксированный type theory, про инлайн логику топоса или про тьюринг-полные языки?

Про любой total functional language с inductive type definitions

но ведь в идрисе у Dec конструктор No как раз принимает функцию prop -> Void, значит, такую функцию можно сконструировать

Ее можно сконструировать из ложного утверждения, типа 1 = 2

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

в этом плане это функция 0 -> 0

google paraconsistent logic

Вы a priori reductio to absurdum предполагаете, оно не во всех type theory есть

то есть, по сути, эта функция показывает, что prop тоже Void?

то есть, по сути, эта функция показывает, что prop тоже Void?

Да

Вы a priori reductio to absurdum предполагаете, оно не во всех type theory есть

Я привык работать во фреймворке интуиционистской логики, в рамках нее и рассказываю. Где-нибудь эта paraconsistent применяется в пруф-ассистантах?

Если нет, то ее польза на уровне set theory для computer scientist (т.е. интересная штука и на бумажке можно порисовать, а попрограммировать нельзя)

Нет, не применяется. Но вопрос же был теоретический, НЯП

Но вообще говоря он скорее про system f чем про dependent types

Ок, тема интересная все равно. Какой профит дает paraconsistent logic?

Потому что у тебя a параметрически полиморфная

Я вот не представляю как в ней что-то можно доказывать

Но наверное можно, раз есть, и зачем-то даже хочется

Просто вот что выходит: если тип Void -> Void населен, то и not (not A)) ~ (a -> Void) -> Void населен, то есть двойное отрицание выполняется. А в интуиционисткой логике вроде как это не аксиоматичено

Ок, тема интересная все равно. Какой профит дает paraconsistent logic?

Ну это логика рассуждений в противоречивых фактах

Звучит как call/cc

В paraconsistent logic можно мнлго чего интересного изучать, с множеством всех множеств работать, с полной арифметикой. Очень жаль, что нету готового пруф асистента для неё

> двойное отрицание выполняется Хм, я вроде соглашусь, что Void -> Void и (a -> Void) -> Void населены, но я не уверен, что ты сможешь из одного сконструировать другое

а почему двойному отрицанию не быть населенным?

К слову, (a -> Void) -> Void очевидно насёлен

Из A |= not not A

в интуиционизме недоказуема только его элиминация Not $ Not a -> a

Да, вот

https://github.com/idris-hackers/software-foundations/blob/develop/src/Logic.lidr#L1269

я в одном своем посте представлял функцию как таблицу результатов. То есть имя тип data ABC = A | B | Cи функию isA : ABC -> Bool isA A = True isA _ = Falseможно составить таблицу (кортеж Bool ^ n, где n = |ABC|) -- A B C (True, False, False) То есть каждому i-ому значению типа ABC соответствует i-ый элемент этого кортежа. Для типа 0 -> 0 это пустой кортеж (), ведь каждому значению Void соответствует некоторое значение Void.

в приниципе понятно я это для себя так объяснил множество A = {a1, a2, a3, ..., an}, |A| = n множество B = {b1, b2, b3, ..., bm}, |B| = m тогда множество функций A->B это множество различных наборов пар (всего n^m наборов) A->B = {{(a1, b1), (a2, b1), ..., (an, b1)}, .. {(a1, bm), (a2, bm), ..., (an, bm)}} и мощность этого множества |A->B| = n^m Тогда если A = ∅, B = ∅ то A -> B = {∅}, |{∅}| = 1

мощность этого множества будет m^n

Стрелочный тип - тип функции, отображения из значений одного типа в значения другого типа. Записываются как a → b, где a - входный тип, тип аргумента, а b - выходной тип, тип результата. Функция называется тотальной, если для каждого входного элемента может вернуть результат за конечое число шагов. Каждую функцию (конечно, если считать, что они все тотальные, в хаскеле это не так) a → b можно записать как таблицу значений - карту между a и b. Можно проиндексировать каждый элемент a и представить тип функции как тип кортеж из |a| элементов типа b, где i-ому элементу кортежа соответствует выходное значение функции при входном aᵢ. Приведем пример: data ABC = A | B | C isA :: ABC -> Bool isA A = True isA _ = False isA', isB', isC' :: (Bool, Bool, Bool) -- A B C isA' = (True, False, False) isB' = (False, True, False) isC' = (False, False, True ) isA - предикат, который возвращает True только для A, для всех остальных значений False. isA' - пример таблицы для этой функции. Если как-то упорядочить множество ABC и дать элементам индекс (`ABC₁ = A`, ABC₂ = B, ABC₃ = C ), то каждому i-ому элементу кортежа соответствует ABCᵢ. Нетрудно заметить, что результатирующий тип можно представить как умножение типа b на самого себя |a| раз, то есть bᵃ. Еще раз - каждую тотальную функцию вида a → b можно записать как bᵃ. Для примера выше, ABC → Bool можно записать как Bool^ABC, и действительно, Bool = 1 + 1 = 2 ABC = 1 + 1 + 1 = 3 Bool^ABC = 2^3 = 8 А именно 8 элементов есть у типа ABC → Bool, то есть ровно 8 функций мы можем составить: isNotABC, isA, isB, isC, isAorB, isAorC, isBorC, isAny :: ABC -> Bool isNotABC _ = False -- 1 isA A = True -- 2 isA _ = False isB B = True -- 3 isB _ = False isC C = True -- 4 isC _ = False isAorB x = isA x || isB x -- 5 isAorC x = isA x || isC x -- 6 isBorC x = isB x || isC x -- 7 isAny _ = True -- 8 Это все функции, которые мы можем составить с такой сигнатурой, все остальные функции будут лишь переименованиями этих (в хаскеле конечно все сложнее, но давайте забудем про пороки хаскеля). Если же взять каррированную функцию от двух аргументов a → b → c, то это аналог (c^b)^a = c^ba, а ba это пара из b и a, отсюда становится абсолютно ясно, что функции (a, b) → c и a → b → c изоморфны. Умножение функций работает так же, как и ожидается: cᵃ * cᵇ = cᵃ⁺ᵇ, то есть (a -> c, b -> c) ~= Either a b → c.

мощность этого множества будет m^n

конечно:) спасибо за поправку

если вспомнить математику, то по определению функция (одно из) — это отношение, то есть множество пар, в котором левые части уникальны

absurd — пустое множество, валидная функция

именно это и записывается на Хаскелле как \case{}

если вспомнить математику, то по определению функция (одно из) — это отношение, то есть множество пар, в котором левые части уникальны

Нельзя просто так редуцировать теорию множеств в теорию типов над тьюринг-полными языками, потому что у тебя не все термы нормализируемы. Тебе нужна Scott domain theory, если ты хочешь об abdurd'е порассуждать

Void -> a начальный объект группы, a -> Void — терминальный

терминальный скорее будет a -> ()

если вспомнить математику, то по определению функция (одно из) — это отношение, то есть множество пар, в котором левые части уникальны

Это при условии, что каким-то волшебным образом определено декартово произведение.

Нельзя просто так редуцировать теорию множеств в теорию типов над тьюринг-полными языками, потому что у тебя не все термы нормализируемы. Тебе нужна Scott domain theory, если ты хочешь об abdurd'е порассуждать

ок, спасибо за наводку

Это при условии, что каким-то волшебным образом определено декартово произведение.

в теории множеств оно естественным образом определено (a, b) = {{a}, {a, b}} A × B = {(a, b) | a ∈ A, b ∈ B}

добродень)

у меня очередной глупый вопрос, а именно - Haskell получше чем OCaml будет?))

В каком смысле получше?

в смысле чем окамл (С)

1) приятная разработка - быстрая 2) быстродействие на сервере

нет SMP

я прост на гитхабе надыбал криптовалюту на окамле ? задался вопросом - почему на нем написали ( tezos, если интересно )

если ты хочешь писать на coq и пилить его, то лучше смотреть на ocaml

если что-то другое, то наверное не стоит

тут есть авторы кардано, которые написали на haskell

понял, спс)

вообще на окамле периодически вылезают интересные вещи связанные с верификацией

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