но ведь в идрисе у 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

понял, спс)

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

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

а у кого-нить наработались хорошие подходы к CRUD (вроде так зовется) и т.п.

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

возможно, postgrest ?

php*admin? (phpmyadmin, phppgadmin)

postgrest - для любителей писать plpgsql

postgrest неплох, правда было бы лучше, если б он в виде либы поставлялся, а не как монолит (например, меня тамошняя модель авторизации ну совсем не устраивает, и заменить её будет не так просто)

phppgadmin норм, но если бы он был на haskell или другом компилируемом языке

ну если это для админов, то вполне сносно

не, тащить php это вообще не вариант

ну если это для админов, то вполне сносно

Для админов не нужно, ибо любой нормальный админ знает SQL. Это ж скорее для кодеров сделано, которые не могут себе позволить ни DBA, ни даже тупо администратора.

тогда можно в idea запросы писать

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

доступ рабочей к базе idea разработчика, это интересно

есть ещё heidisql, но это опять таки полноценный SQL клиент где можно всё

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

таких историй вагон)

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

Это сейчас модно, у гитлаба базу дропали

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

Это не всегда возможно

не спорю, но можно пример?

Несложно организовать такой доступ, если схема БД предполагает собой 3'юю (а то и выше) нормальную форму. Но как известно никто не придумал СУБД, в которой за нормализацию не требовалось бы платить скоростью работы. Если база сильно денормализованная и обширная, с большим количеством реляций, то и создать искусственную версию, да ещё и поддерживать её в актуальном состоянии, очень сложно

Кстати я тут стал задумываться в последнее время — можно ли на уровне Type Theory гарантировать третью, четвёртую, пятую нормальные формы?

ну это к вопросу наполнения данными, он открытый особенно если от данных много что зависи

но вроде как не жесткое ограничение

если в этой Type Theory выражается идея функциональной зависимости (которая идёт от 2-НФ), и сначала описываются все возможные функциональные зависимости — то можно

(и, возможно, даже можно будет синтезировать по этим функциональным зависимостям классы нормальных форм для той или иной предметной области)

параллельная тема про Type Theory в РСУБД (если вдруг не видели): https://arxiv.org/abs/1607.04822 — парни на HoTT опиывают семантику SQL до такой степени, что говорят о классах эквивалентности запросов (с потенциальным выхлопом для оптимизации)