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

то есть понятно, что не с любой, но не то чтобы если в Haskell синтаксис стал а-ля Java, то для меня бы это стало катастрофой (не стало бы)

зачем презентация по недо-katip в этом чятике?

katip не умеет извлекать структуры автоматически из стринг интерполяций ...

то есть понятно, что не с любой, но не то чтобы если в Haskell синтаксис стал а-ля Java, то для меня бы это стало катастрофой (не стало бы)

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

т.е. я считаю позицию @int_index пр ряду вопросов правильной и полезной, но не по тому что можно увидеть глазами все предложения по тому, что можно увидеть глазами - заставляют мои глаза кровоточить

@int_index против хаскеля в продакшоне, так и запишем

katip не умеет извлекать структуры автоматически из стринг интерполяций ...

ну это ж не очень интересно? хотя может местами и полезно

ну это ж не очень интересно? хотя может местами и полезно

Почему не интересно? Большой минус к бойлерплейту

Меньше бойлерплейта - больше пишут логов

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

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

Контекст тоже тащится если ты об этом

katip не умеет извлекать структуры автоматически из стринг интерполяций ...

^

это добавление одного TH метода.

к существующему решению, который часть surface синтаксиса

а самое интересное со структурированными логами в другом (имхо)

причем TH или аналога, чтобы не было runtime cost

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

С reflection приходится всегда либо таскать прокси, либо ScopedTypeVariables+TypeApplications. У имплицитов есть киллер фича - в скоупе может быть только один имлпицит с одним именнем, то есть их можно использовать для тайп инференса

в рефлекшене тоже есть функциональная зависимость, что если Reifies s a, то s -> a, так что тайп инференс там не страдает а вот Proxy да, плохо, и еще без first-class existentials местами плохо

но выдиранием прокси занимаются as we speak

несколько пропозалов в этом направлении, пейпер недавно еще

я на самом деле плохо вижу почему там нужен type inference при написании логов, и так же (я не вижу почему из TH у нас не будет доступа к информации о переменной, т.к. она объявлена в другом блоке)

Например эмулировать ооп синтаксис: mkObj :: (Object a) => a -> (forall a'. (?curObj :: a', Object a') => r) -> r mkObj a f = let ?curObj = a in f class Object a where get :: (?curObj :: a) => IO Int x = do let obj = mkObj a <- obj get b <- obj get pure (a + b)

но может я неправильно помню про ТН, не часто этой фичпй пользуюсь

в рефлекшене тоже есть функциональная зависимость, что если Reifies s a, то s -> a, так что тайп инференс там не страдает а вот Proxy да, плохо, и еще без first-class existentials местами плохо

Эту s еще подать нужно. Если все типы параметризованы ей, то еще можно. А так постоянно писать @s на аппликациях

Да. А как ты еще будешь @s определять, если у тебя ее ни в типе нет, ни явно?

Очевидно. Просто я говорю о том что имплициты подаются по имени, поэтому вместо того чтобы подать @s чтобы прорезолвить оверлоад, можно наоборот выхватывать тип из имлпицита и делать оверлоад только по нему. То есть делать полностью контекстно-зависимые DSL'ки.

так s соответствует имени, а не типу

то есть ?curObj :: a это что-то вроде Reifies "curObj" a

s надо протаскивать вручную или выводить, потому что она локальная, а "curObj" это не переменная, а просто строчка тут две проблемы. первое в том, что это строчка, про это я уже жаловался и сегодня больше не хочу, допустим мы заменим это на data CurObj и Reifies CurObj получается что-то вроде Given-style reflection уже, то есть протаскивать s не нужно, но есть угроза когерентности

Да, но я могу написать obj get, а не obj (\(p :: Proxy s) -> get @s) where get :: forall s a. (Reifies s a, Object a) => IO Int; get = reflect (Proxy @s) & get

для Given-style reflection мне хотелось бы хорошую историю увидеть, то есть понятно, что give True (give False (expr)) это нонсенс, но вот give True expr && give False expr это ок, то есть надо как-то формализовать locally coherent, чего я не видел для Хаскеля

К тому же я могу оверлодать полностью, e.g.: class Object a r | a -> r where get :: (?curObj :: a) -> r data IntObj = IntObj data StringObj = StringObj instance Object IntObj (IO Int) instance Object StringObj (IO String) mkStringObj :: _; mkIntObj :: _; x = do a :: Int <- mkIntObj get b :: String <- mkStringObj get

я еще раз говорю, с implicit parameters две проблемы, — они основаны на строчках и они могут когерентность ломать про строчки — это можно исправить и ни один из примеров выше не сломается про когерентность — это присуще и Given-style reflection и обходится исключительно аккуратностью

имплиситные параметры можно выкинуть если решить проблему про когерентность, тогда любой адекватный пример смог бы переписать на reflection на сейчасшний момент не могу

то есть я верю, что имплиситные параметры можно хорошо применить, но мне от этого проще не становится

то есть ты пойди, возьми Refies, и убери там весь rank2 происходящий

просто в reify вынести forall s наверх

Но ведь в этом не будет смысла?

в этом будут имплиситные параметры

forall s создает синглтон

все примеры выше переписываются тогда на Reifies CurObj a вместо ?curObj :: a

потому что имплиситные параметры это и есть reflection, в котором s в refiy вытащили наверх

и приняли за него строчку

Ну в целом да.

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

Спасибо за идею!

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

так же как математики, которые помешаются там на какой-то конкретной системе счисления и начинают доказывать свойства про "суммы цифр" и т.д., как будто цифры это что-то релевантное, а не способ записи

в защиту математиков — задачки на "десятичные цифры" никогда не считались чем-то выше, чем уровень школьных олимпиад

да я видел как real numbers определяют как последовательность десятичных цифр

а потом задают equivalence class на этом

чтобы 0.9999... и 1.0 приравнять

да я видел как real numbers определяют как последовательность десятичных цифр

Это устаревшая традиция, и на матфаках так не определяют

приятно слышать

Это никогда не существовавшая традиция. В фихтенгольце (50'ые годы) вещественные определяются как дедекиндовы сечения. В крайном случае их конструируют как сходящиеся в себе последовательности

я еще раз говорю, с implicit parameters две проблемы, — они основаны на строчках и они могут когерентность ломать про строчки — это можно исправить и ни один из примеров выше не сломается про когерентность — это присуще и Given-style reflection и обходится исключительно аккуратностью

А зачем имплиситам когерентность? Оригинальная мотивация у них вообще dynamic scoping, который совсем не когерентен 🤔

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

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

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

Ну инженерам-то конечно. Удивительно, что вообще как-то определяют, а не дают как данность

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

Всё так, по-крайней мере Тер-Крикоров так делал. Но надо признать, что на физтехе не готовят математиков

ну конечно, пара человек тут ответили, что TLC вроде нормальная фича, но пропозал не минусанули

у нас через пределы в школе вводили

Хорошая школа

у нас через пределы в школе вводили

По коши?

Ты в 239 учился?

в АГ

Норм, до исхода ЮМШ или после?

не знаю

А ты в каком закончил?

2003 вроде или 2004

2004

ЮМШ убежало летом с 2003'ого по 2004'ый

я как-то не связан с ЮМШ был никак

вроде действительные вводятся аксиоматически через нерациональность корня из 2 и пределы, да. а по поводу позиционно-разрядной системы счисления - не Кантор ли в своих лестницах ее вовсю в доказательствах применял?

Ну они просто математику в АГ преподавали до 2005'ого

у нас преподы с матмеха и алгебру с ПМ вроде

вроде действительные вводятся аксиоматически через нерациональность корня из 2 и пределы, да. а по поводу позиционно-разрядной системы счисления - не Кантор ли в своих лестницах ее вовсю в доказательствах применял?

Аксиоматически ввести это значит не ввести. Нужно модель аксиоматики предоставить. Модель аксиоматики строят либо по Коши — через сходящиеся в себе последовательности, либо через дедекиндовы сечения. Есть извращённые способы, но они неучебные

Мне нравится Eudoxus reals из извращений

у нас через пределы в школе вводили

а это как? у нас только через десятичную запись и через аксиоматику

я не воспроизведу, если тетрадку не почитаю