AG
(exists x:int, x>0, x<4)Size: a a a
2021 April 29
EL
Идея для сайд-проекта: Haskell-like синтаксис, способный однозначно выразить идиомы из программирования и большей части математики
AG
это вы сейчас агду изобрели
EL
forall (x:int|x > 1) {x > 0}EL
Или
forall (x|int x|x > 1) {x > 0}
Если считать "принадлежность к типу ~ условие"AG
ну это дополнительный сахар
AG
с конструктивной точки зрения вы говорите "дайте мне x и свидетельство того что он больше единицы, а я вам отдам свидетельство того что он больше нуля"
AG
т.е. это функция от двух аргументов
AG
существование это соответственно "у меня есть тройка из x, свидетельства того что он больше нуля и свидетельства того что он меньше четырех"
AG
т.е. трехместный тупл
AG
оба квантора связаны каррированием так же как им связаны функции и туплы
s
tldr dependent sum & dependent product
EL
А вот и категористы подъехали
AG
я предпочитаю абстрактные pi/sigma, связь с категорными произведениями и суммами поначалу только запутывает, потому что названия "смещены" :)
AG
ну если влазить в типы, без категорий не обойтись, это аналог пресловутой теории моделей для них
AG
это конечно если влазить именно в "механизм" типов, для формализации высказываний на них оно необязательно
EL
Кажется кто-то опять до восьми утра просидит в википедии и nLab...
EL
Есть какие-то концепты, которые плохо/сложно выражаются в парадигме "everything is a function" или "everything is a list"?
EL
И есть ли ещё какие-то *фундаментальные типы*, которыми можно выразить всё?
inb4: "просто посмотри публикации по Curry-Howard"
inb4: "просто посмотри публикации по Curry-Howard"
s
Да, коуравнители.