Omarov
Где эти символы просто найти
Omarov
Юникод?
afalex
Прикольно)
Андрей
Я вот хочу как-то так писать
takeWhile : ∀ {ℓ} {A : Set ℓ} → (A → 𝔹) → 𝕃 A → 𝕃 A
takeWhile _ [] = []
takeWhile f (x :: xs) = if f x then x :: takeWhile f xs else []
takeWhile∘repeat : ∀ {ℓ} {A : Set ℓ} (n : ℕ) (a : A) (f : A → 𝔹) → f a ≡ tt →
takeWhile f (repeat n a) ≡ repeat n a
takeWhile∘repeat 0 a f p = refl
takeWhile∘repeat (suc n) a f p with keep (f a)
... | ff , p' rewrite p' = 𝔹-contra p
... | tt , p' rewrite takeWhile∘repeat n a f p | p' = refl
И тут возникаю траблы, как в VS сделать мнемоники для используемых уникодных символов.
Выглядит одновременно красиво и страшно, страшно от того, что одни мнемоники
afalex
И кванторы есть )
Andrii
Где эти символы просто найти
У меня в vim настраено в плагине
https://github.com/derekelkins/agda-vim/blob/master/autoload/agda.vim
Просто нажимаешь ,forall он заменяет на ∀
afalex
Очень прикольно, и читается легко
Omarov
Omarov
Прям жосска
Omarov
На древнегреческом писать
Andrii
Зависимые типы это когда у нас есть функция двух аргументов, и тип второго аргумента может зависеть от значения первого
Omarov
afalex
Таблица математических символов — Википедия
https://ru.wikipedia.org/wiki/%D0%A2%D0%B0%D0%B1%D0%BB%D0%B8%D1%86%D0%B0_%D0%BC%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B8%D1%85_%D1%81%D0%B8%D0%BC%D0%B2%D0%BE%D0%BB%D0%BE%D0%B2
Omarov
Зависимые типы это когда у нас есть функция двух аргументов, и тип второго аргумента может зависеть от значения первого
Что такое функция двух аргументов? Это же не функция с двумя аргументами?
Игорь
Нейросетку на Java сложно запилить, как считаете?
afalex
Нейросетку на Java сложно запилить, как считаете?
Простую написать- сложных конструкций языка не потребуется
Andrii
∀ {ℓ} {A : Set ℓ} вот это интересное. Есть множество типов. Возникает вопрос, а тип типов должен принадлежать типу всех типов? Парадокс Рассела, это приводит к противоречиям... Поэтому в Agda есть иерарзия типов, Set 1, Set 2, Set 3, ...
Andrii
Что такое функция двух аргументов? Это же не функция с двумя аргументами?
Да, функция с двумя аргументами. Но первый аргумент, например целое число n. А второй аргумент это вертор длины n, например. Или первый аргумент это формат. Остальные аргументы определяются этим форматом. По сути можно написать свою функцию printf в проверкой соответствия параметров шаблону на этапе компиляции
Omarov
Да, функция с двумя аргументами. Но первый аргумент, например целое число n. А второй аргумент это вертор длины n, например. Или первый аргумент это формат. Остальные аргументы определяются этим форматом. По сути можно написать свою функцию printf в проверкой соответствия параметров шаблону на этапе компиляции
Тебе бы в политику вместо Зеленского
Andrii
Ну и в зависимых типах доказательство это тип. Поэтому, например, если у нас есть вектор длины n. То когда мы получаем i-й элемент, то можно либо возвращать Maybe и там Nothing если индкс за пределами диапазона. А второй пусть принимать два параметра, первый i а второй доказательство того, что 0 ≤ i < n
afalex
∀ {ℓ} {A : Set ℓ} вот это интересное. Есть множество типов. Возникает вопрос, а тип типов должен принадлежать типу всех типов? Парадокс Рассела, это приводит к противоречиям... Поэтому в Agda есть иерарзия типов, Set 1, Set 2, Set 3, ...
Для любого l из множества l обозначаемого как A. Может должно быть: Для любого элемента l из множества A
∀ {ℓ} {ℓ : Set A}
?
Omarov
Cr3sta
Ну там реально специалисты нужны, зона ответственности большая очень. Все таки бухгалтерия, налоги и тп) не думаю
Omarov
Ну там реально специалисты нужны, зона ответственности большая очень. Все таки бухгалтерия, налоги и тп) не думаю
Вот есть Андрий, рубит 6к, а есть не Андрий, пишет на реакт, зарабатывает 6к
Andrii
Для любого l из множества l обозначаемого как A. Может должно быть: Для любого элемента l из множества A
∀ {ℓ} {ℓ : Set A}
?
Нет, тип ℓ будет выведен, а A это некоторый тип уровня ℓ
Например, разберём
data 𝕍 {ℓ} (A : Set ℓ) : ℕ → Set ℓ where
[] : 𝕍 A 0
_::_ : {n : ℕ} → A → 𝕍 A n → 𝕍 A (suc n)
Это вектор, коорый принимает уровень типа, некоторый тип этого уровня, натуральное число и сам является типом уровня ℓ
для которого определён пустой вектор и добавление к вектору некоторого элемента
Andrii
А насколько это актуально сейчас?
Ну... исследования активно ведуться, но писать, похоже, некому...
Andrii
nth𝕍 : ∀ {ℓ} {A : Set ℓ}{m : ℕ} → (n : ℕ) → n < m ≡ tt → 𝕍 A m → A
nth𝕍 0 _ (x :: _) = x
nth𝕍 (suc n) p (_ :: xs) = nth𝕍 n p xs
nth𝕍 (suc n) () []
nth𝕍 0 () []
А вот получение n-го элемента, там пятым памаметром принимается доказательство того, что индекс правилен
afalex
Прикольно, я бы пописал
Andrii
А насколько это актуально сейчас?
Вообще, чистые функциональные языки часто в финтехе используются, но а Украине не развито. Как обычно, нет специалистов, потому что нет проектов, а проекты не заходят потому что нет специалистов
afalex
nth𝕍 : ∀ {ℓ} {A : Set ℓ}{m : ℕ} → (n : ℕ) → n < m ≡ tt → 𝕍 A m → A
nth𝕍 0 _ (x :: _) = x
nth𝕍 (suc n) p (_ :: xs) = nth𝕍 n p xs
nth𝕍 (suc n) () []
nth𝕍 0 () []
А вот получение n-го элемента, там пятым памаметром принимается доказательство того, что индекс правилен
Красиво довольно ) видно что математики придумали )
Andrii
Прикольно, я бы пописал
Мне тоже прикольно, я изучаю, но до не всегда есть время и там есть тонкие места :)
Andrii
А почитаешь дискорд сепциалистов — уши заворачиваются
Omarov
Вообще, чистые функциональные языки часто в финтехе используются, но а Украине не развито. Как обычно, нет специалистов, потому что нет проектов, а проекты не заходят потому что нет специалистов
Мне интересно одно. Вот ты заходишь в этот чат. Вот читаешь беседы. Вот новички задают вопросы. А ты знаешь ответы на все вопросы. Всегда. В чем прикол?
Andrii
Просто расслабится, может порекламировать что-то что считаю интересным. Типа проповедовение ценностей
afalex
Кстати чат реально помог подрасслабиться после кровавого энтерпрайза)
Mikhail
Мне интересно одно. Вот ты заходишь в этот чат. Вот читаешь беседы. Вот новички задают вопросы. А ты знаешь ответы на все вопросы. Всегда. В чем прикол?
Кто-то пьет, кто-то нарктоики употребляет, кто-то в чатах сидит.
afalex
О математике аж вспомнил с agda
Andrii
Опять же, выходной, дети у бабушки, можно посмотреть стримы, неспешно в чате поболтать
afalex
А есть тут те кто понимает прелесть хранения логики всей предметной области в хранимых процедурах?
Omarov
*тут фотография с косяком и стаканом виски на фоне чата*
Учитывая твое местонахождение, не удивлюсь)
Mikhail
А есть тут те кто понимает прелесть хранения логики всей предметной области в хранимых процедурах?
Собеседовался в одну компанию лет 6 назад, у них вся логика на хранимых процедурах была. Как только узнал, сразу прекратили собеседование.
afalex
Mikhail
Правильно сделал. Это ад)
Ну они собирались как раз мигрировать и искали тимлида под все это дело. Возможно даже нашли кого-то.
Mikhail
Там еще и финтех был. Можешь себе представить объем работы.
Andrii
Ага.
Ну... Так рекомендует сам Оракл и его проповедники... В целом там всё заточено для этого, и сам PL-SQL сдёрт из языка Ada :)
Mikhail
Ну... Так рекомендует сам Оракл и его проповедники... В целом там всё заточено для этого, и сам PL-SQL сдёрт из языка Ada :)
Конечно Оракл будет рекомендовать, это же сколько денег можно на поддержке этого всего заработать.
afalex
Вообще хороший плюс таких работ в том что вынужденно sql нормально прокачиваешь) форсированно )
Mikhail
Я бы тоже рекомендовал, если бы работал в Оракле.
Mikhail
Но слава Б-гу обошлось.
Andrii
Вообще хороший плюс таких работ в том что вынужденно sql нормально прокачиваешь) форсированно )
PL-SQL, это отдельный язык по сути. Вопрос больше в том, что сейчас как-то не очень популярно и тяжело найти специалистов
afalex
PL-SQL, это отдельный язык по сути. Вопрос больше в том, что сейчас как-то не очень популярно и тяжело найти специалистов
Я пытался мотивировать знакомых качать sql, но не вышло )
afalex
Так что думаю да, тяжело )
Andrii
Ну а если ты не юзаешь PL-SQL, то зачем тебе Oracle? Юзай любую базу
afalex
PL-SQL, это отдельный язык по сути. Вопрос больше в том, что сейчас как-то не очень популярно и тяжело найти специалистов
Я сонный уже, имел ввиду под sql все проприетарные надстройки типа tsql/plsql и тд
Andrii
Я пытался мотивировать знакомых качать sql, но не вышло )
Это не SQL, у Oracle это язык, где SQL смешан с операторами Ada.
Andrii
Чем тебе не Ada?
DECLARE
past_due EXCEPTION;
acct_num NUMBER;
BEGIN
DECLARE ---------- sub-block begins
past_due EXCEPTION; -- this declaration prevails
acct_num NUMBER;
BEGIN
...
IF ... THEN
RAISE past_due; -- this is not handled
END IF;
END; ------------- sub-block ends
EXCEPTION
WHEN past_due THEN -- does not handle RAISEd exception
...
END;
afalex
Ещё бы я знал Ada)
afalex
Andrii
Ещё бы я знал Ada)
Была книжка Гаввы хорошая, а в последнем стандарте добавили контракты под влиянием Eifell и верификацию, в общем-то достаточно интересная вещь для императивного кода, я сильно понимаю, почему оно не сильно заходит
https://blog.adacore.com/verifythis-challenge-in-spark
Andrii
Кто-то пьет, кто-то нарктоики употребляет, кто-то в чатах сидит.
https://maps.org/news-letters/v18n1/v18n1-MAPS_24.pdf
Dmitriy
Dmitriy
afalex
В href сунь ссылку
Dmitriy
пробовал
Dmitriy
не фурычит))