?

Log in

No account? Create an account
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

Comments:

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, а в том, что без аннотации типы аргументов вывести нельзя.
(Reply) (Parent) (Thread)
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)
(Reply) (Parent) (Thread)
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)
(Reply) (Parent) (Thread)
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
(Reply) (Parent) (Thread)
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)
(Reply) (Parent) (Thread)
Previous Entry  Next Entry