Typescript: unsound behavior или поблажки надежности

[SirEdvin]

Типы могут доказать, что программа в целом безопасна

Это в каком-таком языке? В более-менее популярных остается куча проблем, от вызовов cast и null exception до panic или core dump при использовании сишных либ.

[buggy375]

Посмотрите на «Соответствие Карри — Ховарда» (перенесение мат логики на систему типов), где как пример «полиморфного λ-исчисления» приводится Haskell, "λ-исчислению с зависимыми типами" — Idris.
Более-менее популярные языки зашли с другой стороны.
Но, типы то могут, но не везде )

[SirEdvin]

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

[buggy375]

Посыл статьи — где конкретно TS не гарантирует безопасность. Вот проблема, код, ошибка, issue, рекомендация. Тут все ок или с каким-то примером не согласны?
Я не утверждал, что это полный список и закрыв его — проблем больше не будет.
Или вас из всего материала смутила фраза, что типы могут гарантировать безопасность?

[SirEdvin]

Или вас из всего материала смутила фраза, что типы могут гарантировать безопасность?

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

[SirEdvin]

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

[Aquahawk]

Всё там сказано. Читайте раздел non goals. https://github.com/Microsoft/TypeScript/wiki/TypeScript-Design-Goals

[Aquahawk]

В частности явно заявлено что не является целью: Apply a sound or "provably correct" type system. Instead, strike a balance between correctness and productivity.

[Vadem]

Об этом же написано в статье.

Design goals
Не цель для TS — Сделать систему типов с гарантией безопасности, вместо этого сконцентрироваться на балансе между безопасностью и продуктивностью

[Aquahawk]

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

[VladVR]

Про номинальное сравнение типов — я сейчас использую вот такие типы для id:

export interface CompanyId {
  companyId: string;
}

соответственно если случайно передать CompanyId в метод принимающий UserId будет ошибка компиляции. И даже если ее как то обойти через any, или еще что то, то рантайм исключение возникнет «ближе» к строке содержащей ошибку.

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

[Padreramnt]

type CompanyId = string & { __typename?: 'CompanyId' }
type UserId = string & { __typename?: 'UserId' }

const userId: UserId = 'user.id.1'
const companyId: CompanyId = 'company.id.1'
/*
Тип "CompanyId" не может быть назначен для типа "UserId".
  Тип "CompanyId" не может быть назначен для типа "{ __typename?: "UserId" | undefined; }".
    Типы свойства "__typename" несовместимы.
      Тип ""CompanyId" | undefined" не может быть назначен для типа ""UserId" | undefined".
        Тип ""CompanyId"" не может быть назначен для типа ""UserId" | undefined".
*/
const compiletimeError1: UserId = companyId
/*
Тип "UserId" не может быть назначен для типа "CompanyId".
  Тип "UserId" не может быть назначен для типа "{ __typename?: "CompanyId" | undefined; }".
    Типы свойства "__typename" несовместимы.
      Тип ""UserId" | undefined" не может быть назначен для типа ""CompanyId" | undefined".
        Тип ""UserId"" не может быть назначен для типа ""CompanyId" | undefined".
*/
const compiletimeError2: CompanyId = userId

[nin-jin]

https://github.com/eigenmethod/mol/tree/master/data#units

[impwx]

Не цель для TS — Сделать систему типов с гарантией безопасности, вместо этого сконцентрироваться на балансе между безопасностью и продуктивностью

И тем не менее предлагается включать "режим осады" и сильно перекосить баланс в сторону verbosity:

Предлагается ввести синтаксис позволяющий явно описывать Exceptions в сигнатуре функций

Предлагается добавить undefined к возвращаемому типу T для доступа по индексу к массиву. Но в таком случае при доступе по любому индексу придется использовать ? или делать явные проверки.

Для тех, кому soundness важнее интероперабельности с существующим кодом\подходамит, есть много других компилируемых в JS языков — PureScript, Elm, ReasonML…

[buggy375]

Я за осведомленность — если вы в экипировке на мотоцикле, то не бессмертны, если у вас TS, то не все в безопасности.
Хочу что-то как TS, только более надежное, что-то как Flow, только с лучшей поддержкой )

Почему я бы рекомендовал практики «надежного» TS, а не другой язык:
— Итеративность — можем шаг за шагом улучшать текущую кодовую базу
— Обратная совместимость — можно при расширении старого кода использовать новые подходы
— Порог входа — это TS с хорошими практиками, а не совершенно другой язык
— Типы для сторонних либ и их обновления

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

[VladVR]

если вы в экипировке на мотоцикле, то не бессмертны

нравится эта аналогия. Я, когда приходится рефакторить ts код, хоть бы и не нахожусь в абсолютной безопасности, все же имею подсказки где что может сломаться. моя оценка — система типизации отлавливает 90% моих ошибок. не бессмертие, но спасает от подавляющего большинства «тупизны». Бывает такое, что ошибка такая тупая, что когда найдешь — обтекаешь, сил нет, как такое могло произойти. С чистым js регулярно случалось, с ts буквально стало на порядок реже. Без преувеличений.