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

пусть считает как хочет, жалко что-ли

Я не знаю, когда программист на динамическом языке пишет код он не думает о каких-то мифических тегах, он думает о типах, он работает с типами и ему пофиг как это реализовано.

потому, что он называет тег типом

т.к. не знает что такое тип

не думает он о типах, он думает о тегах. что такое типы он чаще всего вообще не знает

На самом деле, интересный вопрос, как отделить статические проверки от степени функциональности. То что системы типов и тайпчекеры наиболее развиты в тех языках, которые считаются провославными в отношении ФП - это можно рассматривать как совпадение (помимо очевидного набора свойств благприятствующих реализации проверок)

В статических языках вы тоже называете тег типом, мы чуть выше уже это выяснили.

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

(последнее сраведливо и для большинства программистов)

в чате js никто этого требовать не будет

Ну что вы такие нетолерантные к чужому мнению

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

(читают, и тоже имеют свое нетолерантно воспринимаемое чужое мнение)

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

В статических языках вы тоже называете тег типом, мы чуть выше уже это выяснили.

Потому что и кошку, и собаку можно назвать "животное". Так же как типы и рантайм-метки можно назвать "тег"

Предлагаю считать ФП - те языки, у которых существует простая и компактная денотация в абстрактные математические функции (лямбда исчисление)

тип: компайл-тайм тег для тёрма "динамический тип": рантайм тег для значения

В статических языках вы тоже называете тег типом, мы чуть выше уже это выяснили.

нет, это не мы называем тег типом, а вы в своей аналогии называете тип - тегом.

Чем с большим скрипом дается описание денотационной семантики - тем меньше язык ФП

Предлагаю считать ФП - те языки, у которых существует простая и компактная денотация в абстрактные математические функции (лямбда исчисление)

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

специально в кавычках, потому что термин противоречивый

а поэтому проще назвать это просто тегом

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

* разновидность статического анализа до тех пор, пока не появляется какой-то ad hoc полиморфизм, будь то тайпклассы или трейты

ну да, тогда кодогенерация добавляется

*статического, лол

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

Нормальные жсники (типа меня) вспомнят про TypeScript у которого тип переменной на этапе компиляции и то что в ней лежит в рантайме могут не совпадать вообще. Так что это уже не одно и тоже.

вот у вас подгорело то. развели как детей

вот у вас подгорело то. развели как детей

точно

не уверен, что подогрело

Мысленный эксперимент. Возьмем компилятор хаскелля. Проапдейтим таким образом, чтобы типы игнорировались. Оставим недоопределенный код как "недопарсенный санк". Начнем выполнять те участки, которые можно выполнить. При наступлении на переменную будем допарсивать тип, доопределять словари, догенерировать код. и тайпчекать. Это возможно? Если да, то будет ли это типами?

у меня горит

это "в интернете кто-то не прав"

Мысленный эксперимент. Возьмем компилятор хаскелля. Проапдейтим таким образом, чтобы типы игнорировались. Оставим недоопределенный код как "недопарсенный санк". Начнем выполнять те участки, которые можно выполнить. При наступлении на переменную будем допарсивать тип, доопределять словари, догенерировать код. и тайпчекать. Это возможно? Если да, то будет ли это типами?

это называется -fdefer-type-errors

у Haskell есть defer-type-errorz

нет, это не типы уже

-fdefer-type-errors отключает типы

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

и вставляет error "bububu"

где не чекнулось, с ошибкой тайпчеккера

Мысленный эксперимент. Возьмем компилятор хаскелля. Проапдейтим таким образом, чтобы типы игнорировались. Оставим недоопределенный код как "недопарсенный санк". Начнем выполнять те участки, которые можно выполнить. При наступлении на переменную будем допарсивать тип, доопределять словари, догенерировать код. и тайпчекать. Это возможно? Если да, то будет ли это типами?

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

типы от имплементации не зависят, но описанная система не является имплементацией типов

Секция 1.1, "Type theory versus set theory"

Кстати, какой бекграунд для этой книги нужен? А то я пытался читать - сложно

-fdefer-type-errors отключает типы

не отключает, просто генерирует код не как обычно

И вот у слова Т И П в computer science тоже есть класс явлений, которые им называются, и те, которые им не называются. Даже если похожи. Если в рантайме — всё, не тип

В CS работая с типами мы вообще игнорируем существование и рантайма, и компайлтайма, у нас их нет, у нас есть сущность для которой верно единственное условие "Тип это то, что может в себе что-то содержать" и потом уже вводим необходимый нам перечень типов, операции над ними и т.д. CS вообще не про рантайм и компайлтайм, это когда вы CS прекладываете к чему-то, там к разработке компиляторов, к проектированию программ вот тогда у вас всё это появляется до этого этого нет, а типы всё ещё есть. Компиляции нет, а типы есть.

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

> Тип это то, что может в себе что-то содержать вообще-то нет

> stack new now allows template names of the form username/foo to download from a user other than commercialstack on Github, and can be prefixed with the service github:, gitlab:, or bitbucket:. Так сломим царство гитхаба ростовщического. Только в такие инструменты не стыдно веровать.

то есть вместо кода надо вводить что-то похожее на урл, но не урл?

тип - это то что справа от :

это множество - "может в себе что-то содержать"

Кстати, какой бекграунд для этой книги нужен? А то я пытался читать - сложно

бамп

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

это было несколько лет назад, мой бекграунд был на уровне "умею на хаскеле писать" (наверное там же он и остался)

“умею на хаскель писать” имхо дофига какой бэкграунд. не думаю, что во всем чатике более нескольких человек имеют такой

> Тип это то, что может в себе что-то содержать вообще-то нет

Почему-то проклятые комьютерсаентисты вполне себе позволяют определять тип именно так, например, https://youtu.be/h53eFYkAN6I?t=7m31s

это было несколько лет назад, мой бекграунд был на уровне "умею на хаскеле писать" (наверное там же он и остался)

очень крутой программист строит из себя скромника

очень крутой программист строит из себя скромника

это не humblebrag, а факт, у меня очень поверхностные знания всего за пределами Haskell

очень крутой программист строит из себя скромника

КОНТРИБЬЮТОР В ГЭХЭЦЭ

из того же TAPL только ту же первую главу прочитал, которую скинул, а дальше распечатка так и валяется по теории категорий я понял, что такие категории и функторы, дальше уже не разобрался (всякие limits colimits не осилил) по HoTT прочитал только первую главу на Agda написал пару игрушечных программ на C++ писал в школе и из этого имею отдаленное представление о том, какова жизнь без GC и т.д.

то есть единственный реальный бэкграунд у меня в том, что я на Haskell пишу достаточно долго

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

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

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

только как я уже упоминал это не даёт гарантий того, что в переменной типа число не окажется строка в рантайме

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

и flow есть, но и то и другое это не теги в ja

js

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

так там динамический "тип" и статический тип не одно и то же, как и везде

и теги могут по факту отличаться от типов

Что есть рантайм?

С точки зрения включенного компьютера - все рантайм

Что есть рантайм?

С точки зрения работы тайпчекера он проверяет типы в своём рантайме.

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

они используются тут для иллюстрации более-менее типичных случаев

С точки зрения включенного компьютера - все рантайм

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

я не знаю как их можно спутать

т.е. компайл-тайм это рантайм компилятора

Давайте уже каждый обозначит свою позицию на диаграмме и закончим на этом

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

Хорошо, что мы это прояснили.

так там динамический "тип" и статический тип не одно и то же, как и везде

ну не везде, кстати говоря в той же Java к примеру просто невозможно нарушить типизацию

ну, рантайм кодогенератора и программы иной раз перепутать можно еще как

ну не везде, кстати говоря в той же Java к примеру просто невозможно нарушить типизацию

http://wouter.coekaerts.be/2018/java-type-system-broken

ну не везде, кстати говоря в той же Java к примеру просто невозможно нарушить типизацию

да, но из-за сабтайпинга разница между типами и тегами есть, все равно