PP
я хз что за нортон коммандер и какое отношение к программированию он имеет
Size: a a a
2020 August 14
p
Это не важно. это называется IDE. Языки программирования изначально расчитаны на то, что код будет написан текстом, а это потому, что так его быстрее написать, чем накликать
isValidString : (s : String) -> Dec (ValidInput (unpack s))нажимаю хоткей create function initial pattern match clause, идрис генерирует:
isValidString : (s : String) -> Dec (ValidInput (unpack s))удобно? удобно. не нужно бойлерплейт писать.
isValidString s = ?isValidString_rhs_1
CD
Это не важно. это называется IDE. Языки программирования изначально расчитаны на то, что код будет написан текстом, а это потому, что так его быстрее написать, чем накликать
Как только IDE начинает использоваться для генерации кода, это означает, что в языке что-то прямо таки уже нафигачено. Например, в Java будут всякие Clone дергать из IDE, поэлементные конструкторы дергать из IDE
CD
isValidString : (s : String) -> Dec (ValidInput (unpack s))нажимаю хоткей create function initial pattern match clause, идрис генерирует:
isValidString : (s : String) -> Dec (ValidInput (unpack s))удобно? удобно. не нужно бойлерплейт писать.
isValidString s = ?isValidString_rhs_1
Это решает проблему, которая возникает из-за самого дизайна Idris
CD
Почему это просто не отдано командой компилятору, зачем она раскрыта в код как шаблон
RP
Т-34 85
Переслано от Roman na
вот эта падаль, что там тусуется и называется "крестовиками" - вот это адепты скриптухи
а где у него там пукан рвет?
CD
p
Это решает проблему, которая возникает из-за самого дизайна Idris
а вот так:
из
из
isValidInput' : (cs : List Char) -> Dec (ValidInput cs)получаем за три хоткея
isValidInput' : (cs : List Char) -> Dec (ValidInput cs)
isValidInput' [] = ?isValidInput'_rhs_1
isValidInput' (x :: []) = ?isValidInput'_rhs_3
isValidInput' (x :: (y :: xs)) = ?isValidInput'_rhs_4
Если выражаться в с++, то тут сгенерировалось три условияCD
смотри как удобно в go
p
это не то
CD
видишь, прямо язык за тебя код пишет
p
тут ты пишешь идентичный код для разных типов
A
навеяло уроками информатики в 99-ом
CD
тут ты пишешь идентичный код для разных типов
тут ты разворачиваешь некоторый шаблон
PP
это только подтверждает что женерики не нужны
p
а идрис позволяет просто генерировать бойлерплейт который бы ты все равно писал и так и так
CD
а идрис позволяет просто генерировать бойлерплейт который бы ты все равно писал и так и так
почему? я мог написать команду macro(boilerplate) в самом идрисе и этот код бы генерировался компилятором, а не IDE
CD
он же все равно сгенерирован
p
Почему это просто не отдано командой компилятору, зачем она раскрыта в код как шаблон
всмысле отдано командой компилятору? это раскрывает как раз компилятор
CD
всмысле отдано командой компилятору? это раскрывает как раз компилятор
да, только зачем раскрывать макросы