Андрес Хейлсберг рассказывает про TypeScript и его систему типов.
Фактически представили типы в виде множеств значений, где отдельное значение тоже является валидным типом.
Прикрутили операции над множествами — пересечение, объединение, отображения. Сделали уловные операторы для отображений.
Кроме того они фактически прикрутили доказательство теорем к системе типов, которое учитывает control flow в программе. И работает система доказательств в обе стороны — для проверки корректности и для вывода типов.
Честно говоря это настолько круто, что я прям офигел. В существующих языках я такого не видел еще. Даже хаскелл с его наворотами в системе типов выглядит как академическая игрушка. А тут реально работающая вещь, которая еще и голый js умеет проверять на корректность.
Я так понимаю алгоритмы из компилятора TS начинают проникать в компилятор C#, в частности control-flow и escape analysis.
К сожалению эта вся крутость в TS работает в compile time.
Как вы думаете можно ли использовать эти данные о типах чтобы сделать код на TS\JS более быстрым в runtime? Может кто слышал про такие наработки?
Здравствуйте, gandjustas, Вы писали:
G>Кроме того они фактически прикрутили доказательство теорем к системе типов, которое учитывает control flow в программе. И работает система доказательств в обе стороны — для проверки корректности и для вывода типов.
Это, конечно, очень хорошо. Но нужно иметь в виду, что система типов TypeScript "deliberately unsound", т.е. гарантий того, что типы сойдутся в runtime, нет. Кроме того, она undecidable, что в компиляторе решается некоторыми произвольными ограничениями на сложность выводимых типов.
Здравствуйте, nikov, Вы писали:
N>Но нужно иметь в виду, что система типов TypeScript "deliberately unsound", т.е. гарантий того, что типы сойдутся в runtime, нет.
Я это заподозрил, когда посмотрел презентацию. А где-то можно подробнее прочесть об этом?
N>Кроме того, она undecidable, что в компиляторе решается некоторыми произвольными ограничениями на сложность выводимых типов.
Здравствуйте, gandjustas, Вы писали:
G>Честно говоря это настолько круто, что я прям офигел. В существующих языках я такого не видел еще. Даже хаскелл с его наворотами в системе типов выглядит как академическая игрушка. А тут реально работающая вещь, которая еще и голый js умеет проверять на корректность. G>Я так понимаю алгоритмы из компилятора TS начинают проникать в компилятор C#, в частности control-flow и escape analysis. G>К сожалению эта вся крутость в TS работает в compile time. G>Как вы думаете можно ли использовать эти данные о типах чтобы сделать код на TS\JS более быстрым в runtime? Может кто слышал про такие наработки?
Здравствуйте, nikov, Вы писали:
N>Здравствуйте, gandjustas, Вы писали:
G>>Кроме того они фактически прикрутили доказательство теорем к системе типов, которое учитывает control flow в программе. И работает система доказательств в обе стороны — для проверки корректности и для вывода типов.
N>Это, конечно, очень хорошо.
Я тоже так считаю.
N>Но нужно иметь в виду, что система типов TypeScript "deliberately unsound", т.е. гарантий того, что типы сойдутся в runtime, нет.
Все-таки это проблуда поверж JS, который динамически типизирован. И в TS всегда можно написать оператор as и сделать вид что переменная нужного типа, а не того который посчитал компилятор.
Если же не прибегать к грязным вещам, то мне кажется что сойдутся. Хотя вряд ли кто-то проводил исследования на этот счет.
N>Кроме того, она undecidable, что в компиляторе решается некоторыми произвольными ограничениями на сложность выводимых типов.
Ну так это ровно в тех местах, которые undecidable даже в теории. Вроде структурной эквивалентности рекурсивных типов.
Или нет?
Здравствуйте, gandjustas, Вы писали:
N>>Но нужно иметь в виду, что система типов TypeScript "deliberately unsound", т.е. гарантий того, что типы сойдутся в runtime, нет. G>Все-таки это проблуда поверж JS, который динамически типизирован. И в TS всегда можно написать оператор as и сделать вид что переменная нужного типа, а не того который посчитал компилятор. G>Если же не прибегать к грязным вещам, то мне кажется что сойдутся. Хотя вряд ли кто-то проводил исследования на этот счет.
Основная причина — ковариантность всех generic типов, независимо от того, в каких позициях встречаются типы-параметры. С функциональными типами тоже были проблемы. Конечно же, команда TypeScript проводила исследования на этот счёт. Я сам в этом участвовал, когда там работал перед релизом. Впрочем, TypeScript — это не первый язык, в котором осознанно сделан такой выбор. В Eiffel параметры функций могут меняться ковариантно в производных классах, что тоже нарушает type safety.
Здравствуйте, nikov, Вы писали:
N>Основная причина — ковариантность всех generic типов, независимо от того, в каких позициях встречаются типы-параметры. С функциональными типами тоже были проблемы. Конечно же, команда TypeScript проводила исследования на этот счёт. Я сам в этом участвовал, когда там работал перед релизом. Впрочем, TypeScript — это не первый язык, в котором осознанно сделан такой выбор. В Eiffel параметры функций могут меняться ковариантно в производных классах, что тоже нарушает type safety.
Здравствуйте, takTak, Вы писали:
T>>>>>вот тут с flow сравнивают:
G>>>>Это все уже есть в TS.
T>>>посмотри лучше видео, разница есть, можешь начинать с 18 минуты G>>Да-да. Именно это все появилось примерно полгода назад в TS.
T>не понял, Typescript же не на OCaml базируется ?!
Не на окамл , но делает все тоже самое, что в презентации. Анализирует control flow и строит на его основе ограничения для типов.
Система типов в TS не крутейшая. Она на самом деле достаточно слабая местами. Но она крутейшая по главной причине: прагматизм. Они реально тихой сапой внедряют различные возможности типизации, оставляя язык при этом весьма прагматичным: типы в основном под ногами не путаются, легкий способ «обмануть» компилятор через `as any` (или уже через `as unknown`) и т.п.
И при этом — без зауми, без присущего многим другим языкам нездорового снобизма (да, я про Хаскель). Все вводится и объясняется простым доступным языком, и пользоваться всем этим можно вот прямо сейчас, не тратя два года на PhD по математике.
Здравствуйте, gandjustas, Вы писали: G>А можно с примерами кода?
Я могу поделиться. Задача — накормить тигра ведром брюквы.
Решение
abstract class Food {
abstract name(): String
}
abstract class Meat extends Food { }
class Hare extends Meat {
name(): String {
return "hare";
}
}
abstract class Veggie extends Food { }
class Carrot extends Veggie {
name(): String {
return "carrot"
}
}
class Sweede extends Veggie {
name(): String {
return "sweede"
}
}
abstract class Consumer<T extends Food> {
abstract eat(item: T): void
}
class Tiger extends Consumer<Meat> {
eat(item: Meat): void {
console.log("I am a tiger eating " + item.name());
}
}
function fill(items: Veggie[]): void {
var i = 0;
while(i <10) {
items[i] = new Sweede();
i++;
}
}
class Feeder {
carrots: Carrot[];
constructor() {
this.carrots = [];
// Это еще со времен Java известно, поэтому в ней generics инвариантны.
fill(this.carrots);
}
feed(multivore: Consumer<Food>): void {
for (var x of this.carrots)
multivore.eat(x);
}
}
// Вот это вот - то, где отношение "subtype" противоположно отношению параметра
// Consumer<Food> подтип Consumer<Meat> но не наоборот (с точки зрения здравого смысла).
new Feeder().feed(new Tiger());
Потом очень интересно выяснять, отчего же у тигра несварение и где он наелся всякой гадости. Задача усложнается тем, что настроение после подобных экспериментов у подопытного не очень хорошее.
Вот из-за подобных проблем
Здравствуйте, gandjustas, Вы писали:
G>Фактически представили типы в виде множеств значений, где отдельное значение тоже является валидным типом. G>Прикрутили операции над множествами — пересечение, объединение, отображения. Сделали уловные операторы для отображений.
Мне как-то непонятно, в чем смысл всего этого? (кроме стандартного "потому что могли")
Здравствуйте, gandjustas, Вы писали:
G>Посмотрел тут видео с конференции BUILD G>https://youtu.be/Pu92QXdf2t0
G>Андрес Хейлсберг рассказывает про TypeScript и его систему типов.
G>Фактически представили типы в виде множеств значений, где отдельное значение тоже является валидным типом. G>Прикрутили операции над множествами — пересечение, объединение, отображения. Сделали уловные операторы для отображений.
На мой взгляд главная крутость системы типов TypeScript в том, что она максимально близко описывает динамические возможности JavaScript.
Многие фичи TS сделаны для того чтобы описать библиотеки написанные на чистом JavaScript а не создания нового кода на TS.
Другая крутая фишка это разные режимы компиляции --strictFunctionType, --strictPropertyInitialization, --strictNullChecks, --noImplicitAny, --noImplicitThis можно выбирать какие ты хочешь проверки на этапе компиляции.
G>Кроме того они фактически прикрутили доказательство теорем к системе типов, которое учитывает control flow в программе. И работает система доказательств в обе стороны — для проверки корректности и для вывода типов.
G>Честно говоря это настолько круто, что я прям офигел. В существующих языках я такого не видел еще. G>Даже хаскелл с его наворотами в системе типов выглядит как академическая игрушка. А тут реально работающая вещь, которая еще и голый js умеет проверять на корректность.
+ можно легко писать свои правила tslint в внятным AST API для TypeScript + language service
G>Я так понимаю алгоритмы из компилятора TS начинают проникать в компилятор C#, в частности control-flow и escape analysis.
Здравствуйте, gandjustas, Вы писали:
G>К сожалению эта вся крутость в TS работает в compile time. G>Как вы думаете можно ли использовать эти данные о типах чтобы сделать код на TS\JS более быстрым в runtime? Может кто слышал про такие наработки?
Про такое не слышал. Но в TS есть классная фича, которая упрощает некоторые оптимизации. Когда в JS работаешь с большим количеством объектов, в некоторых случаях замена объекта со свойствами на массив дает хорошее ускорение. И TS позволяет описывать типы элементов фиксированного массива с последующими проверками и выводом типов.
const v: [number, string] = [1, 'c'];
const v1 = v[0]; // v1: number
const v2 = v[1]; // v2: string
const v3: boolean = v[1]; // error: "Type 'string' is not assignable to type 'boolean'
Здравствуйте, CoderMonkey, Вы писали:
CM>Здравствуйте, gandjustas, Вы писали:
G>>Фактически представили типы в виде множеств значений, где отдельное значение тоже является валидным типом. G>>Прикрутили операции над множествами — пересечение, объединение, отображения. Сделали уловные операторы для отображений.
CM>Мне как-то непонятно, в чем смысл всего этого? (кроме стандартного "потому что могли")
В частности, для того чтобы описать типами функции javascript библиотек.
Например, нужно описать метод addEventListener(type, handler). type это имя события, handler это функция обработчик, которая принимает на вход объект события,
тип объекта события зависит от имени события: mousedown — MouseEvent, keydown — KeyboardEvent.
Можно описать функцию просто, но тогда нам придется самостоятельно контролировать указывать тип объекта события в коде обработчика.
// описываем соответствие имени события и типа
interface DocumentEventMap {
"abort": UIEvent;
"activate": Event;
"beforeactivate": Event;
"beforedeactivate": Event;
"blur": FocusEvent;
"canplay": Event;
"canplaythrough": Event;
"change": Event;
"click": MouseEvent;
......
}
// сигнатура функции
function addEventListener<K extends keyof DocumentEventMap>(type: K, listener: (ev: DocumentEventMap[K]) => any): void;
// дальше в коде имеем контроль типа аргумента функции обработчика
addEventListener('abort', (v: UIEvent) => { // OK!
})
addEventListener('abort', (v: FocusEvent) => { // ERROR: Argument of type '(v: FocusEvent) => void' is not assignable to parameter of type '(ev: UIEvent) => any'.\n Types of parameters 'v' and 'ev' are incompatible.\n Type 'UIEvent' is not assignable to type 'FocusEvent'.\n Property 'relatedTarget' is missing in type 'UIEvent'
})
Здравствуйте, CoderMonkey, Вы писали:
CM>Здравствуйте, gandjustas, Вы писали:
G>>Фактически представили типы в виде множеств значений, где отдельное значение тоже является валидным типом. G>>Прикрутили операции над множествами — пересечение, объединение, отображения. Сделали уловные операторы для отображений.
CM>Мне как-то непонятно, в чем смысл всего этого? (кроме стандартного "потому что могли")
Другой пример. Функция merge объединяет два объекта в один.
