Здравствуйте, karbofos42, Вы писали:


K>И что же выведет в светлом будущем их язык для такой функции:
K>

K>def sum (a, b)
K>  a + b
K>end

K>sum("1", "2") // "12"
K>sum(1, 2)     // 3
K>sum(1, "2")   // ошибка
K>sum("2", 1)   // "21"
K>

K>откуда здесь контроль типов появится и как они определят какую логику я в sum заложил?
K>ну, допустим, автоматика может поругаться и сказать, что sum(1, "2") вызывать нельзя, т.к. упадёт.
K>А откуда возьмётся информация, что из всех вариантов нормально вызывать только sum(1, 2), т.к. другие вызовы вернут ошибочный результат и это не то поведение, которое мне нужно?

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

K>А когда я данные буду получать из БД или какого-нибудь внешнего веб-сервиса, то кто узнает, что пришло не то?

Код который парсит эти данные должен будет проверить что пришло то. Иначе не скомпилируется.

K>А как они будут контролировать подобные функции:

def get_value(params) # тип результата выведен как str | int 
  return "ошибка" unless params.has_key?("value")

  return params["value"].to_i
end

a = get_value({}) # тип a - str | int
b = get_value({"value" => 10}) # тип b - str | int
a + b     # Ошибка компиляции - не найдена функция +(str | int, str | int)

Здравствуйте, Константин Б., Вы писали:

КБ>В прекрасном языке будущего для склейки строк не используется оператор + .

А было бы неплохо научить компиляторы генерировать какие-нибудь StringBuilder'ы, чтобы в коде явно этим не заниматься.

КБ>А вообще странно требовать от обычной статической типизации чтобы оно само догадывалось какие инварианты должны соблюдаться в твоем коде.

Так это не я заявляю, что аннотация типов не нужна. Кто заявил — пусть и догадывается.
Меня лично устраивают языки со строгой типизацией и все эти ruby стараюсь стороной обходить (к сожалению не получается)

K>>А когда я данные буду получать из БД или какого-нибудь внешнего веб-сервиса, то кто узнает, что пришло не то?

КБ>Код который парсит эти данные должен будет проверить что пришло то. Иначе не скомпилируется.

так аннотация типов же не нужна, а входные данные приходят извне, как это может на компиляцию влиять?
Вместо указания типа, я должен буду тестовые данные (или какую-нибудь xsd, json-схему) компилятору давать, чтобы он их анализировал и тип данных выводил?

Здравствуйте, karbofos42, Вы писали:
K>А было бы неплохо научить компиляторы генерировать какие-нибудь StringBuilder'ы, чтобы в коде явно этим не заниматься.
Там же вопрос не в том, кто этим занимается, а в семантике операций, синтаксически описанных как сложение.
K>Так это не я заявляю, что аннотация типов не нужна. Кто заявил — пусть и догадывается.
K>Меня лично устраивают языки со строгой типизацией и все эти ruby стараюсь стороной обходить (к сожалению не получается)
+1
КБ>>Код который парсит эти данные должен будет проверить что пришло то. Иначе не скомпилируется.

K>так аннотация типов же не нужна, а входные данные приходят извне, как это может на компиляцию влиять?
Одно другому не мешает. Грубо говоря, функции, читающие входные данные, возвращают тип byte[]. То, что вы его не пишете руками, не означает, что его нет.
K>Вместо указания типа, я должен буду тестовые данные (или какую-нибудь xsd, json-схему) компилятору давать, чтобы он их анализировал и тип данных выводил?
Нет, отчего же. Компилятору достаточно наличия типизирующих функций — какой-нибудь parse_int превращает byte[] в (int | none).
Какой-нибудь x ?? -1 превращает int | none в int.
После этого компилятору остаётся только проверить, что у вас в + передаются два int, а не byte[] / int или ещё какая дичь.

Я всё равно считаю, что такого автовывода недостаточно — чёрт бы с ней с проблемой останова. Детектирование ошибок в такой системе превращается в увлекательную охоту, сравнимую с поиском источников NullReferenceException.
Ведь NRE — это частный случай провала типизации. Если у нас есть аннотации типов (или, скажем, [NotNull]), то чётко видим то место, в котором нарушено соглашение.
А если у нас везде автовывод, то забытый где-то оператор ?? приводит к лавине пересмотра типов по всей программе. И где-то в совершенно другом модуле у нас выпадает "ошибка вызова операции Add: типы аргументов не совпадают" или "неполное покрытие алгебраического типа".
Это, конечно, всё ещё лучше, чем кложевское "не удалось привести аргумент к IFn" или как там оно у них называется, вылетающее в рантайме. Но значительно хуже, чем привычная нам диагностика на границе модулей/методов.
В итоге, опциональная аннотация типов позволяет получить лучшее из обоих миров: убрать многословность номинативной типизации, и оставить возможность раннего обнаружения нарушений контрактов.

Здравствуйте, vaa, Вы писали:

vaa>Чем хорош "Руби" и сколько ему осталось / Владимир Дементьев (о типах)

Ну вот есть язык Crystal, где считай тот же Руби но с тем самым автоматическим выводом типов. Будущее уже наступило:
https://crystal-lang.org/

(сам не пользовался, подробностей не скажу)

Здравствуйте, maxkar, Вы писали:

vaa>>Сказали же. Ну, типа, что типы рано или поздно станут не нужны в результате развития компилятор-строения а зависимости остануться.
M>Явные аннотации останутся нужны для языков, подобных современным (Java/C# и подобные). Дженерики (generics) + сабтайпинг (subtyping) дают систему типов, которая в общем случае не может быть решена (за конечное время) автоматически при отсутствии аннотаций. "Не может быть решена" == "задача вывода типов сводится к решению проблемы останова".

Это несколько устаревшие представления, академики уже нащупали решения, просто в мейнстрим это еще не пришло. См. MLsub, SimpleSub, CubiML, MLscript...



M> Тот же Ocaml имеет глобальный вывод типов (аннтоации типов можно не писать). Но в нем нет ни автоматического приведения подтипа к базовому типу (нет subtyping),

Там есть subtyping для объектов и хороший вывод типов для них же. Просто этой частью языка мало кто пользуется.

Здравствуйте, D. Mon, Вы писали:

DM>Это несколько устаревшие представления, академики уже нащупали решения, просто в мейнстрим это еще не пришло. См. MLsub, SimpleSub, CubiML, MLscript...
Спасибо! Интересно, как именно они делают subtuping (как пишут, nonstandard but sound). Будет время — почитаю.

M>> Тот же Ocaml имеет глобальный вывод типов (аннтоации типов можно не писать). Но в нем нет ни автоматического приведения подтипа к базовому типу (нет subtyping),
DM>Там есть subtyping для объектов и хороший вывод типов для них же. Просто этой частью языка мало кто пользуется.
А где? Вот я открыл 12 Using coersions. Первое же предложение: "Subtyping is never implicit.". Ну и чуть дальше про то, что "We have seen that points and colored points have incompatible types. For instance, they cannot be mixed in the same list.". Это вообще нарушает Liskov Susbtitution Principle в отношении типа/подтипа. А все классические выводы про неразрешимость типов вроде бы сформулированы для LSP-совместимых систем типов.

И чуть дальше есть интересный пример:

# let to_point cp = (cp :> point);;
val to_point : #point -> point = <fun>

Видите, какой тип выводится для аргумента? Это не point. Это специальная аббревиатура для параметризованных типов. Я совсем чуть-чуть поигрался с ними, чтобы продемонстрировать:

class point = object end;;
let pair (x: #point) = (x, x);;
print_string(pair)

Вот это вот чудо (не компилируется, мне нужнo былo увидеть выведенные типы и желательно в онлайн-редакторе, чтобы локально для экспериментов ничего не ставить) дает ошибку

File "./HelloWorld.ml", line 3, characters 12-18:
3 | print_string(pair)
^^^^^^
Error: This expression has type (#point as 'a) -> 'a * 'a
but an expression was expected of type string

Т.е. определение метода развернулось в generic с ограничениями на типы. Это я не буду отрицать — generics поддерживают subtyping и границы типа (type bounds). Но для выражений subtyping отсутствует — каждое выражение (expression) имеет ровно один тип и не может быть использовано вместо значения родительского типа (но может быть использовано в generic-методах с соответствующей границей или в приведении/coersion).

Если переводить это в популярные языки, у нас получается что-то вроде:

class Point()
class ColoredPoint() extends Point

def printPoint(x: Point): Unit = ()
def printAnyPoint[T <: Point](x: T): Unit = ()

printPoint(new Point()) // compiles
printPoint(new ColoredPoint()) // does not compile (if type system is similar to Ocaml)
printAnyPoint(new Point()) // compiles
printAnyPoint(new ColoredPoint()) // compiles

Здравствуйте, maxkar, Вы писали:

M>Здравствуйте, D. Mon, Вы писали:

DM>>Это несколько устаревшие представления, академики уже нащупали решения, просто в мейнстрим это еще не пришло. См. MLsub, SimpleSub, CubiML, MLscript...
M>Спасибо! Интересно, как именно они делают subtuping (как пишут, nonstandard but sound). Будет время — почитаю.

Эта тема называется Algebraic Subtyping, и главный шаг там был в том, чтобы взять Хиндли-Милнер и перейти от уравнений вида t1==t2 к уравнениям t1 <: t2. При генерации уравнений (теперь неравенств) нужно только понять в каждом случае что должно быть подтипом чего, а при их решении обычная унификация превращается в несколько более сложную "биунификацию", где у каждой типовой переменной есть верхняя и нижняя граница в типах.
Я на этом небольшую собачку съел, т.к. на работе как раз делал тайпчекер для языка с сабтайпингом, полиморфизмом и глобальным выводом типов.

По-моему, самое понятное объяснение есть у Simple-sub:
https://infoscience.epfl.ch/record/278576
https://github.com/LPTK/simple-sub


M>>> Тот же Ocaml имеет глобальный вывод типов (аннтоации типов можно не писать). Но в нем нет ни автоматического приведения подтипа к базовому типу (нет subtyping),
DM>>Там есть subtyping для объектов и хороший вывод типов для них же. Просто этой частью языка мало кто пользуется.
M>А где?

class point x_init y_init =
  object
    method x : int = x_init
    method y : int = y_init      
  end

class colored_point x y (clr : string) = 
  object 
    inherit point x y    
    method color = clr
  end

(* works with any object with integer x and y *)
let prnt o = Printf.printf "%d %d\n" o#x o#y;;

let p  = new point 1 2;;
let cp = new colored_point 3 4 "red";;

(* classless object *)
let p3 = object
           method name = "Bob"
           method x = 5
           method y = 6
           method z = 7
         end;;

prnt p;;
prnt cp;;
prnt p3;;

выводит

1 2
3 4
5 6

Классы можно объявлять, можно не объявлять, сразу объекты лепить. Наследование можно использовать, а можно не использовать — структурная подтипизация работает. Аннотации для полиморфных функций можно не писать, необходимый минимум типов, который наша функция ожидает, выводится сам. В данном случае для prnt выводится тип
< x : int; y : int; .. > -> unit

Здравствуйте, karbofos42, Вы писали:

K> Так это не я заявляю, что аннотация типов не нужна. Кто заявил — пусть и догадывается.

Ну нет. Точно такую же претензию можно предъявить к оператору + например в тои же C++.
А чегой-то он мне дает строки складывать, когда я хочу чтобы + только с числами работал.

K>>>А когда я данные буду получать из БД или какого-нибудь внешнего веб-сервиса, то кто узнает, что пришло не то?

КБ>>Код который парсит эти данные должен будет проверить что пришло то. Иначе не скомпилируется.

K>так аннотация типов же не нужна, а входные данные приходят извне, как это может на компиляцию влиять?
K>Вместо указания типа, я должен буду тестовые данные (или какую-нибудь xsd, json-схему) компилятору давать, чтобы он их анализировал и тип данных выводил?

Ну вот пришел тебе any/object/IIUnknown. Ты с ним ничего не можешь сделать пока не проверишь что там внутри.

if (X is string) {
   // Здесь можно работать с X как со строкой
}
// a здесь нельзя

Ну формально можно придраться что у нас тут аннотация типов. Точно также можно сказать что кавычки у строковых литералов — это тоже аннтотация типа. Или x = new Foo() — тоже аннотация типа. Но если речь все-таки о типах в объявлениях переменных и функций — то можно обойтись и без аннотаций.

Здравствуйте, Константин Б., Вы писали:

КБ>Ну нет. Точно такую же претензию можно предъявить к оператору + например в тои же C++.
КБ>А чегой-то он мне дает строки складывать, когда я хочу чтобы + только с числами работал.

Нет. Оператор + реализован для конкретных типов и компилятор подбирает при сборке нужную реализацию.
Если я создам новый класс, то не смогу его объекты скадывать при помощи старых реализаций.
Мне придётся писать свою реализацию оператора или прописывать правила приведения к другому типу.

КБ>Ну формально можно придраться что у нас тут аннотация типов. Точно также можно сказать что кавычки у строковых литералов — это тоже аннтотация типа. Или x = new Foo() — тоже аннотация типа. Но если речь все-таки о типах в объявлениях переменных и функций — то можно обойтись и без аннотаций.

И вместо того, чтобы в сигнатуре метода указать его входные типы и перегрузить метод для всех возможных вызовов, я буду писать одну реализацию и в ней тонны проверок типов на все случаи жизни?
Меня вот бесит это писать и ещё больше ненавижу поддерживать подобный код на Руби.
Хоть какую-то пользу это приносит, кроме вот этих разговоров про аннотацию типов?
В чём разница, где именно я укажу тип данных, если всё равно по факту нужно будет его указывать?
Я вот вижу разницу в том, что в С++/C#/Java/... это за меня компилятор всё сделает и мне не нужно голову забивать проверками.
В Руби же именно что приходится кучу проверок пихать.

Здравствуйте, D. Mon, Вы писали:

DM>Я на этом небольшую собачку съел, т.к. на работе как раз делал тайпчекер для языка с сабтайпингом, полиморфизмом и глобальным выводом типов.
А если не сложно, можете рассказать, в какой области используется язык? И какие отзывы от реального использования? Если есть продукт, можно просто ссылку на страничку продукта, я там прочитаю.

Я прочитал про Simple-sub (отличная статья!). У них так же, как и во всем Хиндли-Милнере, полиморфные функции (верхнего уровня) не явлюятся значением первого порядка. При их использовании происходит разрешение параметров типов и функции превращаются в "мономорфные" (при этом аргумент может быть переменной типа). Такое ограничение далеко не всегда является проблемой на практике. Но все равно остается ограничением и существенными отличием от объектно-ориентированных языков. Например, следующий интерфейс не будет выразим (в виде record, хотелось бы какого-нибудь замыкания) в алгебраических подтипах:

trait DbPool {
  def withConnection[T](callback: DBConnection => T): T
}

Пример специально выбран из более-менее обычной практики. Подобный полиморфизм в Ocaml можно сделать через модули. Но, насколько я знаю, типы у модулей в том же Ocaml нужно всегда прописывать вручную. Отсюда и вопрос о практике применения языка.

Ваше замечание про полиморфизм и подтипы принято . Проблему завершимости доставляет не сам полиморфизм. Ее доставляет попытки сделать полиморфные функции объектом превого порядка — например, возможность задекларировать поле записи как полиморфную функцию (подтипы, наверное, тоже нужны для создания проблемы останова, но я точно не помню и книжки под рукой нет). То, что естественно ложится в ООП но гораздо сложнее выражается в ML.

DM>Аннотации для полиморфных функций можно не писать, необходимый минимум типов, который наша функция ожидает, выводится сам.
Спасибо за пример! Но я знаю, как его сломать

class point x_init y_init =
  object
    method x : int = x_init
    method y : int = y_init      
  end

class colored_point x y (clr : string) = 
  object 
    inherit point x y    
    method color = clr
  end
  
let cb fn =
  fn (new point 1 2);
  fn (new colored_point 1 2 "blue");;

Вроде бы в Ocaml без приведения (coersion) это заставить работать вообще невозможно. У fn выводится тип 'a -> unit с границей 'a <: { x : int, y: int }. И он связывается ровно один раз — в процессе передачи fn в cb, внутри cb этот 'a один и тот же (мономорфен). Так как point и colored_point разные типы, явные аннотации типов тоже не помогут. Алгебраические подтипы — да, выведут здесь все правильно.

Здравствуйте, vaa, Вы писали:

Судя по росту популярности TypeScript все же нужна. Но там конечно и Angular и React его продвинули

Здравствуйте, vaa, Вы писали:

vaa>Сказали же. Ну, типа, что типы рано или поздно станут не нужны в результате развития компилятор-строения а зависимости остануться.
Что-то у меня сегодня настроение подозрительно хорошее. Так что давайте я расскажу еще про ситуации, которые будут огромным препятсвием на пути автоматического вывода типов.

Для начала нужно отметить, что в современном мире у типов есть три основных предназначения. Первое — указание среде выполнения о том, как правильно размещать данные. Те же записи в языках вроде C (и даже ассемблера). В современных языках происходит усложнение. Например, объекты в Java/.NET определяют логическую структуру а конечное физическое представление определяется уже средой выполнения. В динамических языках указание может быть еще более расплывчатым — "просто число" или "объект/хэш". Но главная роль типа остается неизменной — указание/инструкция для компилятора или среды выполнения. Второе назначение (и его упоминали уже другие участники) — информация для других разработчиков. Например, контракты на поведение объектов и функций, связанных с типом. Третье назначение — доказательство определения определенных свойств программ. Хорошим (и наиболее известным) примером данного пункта будут параметры времени жизни в Rust.

В процессе эволюции языков фокус постепенно смещается с первой роли (инструкции компилятору или среде выполнения) на две последние (информация для других людей и проверка корректности программ). И вот тут уже возникает проблема с тем, что становится необходимо понимать семантику. Например, с точки зрения компилятора и среды выполнения мы всегда можем сложить два целых числа. А вот с точки зрения человека мы вряд ли должны складывать сантиметры с миллиметрами. Для решения данной конкретной проблемы есть два подхода. Более распространен подход с созданием типов-оберток и последующей их оптимизацией компилятором (например, Haskell). Другой возможный подход — непрозрачные синонимы типов (Opaque type alias). Они позволяют отличать значения разных размерностей на уровне системы типов. Компилятору без помощи человека будет очень сложно понять, что здесь требуется отдельный тип.

Непрозрачные типы, конечно, занимательны. Но у них хотя бы есть какие-то "значения", присутствующие в программе. Я же хочу рассказать о полезных типах, которые вообще не имеют значений. Давайте рассмотрим практическую задачу — контроль уровней изоляции транзакций. Мы пишем программу, работающую с базой данных. У нас есть различные методы. Многие выполняют только один запрос и им достаточно соединения с базой. Некоторые делают несколько модификаций и требуют транзакцию. В ряде случаев для корректной работы нам нужна не просто "транзакция", а транзакция с определенным уровнем изоляции. Например, чтение может требовать уровня serializable а запись — любого уровня ниже repeatable read. Все вышеописанные методы с радостью присоединятся к текущей транзакции требуемого уровня, если таковая есть. Последнее требование проблем обычно не представляет — можно передавать соединение с базой данных при вызове метода. Но как проверить во время компиляции, что у нас выставлен правильный уровень изоляции?

На помощь в решении проблемы контроля уровня изоляции приходят типы-свидетельства (evidence type, также известные как контекстные свидетельства/context evidence). Давайте параметризуем наши транзации (тип) уровнем изоляции:

trait Transaction[Level]:
  def query(...): ...
end Transaction

Как мы смоделируем Level? Это параметр типа, нам нужно как-то сравнивать "значения" друг с другом. Т.е. нам нужна иерархия:

abstract selaed class ReadUncommitted
abstract sealed class ReadCommitted extends ReadUncommitted
abstract sealed class RepeatableRead extends ReadCommitted
abstract sealed class Serializable extends RepeatableRead

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

//любая транзация будет работать
def anyTx(using tx: Transaction[_]) = ??? 
// только repeatable read
def anyRR(using tx: Transaction[RepeatableRead] = ??? 
// read uncommitted и read committed
def notTooMuch[Level >: ReadCommitted](using tx: Transaction[Level]) = ???
// read committed и выше
def notTooLow[Level <: ReadCommitted](using tx: Transaction[Level]) = ???
// Можно даже совмещать обе границы:
def arbitraty[Level <: ReadComitted >: RepeatableRead](using tx: Transaction[Level]) = ???

После этого нам достаточно добавить методы для старта транзакций в нашем нетранзакционном контексте:

trait NonTransaction:
  def readUncommittedTx[T](cb: Transaction[ReadUncommitted] => T): T
  def readCommittedTx[T](cb: Transaction[ReadCommitted] => T): T
  ...
end NonTransaction

Каждый метод получает транзакцию нужного уровня. Все дальнейшие передачи внутри метода проверяются. Например, следующий код не скомпилируется:

def doSer(using tx: Transaction[Serializable]): Unit = ()
def doRr(using tx: Transaction[RepeatableRead]): Unit =
  doSer(tx)

Требуемые уровни изоляции нужно писать вручную. Да, можно ошибиться. Но мне кажется, что иметь хоть какую-то защиту от опечаток все же лучше, чем совсем ничего.

Интересно и то, что без параметра типов проблему вряд ли можно решить. Стандартное наследование не позволит использовать уровни транзакций как высокоуровневый тип. Допустим, мы объявим ReadUncommitted extends Transaction. Но тогда мы не сможем ограничить уровни с обеих сторон. Serializable будет всегда приводим к ReadUncommitted (наследование — стандартное для .NET/Java). А вот дополнительный параметр типа позволяет обойти данное ограничение.

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

Ну и вообще в данном случае для контроля уровня транзакций хорошо было бы иметь "параллельную" систему типов. Не создавать синтетические параметры типов а добавить еще аннотацию и соответствующие правила проверки. Тогда можно было бы строить библиотеки типов и использовать их по необходимости:

(def doSer 
    [doc: делает что-то полезное]
    [baseType: unit]
  (tx [baseType: Transaction]
      [txLevel: Serializable]
      [doc: Соединение с базой данных]
      [lifetime: 'a]
  )
)

Была бы возможность, я бы Растовскую проверялку заимствований тоже с радостью использовал чтобы контроллировать отсутствие утечек. А то вдруг кто-то мою Transaction сложит в глобальный список? Она для такого не предназначена!

Здравствуйте, vaa, Вы писали:

vaa>Чем хорош "Руби" и сколько ему осталось / Владимир Дементьев (о типах)
Вообще то учитывая современные возможности процов, именно для компилятора, если разработчик компилятора не суперкриворукий, аннотации типов действительно не нужны. Ибо там, где они требуются, можно тупо делать ленивые вызовы и это на современном железе вообще практически не повлияет на производительность.

Вот только аннотации типов нужны в первую очередь людям. Ибо человек даже в детском проекте на миллион строк кода уже не способен адекватно понимать у какого параметра можно дернуть какой метод. В очень большой теории можно увеличить зависимость человека от IDE (еще увеличить!!!) и выводить типы из тестов, и именно для человека IDE будет показывать какой тип параметров требуется. И да, я предполагаю что в теории это может сработать, это вполне адекватно и что рано или поздно IDE к этому придут. Однако пока что светлое будущее ни черта не наступило и вряд ли наступит в ближайшие лет 5.

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

Соответственно я предполагаю, что рано или поздно действительно разработчики компиляторов и IDE наймут того, кто сможет сделать крутой вывод типов без потери производительности как минимум на современном железе. Но вот ХЗ сколько ждать еще, предполагаю что лет 10, не меньше. Ну и конкретно я думаю бы справился как минимум в написании High Level Design

Здравствуйте, elmal, Вы писали:

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

Что такое здесь "ленивые вызовы" и как они связаны с типами? Явно не про lazy evaluation речь, как я понял.


E>Однако на практике пока что все очень и очень печально — даже компиляторы не в состоянии осилить компиляцию без явного указания типов как минимум параметров функций.
E>Соответственно я предполагаю, что рано или поздно действительно разработчики компиляторов и IDE наймут того, кто сможет сделать крутой вывод типов без потери производительности как минимум на современном железе. Но вот ХЗ сколько ждать еще, предполагаю что лет 10, не меньше. Ну и конкретно я думаю бы справился как минимум в написании High Level Design

Щито? Для определенного класса языков автоматический вывод типов (в том числе параметров функций) существует уже лет 40, эта задача решена и в теории, и на практике — см. SML, OCaml, Haskell, Elm и т.п. С мейнстримными ООП языками дела похуже, но см. тот же Crystal выше.

Здравствуйте, maxkar, Вы писали:

DM>>Я на этом небольшую собачку съел, т.к. на работе как раз делал тайпчекер для языка с сабтайпингом, полиморфизмом и глобальным выводом типов.
M>А если не сложно, можете рассказать, в какой области используется язык? И какие отзывы от реального использования? Если есть продукт, можно просто ссылку на страничку продукта, я там прочитаю.

Используется в инвестфонде для внутренних задач. Широкой публике не доступен.
Немного писал о нем тут: https://thedeemon.livejournal.com/147209.html

M>Я прочитал про Simple-sub (отличная статья!). У них так же, как и во всем Хиндли-Милнере, полиморфные функции (верхнего уровня) не явлюятся значением первого порядка.

Тут что-то с терминологией. Если речь о https://en.wikipedia.org/wiki/First-class_function , то в ХМ полиморфные ф-ии вполне себе первоклассны — я могу передать map как аргумент в другую ф-ю или вернуть из третьей. Возможно, речь про higher rank типы — когда квантор forall не снаружи, а внутри сигнатуры, у параметра. Такое есть в Хаскеле (который сам на ХМ, просто с наворотами), и в Окамле, причем не только через модули, можно с рекордами или объектами:
https://v2.ocaml.org/manual/polymorphism.html#s:higher-rank-poly

https://webcache.googleusercontent.com/search?q=cache:o0i4KovTzBEJ:https://soap.coffee/~lthms/posts/RankNTypesInOCaml.html

Если этого не было в Simple-sub, то больше чтобы не раздувать реализацию фичами, не относящимися к основной теме. Там все же весь "язык" — лишь минималистичная демонстрация одной идеи. Вот MLscript уже не так минималистичен, там фич побольше, но инфы поменьше.

M>Например, следующий интерфейс не будет выразим (в виде record, хотелось бы какого-нибудь замыкания) в алгебраических подтипах:
M>

trait DbPool {
  def withConnection[T](callback: DBConnection => T): T
}

Не вижу почему. Разве что может понадобиться вынести Т выше.

Higher rank типы не выводятся автоматически нигде, но если автор языка их явно добавляет, особой несовместимости с идеями algebraic subtyping я не вижу, это вещи ортогональные.

M>Ваше замечание про полиморфизм и подтипы принято . Проблему завершимости доставляет не сам полиморфизм. Ее доставляет попытки сделать полиморфные функции объектом превого порядка — например, возможность задекларировать поле записи как полиморфную функцию (подтипы, наверное, тоже нужны для создания проблемы останова, но я точно не помню и книжки под рукой нет). То, что естественно ложится в ООП но гораздо сложнее выражается в ML.

Да точно так же выражается. Просто аннотации нужны, да, вывод типов не телепат чтобы угадывать куда forall ставить.

M>Спасибо за пример! Но я знаю, как его сломать
M>Вроде бы в Ocaml без приведения (coersion) это заставить работать вообще невозможно.

Тут нужно приведение, да, ибо унификация на равенствах и ожидает одинаковый тип.

Здравствуйте, Serginio1, Вы писали:

S>Здравствуйте, vaa, Вы писали:

S>Судя по росту популярности TypeScript все же нужна. Но там конечно и Angular и React его продвинули

может потому что в js слабая типизация в отличии от например common lisp

Здравствуйте, D. Mon, Вы писали:

DM>Щито? Для определенного класса языков автоматический вывод типов (в том числе параметров функций) существует уже лет 40, эта задача решена и в теории, и на практике — см. SML, OCaml, Haskell, Elm и т.п. С мейнстримными ООП языками дела похуже, но см. тот же Crystal выше.
Есть ли нормальная поддержка этого в IDE? Чтобы прекрасно работал автокомплит, чтобы автоматом подсвечивались ошибки. Чтобы работало все настолько хорошо, что б желания явно писать тип не было. И при этом в любой момент можно было выведенный тип узнать минимумом действий при просмотре кода и поиске ошибок. Из того, что я вижу — простор для улучшения по сравнению с текущей ситуацией огромен.

Здравствуйте, vaa, Вы писали:

S>>Судя по росту популярности TypeScript все же нужна. Но там конечно и Angular и React его продвинули

vaa>может потому что в js слабая типизация в отличии от например common lisp
Не смотрел common lisp. E JS динамическая типизация. Там никакого интеллисенса и проверки кода нет.
Да можно вывести тип в области видимости присваивания. Но не более

Но суть то TS это прежде всего Intellisense и синтаксическая проверка кода.

Здравствуйте, elmal, Вы писали:

DM>>Щито? Для определенного класса языков автоматический вывод типов (в том числе параметров функций) существует уже лет 40, эта задача решена и в теории, и на практике — см. SML, OCaml, Haskell, Elm и т.п. С мейнстримными ООП языками дела похуже, но см. тот же Crystal выше.
E>Есть ли нормальная поддержка этого в IDE? Чтобы прекрасно работал автокомплит, чтобы автоматом подсвечивались ошибки. Чтобы работало все настолько хорошо, что б желания явно писать тип не было. И при этом в любой момент можно было выведенный тип узнать минимумом действий при просмотре кода и поиске ошибок. Из того, что я вижу — простор для улучшения по сравнению с текущей ситуацией огромен.

Да, давно. С Окамлом это у меня в OcaIDE работало в 2008 году еще. Навел мышку на что-то — его тип показали. И остальное тоже, насколько помню.

http://www.algo-prog.info/ocaide/screenshots.php

Здравствуйте, maxkar, Вы писали:
M>Непрозрачные типы, конечно, занимательны. Но у них хотя бы есть какие-то "значения", присутствующие в программе. Я же хочу рассказать о полезных типах, которые вообще не имеют значений. Давайте рассмотрим практическую задачу — контроль уровней изоляции транзакций. Мы пишем программу, работающую с базой данных. У нас есть различные методы. Многие выполняют только один запрос и им достаточно соединения с базой. Некоторые делают несколько модификаций и требуют транзакцию. В ряде случаев для корректной работы нам нужна не просто "транзакция", а транзакция с определенным уровнем изоляции. Например, чтение может требовать уровня serializable а запись — любого уровня ниже repeatable read.
Вот этот момент я не понял. Почему запись вдруг будет требовать уровень ниже repeatable read?
Обычно ситуация ровно обратная: метод может требовать определённых гарантий, но не их отсутствия.
Ну, там, метод, который просто читает баланс счёта может вообще транзакции не требовать.
Метод, который получает список счетов с их балансами будет требовать serializable.
Метод, который переводит с одного счёта на другой, будет требовать repeatable read.

В итоге, всё прекрасно моделируется стандартным subtyping-ом, который реализован в любом ОО-языке.

Ну, а если нам всё же для чего-то требуется один из конкретного списка уровней изоляции, то это проще всего смоделировать на алгебраических типах:

BelowRepeatableRead ::= ReadCommitted, DirtyRead;
RepeatableReadOrAbove ::= RepeatableRead, Serializable;