Как стать автором
Обновить
36
0

Программист-теоретик

Отправить сообщение
Я встречал перевод «sound» как «надёжный». Но это маргинально.
Для тех, кто не в теме, что это за возможность такая? Как рассахариваются несколькострочные конструкции, если функция не удовлетворяет естественным квадратам? Или там единственное отличие состоит в отсутствии требования к наличию fmap?
Это свойства всех людей в большей или меньшей степени. Хабравчанам они тоже присущи, покуда они являются людьми.
ИМХО, эта подветка содержит одну рефлексию на гране перехода на личности и может сколь угодно отдалиться от исходной темы.
Форк порождает точную копию истории, которая может со временем разойтись с оригиналом.
А здесь просто мерж в мистресс^W мастер.
Вообще самая удивительная вещь во Вселенной — то, что она существует.
Это предмет веры. И есть те, кто это не разделяет. Или «существование» надо понимать как-то нестандартно.

Но если верить в бытие Вселенной, то это действительно чудесно.
Не ради рекламы замечу, что в дискорде каналы куда приятнее читать, в первую очередь из-за обилия ботов, которые и код с IO подсветят и исполнят, и tex картинкой покажут и спам удалят.
Насколько мне известно, лишь немногие немейнстримовые языки могут похвастаться поддержкой зависимых типов. На этом фоне вменять скале как языку своей эпохи это в вину странно. Но да, их не хватает.
На хабре тоже никто не комментирует статьи годовалой давности.
Комментируют, но хабр не предоставляет инструментов для удобного выявления этих комментариев. По факту только автор статьи, те, кто комментировал статью или подписался на неё, и случайные захожане будут уведомлены.
Я думаю, люди это понимают и потому количество оставленных комментариев существенно меньше, чем могло бы быть. Но даже так они есть.
Я говорил не только про gradual typing, хотя этот подход является частным случаем.

Общая задача gradual typing и иже с ним (напр., threesomes) пытается сдружить типизированный код и нетипизированный. Грубо говоря, gradual typing предоставляет возможность локально положить болт на надёжную (sound) систему типов, чтобы затем проверять контракты в рантайме. По моим представлениям это исходно порочный подход, если только не в связи с задачей миграции, о которой говорится в лекции.

Я же говорил о том, чтобы использоваться явную систему типизации (т.е. ту, в которой тип является частью грамматики языка), которая позволяет не писать типы, если в этом нет необходимости (в противовес всем системам типов лямбда-куба, где типы необходимо указывать для каждой переменной). Как пример, в Java появился var, в Haskell изначально был Хиндли-Милнер.

Мысль простая, но судя по комментариям многие считают, что явная система = необходимость (а не возможность) писать типы явно.

P.S. спасибо за ссылки.

upd. а мог бы оставить ссылку на ту же мысль, выраженную другими словами.
Но если за эту часть отвечает вручную написанная программа, то нет, правила построения модели заложены извне программистом.
Позанудствую: в Вашем первом определении и не требуется, чтобы ИС могла строить то (программу, алгоритм), что строит модель; требуется, что она сама могла строить модель. Поэтому даже если правила построения модели заложены извне, а сама ИС умеет только строить модель, то уже под определение подходит.

Но кажется, Вы готовы наделить интеллектом почти любую систему с оговоркой, что её уровень низкий:
Уровень интеллекта это количественная характеристика (больше/меньше), а не качественная (есть/нет).
В цитате речь идёт о неконтролируемом и вредном для вычислителя/пользователя взаимодействии кубита со средой. Это аналогично проблеме классических устройств, вроде размагничивающего фактора. В КК временные интервалы меньше — сложнее удержать кубит в одном состоянии.
Касаемо прикладного (контролируемого) взаимодействия вычислителя с окружающей средой, то тут я не теме, но судя по размерам текущих прототипов, в качестве окружения выступает классический вычислитель.
Не, тут сработал закон Мерфи: единственная непроверенная пара дала сбой.
Но даже ребёнок 4-6 лет уже интуитивно понимает, что такое «подножие холма» или «голова колонны».
Мне кажется, оно так не работает. Интересно было бы увидеть экспериментальные данные.

Когда я начал рефлексировать над своим языком(~4-5 лет было), очень удивился, что многие слова с очевидно разным смыслом в известном мне употреблении оказались этимологически связаны. Мне рано объяснили, что бывают созвучные или похожие (в местном произношении) слова, которые не связаны по смыслу или происхождению, например, «лев» и «левый», «замок» и «замок», «надо» и «надежда». Поэтому большинство этимологически родственных слов я воспринимал как просто разные, особенно, если связь смысла не прослеживалась очевидным (без ad-hoc измышлений) образом, например, «устроить [жизнь]» и «построить [здание]». Так что я бы не был уверен, что все дети 4-6 лет интуитивно понимают связь слов «нога» и «подножье» (притом таковой нет у слов «рука» и «ружьё»).

Многие люди тоже не видят связи между многими родственными словами (напр., «объём», «нанять» и «вонмем») или наоборот приписывают связь там, где её нет (вспомним занимательную лингвистику Задорнова).
Возможно. Или я с годом ошибся.

Впрочем, уточню мысль: для ещё-вчера-noname языков нет ide, ибо жирно (дай бог чтоб кроме компилятора вообще что-то было), но жизнь заставляет с ними работать и рефакторить.
какой смысл вылезать из уютненькой идешечки? Вот если она не осиливает
Или если она не существует.
Если мы берём не язык из топ-20, такое вполне частое явление. Даже у JS до ~2010 не было иде. А sed/awk тащат любой текстовый язык.
с одной стороны будет максимально строгим (то есть гарантировать отсутствие рантайм-ошибок)
Если в число рантайм-ошибок включать зависание, то все Тьюринг-полные языки не подходят. А прочие ошибки (как-то деление на ноль) лёгким движением руки можно превратить в зависание, лишь немного изменив семантику языка.
Правды ради стоит отметить, что на практике нам не всегда нужны Тьюринг-полные ЯП.
в нем не будет никакого синтаксиса объявления типов так как он будет выводить и проверять все типы из кода?
Первые исследования систем типов проводились на лямбда-исчислении. А.Черч предложил (явную) простую систему типов, в которой тип был неотъемлемой частью функций. Х.Карри предложил эквивалентную (неявную) систему, в которой тип как языковая конструкция вводился только на этапе вывода, но не был синтаксическим элементом языка.
Так что да, существовать могут.
Общая идея неявных систем типов состоит в том, что тип возникает только на этапе проверки (вывода) типов подобно тому, как нетерминальные символы возникают только при описании грамматики/синтаксическом разборе, но не являются частью языка.
Как бы это странно не звучало, но в рамках подхода Карри JavaScript со сборщиком, который падает, если для каждой переменной не может быть однозначно выведен тип, вполне может считаться языком с неявной типизацией.
Возможность указать тип имеет тенденцию усложняться… в итоге внутри языка мы создаем еще один язык со своим синтаксисом но уже на типах
Тенденция усложняться связана не с возможностью указать тип, а с желаниями иметь мощную систему типов, позволяющая гибче абстрагироваться, сохраняя при этом строгость.
Если система типов явная, то да — язык типов в языке, так и задумано.
Если система типов неявная, то язык типов всё равно будет сложный, но сокрытый внутри тайпчекера.
Из плюсов: 1) текст станет чище от типов, 2) пользователю не нужно знать язык типов.
Из минусов: 1) невозможно передать тайпчекеру информацию относительно типов или их вывода (всё усугубляется требованием к тайпчекеру, чтобы он выводил типы за конечное время), 2) невозможно использовать типы в качестве схемы/интерфейса или как способ описания фрагмента предметной области.

В настоящее время, как мне видится, перспективным направлением является разработка гибридного подхода: чтоб была возможность указать тип или способ вывода, и чтоб была возможность не указывать ничего, и так для каждого выражения.
В математике так же.
Переменная — это символ, который принимает некоторое значение в контексте. Например, при вычислении x^2+2*x в контексте [x=3], скажем, при вычислении f(3) функции f(x)=x^2+2*x, значение x неизменно. Однако, мы называем x переменной, потому что она зависит от контекста.

Либо же в JS так говорят по привычке.

Информация

В рейтинге
Не участвует
Откуда
Красноармейск, Донецкая обл., Украина
Зарегистрирован
Активность