То есть показать, что число входить какой-то диапазон, это уже непростой случай.

Я не говорю уже о свойствах каких-то операций, а просто о констрейнте на входные или выходные данные.

Мне сложно представить себе доказательство чего-либо без зависимых типов или refinement-типов или беспощадного использования TypeFamilies+GADTs

И в последнем случае это не "отлично" строить доказательства, а "мучительно"

Мне сложно представить себе доказательство чего-либо без зависимых типов или refinement-типов или беспощадного использования TypeFamilies+GADTs

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

в теории доказательства строятся на мета-языке

Как можно "отлично" строить доказательства без завтипов?

В Isabelle/HOL нет завтипов, а док-ва строят. Даже на верифицированную ОС набралось + куча всяких библиотек по формализации всего и вся.

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

У них есть книга “Concrete Semantics” — довольно легко читается (это если интересует применение Isabelle к ProgLangTheory)

книжка в свободном доступе

А еще у Isabelle есть IDE 😉 (закончу оффтоп)

а что за "чат про тапл"?

deptypes?

А расскажите поподробнее, что за история с неправильным пониманием тайпклассов?

> Wadler conceived of type classes in a conversation with Joe Fasel after one of the Haskell meetings. Fasel had in mind a different idea, but it was he who had the key insight that overloading should be reflected in the type of the function. Wadler misunderstood what Fasel had in mind, and type classes were born!

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

http://lambda-the-ultimate.org/node/3858#comment-58029 коротенький тред про принцип работы isabelle от neelk

а что за "чат про тапл"?

вижу уже нашел, но вдруг кому надо будет https://t.me/joinchat/A8_s30LVQrNmQWBlBlJUKw

> Wadler conceived of type classes in a conversation with Joe Fasel after one of the Haskell meetings. Fasel had in mind a different idea, but it was he who had the key insight that overloading should be reflected in the type of the function. Wadler misunderstood what Fasel had in mind, and type classes were born!

Хех, забавно! Спасибо.

странно, а вот его мне не добавить

В "Завтипы в массы" и в "TAPL" добавился. Есть ещё какие-то?

нету больше

@A64m_qb0 А вы, случаем, не можете посоветовать, что обзорного почитать по последним достижениям в доказательствах теорем за последние лет 10?

только я нигде не видел что на самом деле это Джо Фейзел придумал-то. в самом первом письме вадлера про тайпклассы https://homepages.inf.ed.ac.uk/wadler/papers/class-letter/class-letter.txt , он только пишет что идея тоже подразумевала указание класса в схеме типа, т.е. Вадлер перешел от эмельной перегрузки в (1) к (2) под влиянием интерпретации этой идеи, но в чем она заключалась нигде не написано Ж(((

@A64m_qb0 А вы, случаем, не можете посоветовать, что обзорного почитать по последним достижениям в доказательствах теорем за последние лет 10?

не могу, я этим не увлекаюсь

@A64m_qb0 А вы, случаем, не можете посоветовать, что обзорного почитать по последним достижениям в доказательствах теорем за последние лет 10?

https://ru.m.wikipedia.org/wiki/Воеводский,_Владимир_Александрович

Наслышан. Что конкретного обзорного почитать у него?

Посмотри видео, поищи

Я из телефона, у него хорошие видео intro

Спасибо, поищу.

https://www.youtube.com/watch?v=l79c_OqEjZI

Оно?

Это он там про HoTT расказывает же, да?

Нет это про то что он сам занимался, открыл

Так он HoTT и придумал 🙂

хотя и не только HoTT

@qnikst этих QQ расплодилось уже много

?

Спам

Надо бота прикручивать

2шт

капец, вчера вечером только кикнул десяток, сегодня уже штук 30 забежало

Позабыты хлопоты, остановлен бег, Вкалывают роботы, а не человек.

я смотрю, хвр теперь и гхцжс-ы собирает

а чего за мода в кафе стала непроверенный код писать, и вообще странные вещи?

всегда была

бытие рассылкой больше не является блокирующим фактором?

да раньше казалось как-то получше было

или у меня просто болит голова и я сегодня злой

что, совсем плохо стало? я последнее время кафе не читаю

ну как-то неприятно

появились большое число тривиальный вопросов (нормально), с большим числом тривиальных ответов (не очень)

ask a silly question and you get a silly answet

@weonn приди, добавь в чат @Cyberdyne_Systems_bot и дай ему админку

done

\o/

сейчас на одного китайца будет 10 мусорных сообщений с приветствиями

а бот на сабже написан?

Господа, а не подскажите, как вы кэш в веб-сервисах делаете? Можно, наверно, такой пример привести: с одной стороны база, с другой стороны scotty. На тяжёлые запросы не хочется сильно часто ходить в базу. Можно это реализовать несколькими способами. Интересны ваши подходы.

Так же, как и везде - redis.

TVar ?

зависит от, отпростого Map, или Map на Tvar или Lrucache до редиса

или lmdb

redis реже

Привет ребята, Можно ли написать такую общую функцию h, из этих двух? типа объединить в одноу h :: Int -> (Int -> Maybe Int) -> Maybe Int -- h _ Nothing = Nothing h a b = b a h2 :: Int -> (Maybe Int) -> Maybe Int h2 _ Nothing = Nothing чтобы было так: h 5 Just == Just 5 h 5 Nothing == Nothing

И на сколько я отклонился от ФП парадигмы захотев написать такую функцию?

foo x m = x <$ m ?

не вижу в чем проблема хотеть такое написать

<$ - живёт в Data.Functor

Прикольно спс, буду изучать)

@qnikst в случае с <$ надо будет 5 <$ Just (), а не 5 <$ Just, это не то же самое

Но и Nothing не Int -> Maybe Int

да, но в определении h там матчинг на Nothing закомменчен

Тут главный вопрос: зачем?

что-нибудь типа x & _Just .~ y не прокатит?

что-нибудь типа x & _Just .~ y не прокатит?

Опять не то же самое, у тебя x должно быть Just (), а не Just

это эквивалент <$

@kwas000 будет жить. Поприветствуем!

а, он вот что хочет...

тогда да, вопрос зачем :)

> h 5 Just == Just 5 h 5 Nothing == Nothing тут просто типики не сходятся

понятно, что там Just _

но всё же

так вопрос про то, как перегрузить, чтобы типы сошлись