?

Log in

November 2016   01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
cartoon

TypeScript: Static or Dynamic?

Posted on 2016.06.15 at 21:49
Tags: ,
https://medium.com/@gaperton/typescript-static-or-dynamic-64bceb50b93e#.mbkvfp8hh

Про TypeScript, и немного про теорию языков программирования вообще.

В связи с ростом популярности TypeScript, оживились флеймы static vs dynamic languages. Стороны опять точат копья.

А дело в том, что война окончена. В статье я, взрывая мозг примерами, популярно объясняю, что такое soft type system. На примере TypeScript. Ну и заодно делая небольшой экскурс в терминологию и понятия теории языков программирования.

Comments:


Николай Меркин
kodt_rsdn at 2016-06-16 03:32 (UTC) (Link)
Прямо уж взорвал примерами. Три раза написал function g().
Взгляд на типы с позиции менеджера, как на средство QA, это правильно, но чую, что неполно. Как минимум, в типы удается вынести генерацию обобщённого кода, т.е. уменьшить писанину и повысить выразительность.
А "мягкая типизация" - это расхожий термин или свежевведённый?
Имхо, любой язык с возможностями стирания типа, вплоть до тупо реинтерпреткаста к void*, сюда попадает. Или кое-кто что-то недоговорил и недовзорвал...
Gaperton
gaperton at 2016-06-16 04:47 (UTC) (Link)
> А "мягкая типизация" - это расхожий термин..

О. Это очень cтарый термин. Сейчас совсем не в моде. Даже статьи в википедии нет. Погуглите.

Edited at 2016-06-16 04:57 am (UTC)
Gaperton
gaperton at 2016-06-16 04:49 (UTC) (Link)
> Имхо, любой язык с возможностями стирания типа, вплоть до тупо реинтерпреткаста к void*, сюда попадает.

Конечно же нет.
Gaperton
gaperton at 2016-06-16 04:59 (UTC) (Link)
> Взгляд на типы с позиции менеджера

Так как я и инженер и менеджер, мне трудно разделять это "позиции". И я не вижу в этом исскуственном и надуманном "разделении" (и на мой взгляд глупой попытке их противопоставления) никакого практического смысла. Это две половинки знания об одном и том же, весь вопрос в том, обладаешь ли ты ими. Или хотя бы даже одной из них. Отсуствие обоих из них ничуть не мешает людям об этом руссуждать.

Ты считаешь, что-то "неполно"? Дополни.

Edited at 2016-06-16 05:37 am (UTC)
Николай Меркин
kodt_rsdn at 2016-06-16 03:48 (UTC) (Link)
Кстати, а кто сказал, что тип оператора деления - (any,any):number?
Если он перегружен, там вполне может быть (number,number):number|(MySuperFoo,xz):MyDuperBar|(any,any):number=NaN.
Т.е., иногда на выходе будет не число и даже не боттом, поэтому придётся обобщить результат до всё того же any.
Либо транслятор должен оттрассировать все вхождения функции g()...
Gaperton
gaperton at 2016-06-16 04:51 (UTC) (Link)
Особенности интерпретации оператора деления определяет конкретная ситема типов. Как она скажет - так и будет. В ней, например, может не быть никакого NaN, которое number. В ней могут быть, или не быть перегруженные операции.

Я намеренно упростил. Этот пример - это простейшая иллюстрация некой концепции, которая объясняется. Текст расчитан на человека, который не знает ничего, кроме JavaScript. И аппелирует к нему.

Я думаю, это вполне понятно, не? Концепция понятна? Или у нас проблемы с пониманием примеров?

Edited at 2016-06-16 05:30 am (UTC)
Gaperton
gaperton at 2016-06-16 05:11 (UTC) (Link)
С местными правилами бана, кстати, ты знаком, дружище? :) Оно называется "о модерировании и мудаках". Крайне рекомендую. Куда более строгое, чем на РСДН :)

Нет то, чтобы я намекал на что-то. Не пойми меня неправильно. Я уверен, что не смотря на некоторые смутные сигналы (это о моих догадках касательно твоего мотива оставлять здесь комментарии), ты сможешь держать себя в руках :)

http://gaperton.livejournal.com/62888.html

Edited at 2016-06-16 05:21 am (UTC)
VoidEx
voidex at 2016-06-16 06:56 (UTC) (Link)
А тип function const(a, b) { return a; } выведет как any, any -> any?
А тип function app(f, x) { return f(x); }?

По поводу g, я не понял, почему именно вывело any:
1. Так как в JS можно любой объект делить на 10 (если не число), и получится NaN, и именно поэтому вывело any
2. В JS в любую функцию можно всегда передать что угодно, поэтому и any

А что понимается под "война окончена"? Если то, что адепты статики скажут, что это очень хороший компромисс, то сомнительно, ибо им dep types подавай.
Gaperton
gaperton at 2016-06-16 07:37 (UTC) (Link)
> А тип function const(a, b) { return a; } выведет как any, any -> any?

Да. Так и выводит. Вот здесь можно посмотреть. https://www.typescriptlang.org/play/

> А тип function app(f, x) { return f(x); }?

Да. Выводит как все any. Не смотря на то, что могло бы предположить что f - это function.

Ибо не хочет ломать семантику JS (их установка - корректная JS программа должна скомпилироваться). ТО есть, для более строгой типизации надо намекнуть явной аннотацией.

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

Edited at 2016-06-16 07:43 am (UTC)
Gaperton
gaperton at 2016-06-16 07:40 (UTC) (Link)
> А что понимается под "война окончена"? Если то, что адепты статики скажут, что это очень хороший компромисс, то сомнительно, ибо им dep types подавай.

Ну, имеется более примитивный холивор, чем зависимые типы. Такой, совсем брутальный. Вроде "типы - говно!". Примерно треть детей выросших на динамическиз языках так реагирует. Оно есть. Я видел в конфах. Статья написана по мотивам флейма в Israel JavaScript, который меня совершенно изумил.
Gaperton
gaperton at 2016-06-16 07:49 (UTC) (Link)
> 1. Так как в JS можно любой объект делить на 10 (если не число), и получится NaN, и именно поэтому вывело any

Разные системы типов могут делать разные предположения. Мы легко можем навесить на JS более строгую систему типов, например. Которая запрещает NaN. И это будет по своему логично - как правило появление статически выводящегося NaN ничем хорошим не грозит, это явная ошибка.

Но это выбор разработчиков TypeScript. Они сделали такую систему типов, которая трактует этот NaN как норму, так что у нас выводится any. Она динамеческая.

Edited at 2016-06-16 07:57 am (UTC)
Gaperton
gaperton at 2016-06-16 07:51 (UTC) (Link)
> 2. В JS в любую функцию можно всегда передать что угодно, поэтому и any

Мало ли что можно передать в JS. Система типов TypeScript это не принимает во внимание, это всеж таки отдельный язык.
VoidEx
voidex at 2016-06-16 09:15 (UTC) (Link)
Моё внимание привлекла эта фраза:
When it prefers “any” by default, it’s called “Soft type system”.

И возник вопрос, soft type system - это свойство типизации некоего языка, или таки оно имеет смысл только при наличии какого-то другого языка с динамической типизацией, поверх которой сделан этот soft type system? Ну или как минимум суть в том, что если мы опустим все аннотации - должно работать так, будто всё динамическое (т.е. всегда проходить проверку типизации).

Я нагуглил pdf-ку "A soft-typing system for Erlang", где есть такая фраза:

A static type system added to an existing dynamically
typed programming language is sometimes referred to as a
soft-typing system

Плюс в таком случае мне понятно, что значит "by default", и почему именно так себя ведёт TS. Любой тип можно привести к any, а наоборот - нет, поэтому в возвращаемом значении вывести конкретный тип можно - ничего не пострадает, а в аргументе - нет, так как тогда туда any не передашь. Поэтому в аргументах надо by default (как я понимаю, там всегда any по умолчанию), а в возвращаемом - нет, можно строже.

Поэтому нельзя вывести тип аргумента в примере app(f, x), как функцию.

Т.о. если я верно понимаю, дело не в семантике самого JS, а в том, что без аннотации типы аргументов вывести нельзя.
Gaperton
gaperton at 2016-06-16 14:56 (UTC) (Link)
> И возник вопрос, soft type system - это свойство типизации некоего языка, или таки оно имеет смысл только при наличии какого-то другого языка с динамической типизацией, поверх которой сделан этот soft type system?

Обычно, под этим понималась нашлепка над базовым динамическим языком. Да. О TypeScript так можно сказать - это Soft Type System для JavaScript. Хотя можно и сразу такой язык придумать, который dynamic by default.

Вот первая статья, откуда пошел термин. В ней автор делает soft type system для статического ML, например.
http://courses.cs.ut.ee/2006/types/uploads/Main/cartwright91soft.pdf

Edited at 2016-06-16 02:58 pm (UTC)
Gaperton
gaperton at 2016-06-16 15:09 (UTC) (Link)
> Ну или как минимум суть в том, что если мы опустим все аннотации - должно работать так, будто всё динамическое (т.е. всегда проходить проверку типизации).

Они стараются делать так, что большинство _корректных_ программ на JS компилируется без аннотаций. Это не совсем так, что все динамеческое, type inference все-таки есть, и он работает.

Вот на это, например, компилятор ругается.

function g( a ) {
	return "" + a; // inferred as string
}

1 / g( 5 ) // cannot divide number by string.


Edited at 2016-06-16 03:10 pm (UTC)
VoidEx
voidex at 2016-06-16 19:34 (UTC) (Link)
Да, я не учёл, что хотя к any всё приводится, TS не будет это делать сам.

Стоит деление вынести в отдельную функцию div(x, y) { return x / y; } как ошибка пропадёт. Но здесь, видимо, играет роль, что в JS (судя по описанию ошибки) можно делить на any, поэтому приходится выводить y как any. Если бы можно было делить только number на number, тип можно было бы сделать строже. Т.е. из связи JS там "везде" any, в soft types для ML такого нет. Если я верно понял, суть в том, что any берётся тогда, когда не удалось вывести ничего лучше.

P.S. Кстати, S x. x x мне удалось типизировать на агде. Правда, там нет вывода типов.


S : {a : Set} {β : Set → Set} → ({α : Set} → α → β α) → β (a → β a)
S x = x x

id : {a : Set} → a → a
id x = x

test : {a : Set} → a → a
test = S id
Gaperton
gaperton at 2016-06-19 06:15 (UTC) (Link)
Да, именно так. На any делить можно (и с any вообще все можно), а вот на string уже нельзя. any выводится, когда 100% не выводится ничего лучше.

И это разрушает мозг с непривычки. Ваще не так, как в статических системах типов. На any делить можно потому, что есть шанс, что там number попадется - то есть, программа с any трактуется как динамически типизированная.

Edited at 2016-06-20 05:29 am (UTC)
nivanych at 2016-06-16 08:01 (UTC) (Link)
> TypeScript

Ладно бы PureScript...
Gaperton
gaperton at 2016-06-16 08:07 (UTC) (Link)
Пишите про PureScript.
nivanych at 2016-06-16 08:12 (UTC) (Link)
Собственно, я про то, что всякие "статическое vs. динамическое" совершенно бессмысленны, если в качестве статического привлекается убогая система типов.
Gaperton
gaperton at 2016-06-19 05:18 (UTC) (Link)
Они совершенно бессмысленны без всяких "если" :). Потому, что есть такие вещи, как Gradual Typing, стирающие эти границы. Убогость или не убогость системы типов (что, кстати, оценочное суждение - оно не несет технической информации) этому совершенно перпендикулярна.
Владимир Макайда
byyj at 2016-06-16 12:08 (UTC) (Link)
Генная инженерия, скрестили ужа с ежом и удивляются, почему оно не взлетает. Лучше бы в F# так вкладывались.

По существу хорошей статьи можно сказать, что пока вы не можете доказать математически полного покрытия тестами, любое маленькое движение в сторону строгой типизации будет полезно для качества, в ущерб скорости наброса. Typescript и есть такое аккуратное движение в эту сторону.
Трещиноватые коллекторы. Инструкция.
maksenov at 2016-06-17 02:37 (UTC) (Link)
TypeScript уже взлетел, и ради интереса просто стоит посмотреть какие библиотеки на нем написаны.

А не могли бы вы пояснить что значит математически полное покрытие тестами, и какой цели оно служит? Потому что если оно только гарантирует корректность использования всех типов, то это бессмысленно, потому что программа может быть некорректной, но все типы совпадают.
Владимир Макайда
byyj at 2016-06-17 05:49 (UTC) (Link)
То, что это приятнее и качественнее, мне кажется очевидно. Критика была в том, что поскольку люди исходили "из возможного", то и получилось "то, что возможно". Поэтому и приходится "объяснять себя" вот в таких статьях.


Как говорил Дейкстра, отладка программы - это сведение количества ошибок к приемлемому минимуму. Так и живём:)
Alexander  Mikhalev
alexander_mikh at 2016-06-18 20:34 (UTC) (Link)
>TypeScript уже взлетел, и ради интереса просто стоит посмотреть какие библиотеки на нем написаны.

погуглил, нашел мало. Приведите пример?
Трещиноватые коллекторы. Инструкция.
maksenov at 2016-06-19 03:19 (UTC) (Link)
Из крупных: angular, angular2, dojo2, immutable.js.

К большому количествую уже готовых библиотек есть внятные описания типов для использования с TS: https://github.com/DefinitelyTyped/DefinitelyTyped
Gaperton
gaperton at 2016-06-19 05:11 (UTC) (Link)
На нем Angular 2 сделан. Хотя бы поэтому TypeScript-у никак не избежать "взлета".

Ну и потому, что его система типов весьма неплоха, если ее сравнивать не с эзотерикой, а с популярными языками, на которых реально пишут. С Java, например.

Edited at 2016-06-19 05:20 am (UTC)
Gaperton
gaperton at 2016-06-19 05:32 (UTC) (Link)
> А не могли бы вы пояснить что значит математически полное покрытие тестами, и какой цели оно служит?

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

https://ru.wikipedia.org/wiki/%D0%A6%D0%B8%D0%BA%D0%BB%D0%BE%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B0%D1%8F_%D1%81%D0%BB%D0%BE%D0%B6%D0%BD%D0%BE%D1%81%D1%82%D1%8C

Разумеется, на практике мало кто подгоняет покрытие под цикломатику. Есть два разных software engineering - о котором говорят в сети и на конференциях, и как реально делают. В реальности дай бог если каждая строка написанного кода тестами вызывается.

Что звучит разумно (ну код-то мы вообще хоть раз вызвать тестами должны!), но (внезапно) этого трудно достичь из-за так называемого "защитного кода" и обработки ошибок. Каждую исключительную ситуацию покрывать тестами, эээ... Влом. Некоторые из них не так просто воспроизвести.

В общем, это "полное покрытие" - Неуловимый Джо. Никто его не может поймать, и никому он особенно не нужен.

Edited at 2016-06-19 05:43 am (UTC)
Трещиноватые коллекторы. Инструкция.
maksenov at 2016-06-19 15:10 (UTC) (Link)
Ага, спасибо.

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

По ощущениям оно так и происходит - функциональными и интеграционными тестами проверяются типичные форкфлоу (сразу вскрывая глупые ошибки с типами), а на остальное кладется болт.
Gaperton
gaperton at 2016-06-20 05:32 (UTC) (Link)
Об этом я и писал в статье. Системы типов популярных языков слишком слабы, чтобы конкурировать с традиционными QA процедурами (а эзотерику мы всерьез не воспринимаем - есть объективные причины, почему она даже близко не подходит к мэйнстриму). Ловля этих ошибок чуть раньше - приятно, но само по себе не преимущество. Оно в другом.

И это другое - оно более важное.

Edited at 2016-06-20 05:45 am (UTC)
Previous Entry  Next Entry