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

Взгляните, например, на это выражение (псевдокод, синтаксис Haskell/Ela):

let foo f = (f fst, f snd)
    bar g = g (id, [])
  in (foo bar, foo map)

	Пояснения для тех, кто подзабыл синтаксис
	let ... in expr -- декларации локальных функций/значений для использования в выражении expr f x = ... -- декларация функции f c параметром x f x -- применение функции f к аргументу x (x, y) -- пара (кортеж из двух элементов, возможно, различного типа) id -- функция, возвращающая свой аргумент без изменений [] -- пустой список (id и [] выбраны просто как примеры выражений несовместимого типа) fst -- функция, возвращающая первый элемент пары, тип (a, b) -> a snd -- функция, возвращающая второй элемент пары, тип (a, b) -> b map -- функция, преобразующая функцию над элементами списка в функцию над списками, тип (a -> b) -> ([a] -> [b])

Пропробуйте мысленно убедиться, что это выражение является типобезопасным в том смысле, что оно не пытается выполнять ни над каким значением операций, которые оно не поддерживает (например, не вызывает список как функцию, и не пытается получить компонент кортежа из функции). Что является его результатом?

Ela, будучи в значительной степени динамически типизированным языком, считает это выражение корректным (как можно убедиться здесь). Haskell же отвергает его, как некорректно типизированное, хотя, если оставить в последней строке только foo map, то он может успешно вывести типы. Если же мы оставим только foo bar, то типы не выводятся, хотя всё же можно убедить Haskell в корректности выражения, включив поддержку rank-2 типов, и вручную добавив аннотацию типа для foo.

Вопрос: Есть ли статическая система типов, способная убедиться в типобезопасности приведённого выше выражения (хотя бы с вручную указанными аннотациями)? Если да, то какой тип она назначит функции foo?

Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию, с минимальными проверками на корректность (например, отвергать такие выражения, как head map или [] id), но позволять вручную указывать произвольные контракты (включая те, которые не выражаются в "обычных" системах типов, например, что функция принимает непустой список положительных целых чисел, не содержащий дубликатов). Компилятор может иметь разные уровни проверки контрактов: начиная от самых быстых, которые могут работать в фоновом режиме в процессе набора кода и помогать IDE показывать правильное автодополнение, до самых тщательных, которые могут запускаться в процессе continuous integration. Сторонние производители могли бы выпускать продукты, реализующие проверку расширенного множества контрактов.

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

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

не следует ли это из того, что для некоторого "универсального" алгоритма вывода типов может потребоваться очень большое количество времени (NP?) на вывод даже в относительно небольших примерах?

N>Взгляните, например, на это выражение (псевдокод, синтаксис Haskell/Ela):
N>

N>let foo f = (f fst, f snd)
N>    bar g = g (id, [])
N>  in (foo bar, foo map)
N>

N>...Что является его результатом?

Не уверен, что понял этот пример, т.к. никогда не писал ни на Haskell/ML, ни на Ela.
Насколько я понял foo bar вернет (bar fst, bar snd) ==> (fst (id, []), snd (id, [])) ==> (id, []), тип — кортеж.
Соответственно foo map ==> map (id, []) ==> [] -> [], видимо тип аргумента этой функции — пустой список.

Результатом, видимо, будет кортеж ((id, []), [] -> []).

Честно говоря, не понимаю в чем тут проблема, если компилятору не пытаться "увидеть" во всех точках вызова foo один и тот же возвращаемый тип, или может я чего-то не понимаю?

Если отвлечься — в Haskell используется алгоритм вывода типов Hindley-Milner, может быть возможно рассмотреть какую-то надстройку над ним, вариант с эвристиками?

N>Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию...

Рискну предположить, что сходным примером могла бы быть попытка написания программы с использованием статического и динамического языка программирования тесно интегрированных друг с другом на уровне платформы (пример — JVM, Java + Clojure).
Хотя, java, видимо, не является хорошим примером статической типизации.

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


N>Вопрос: Есть ли статическая система типов, способная убедиться в типобезопасности приведённого выше выражения (хотя бы с вручную указанными аннотациями)? Если да, то какой тип она назначит функции foo?
Есть терема геделя о неполноте, которая, как мне кажется, в этом случае очень даже применима.
То есть какую бы непротиворечивую систему типов мы не выбрали в ней найдется выражение корректное выражение (его корректность доказывается подстановкой), которое в рамках этой системы неразрешимо.

N>Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию, с минимальными проверками на корректность (например, отвергать такие выражения, как head map или [] id), но позволять вручную указывать произвольные контракты (включая те, которые не выражаются в "обычных" системах типов, например, что функция принимает непустой список положительных целых чисел, не содержащий дубликатов). Компилятор может иметь разные уровни проверки контрактов: начиная от самых быстых, которые могут работать в фоновом режиме в процессе набора кода и помогать IDE показывать правильное автодополнение, до самых тщательных, которые могут запускаться в процессе continuous integration. Сторонние производители могли бы выпускать продукты, реализующие проверку расширенного множества контрактов.

В теории очень даже верно и такое наблюдается во многих местах. Например есть javascript, есть надстройка — типизированный typescript, который довольно мощной системой типов обладает. Есть всяческие подмножества с аннотациями, типа asmjs.

На практике система типов обеспечивает не только корректность кода, но и эффективность его исполнения. Даже нереально зализанные движки JS, на правильно подготовленном коде, сливают по сравнению с типизированными языками. Вещи типа asmjs могут улучшить положение, но они vendor-specific и ни разу не расширяемые, особенно сторонними производителями.

Кроме того, если позволить писать нетипизированный код, то в него по-любому проникнут ошибки. Потому что на аннотации все будут забивать.

Ошибки стоят дороже невозможности написать красивый код. Поэтому я останусь на стороне строгости типизации, даже в ущерб возможностям.

Приведенный код легко было бы написать так:

let foo f1 f2 = (f1 fst, f2 snd)
    bar g = g (id, [])
  in (foo bar bar, foo map map)

Или задействовать механизмы макросов (как в Nemerle), foo можно легко превратить в макрос, который выполняет подстановку в compile-time.

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

G>Или задействовать механизмы макросов (как в Nemerle), foo можно легко превратить в макрос, который выполняет подстановку в compile-time.

Кстати, это интересная мысль — сделать все локальные (или приватные) функции безтиповыми по умолчанию, и проверять их корректность по месту вызова. При этом совсем не обязательно их действительно инлайнить в получаемом бинарнике.

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

N>Кстати, это интересная мысль — сделать все локальные (или приватные) функции беcтиповыми по умолчанию, и проверять их корректность по месту вызова.

Так а что мешает так делать везде? Как в шаблонах C++.

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

N>>Кстати, это интересная мысль — сделать все локальные (или приватные) функции беcтиповыми по умолчанию, и проверять их корректность по месту вызова.

RO>Так а что мешает так делать везде? Как в шаблонах C++.

Ну вроде как инкапсуляция нарушается. И часто нужно модули в бинарной форме распостранять, без исходников.

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

Видимо, у меня какое-то не такое восприятие, но мне вопрос, вынесенный в название темы, кажется странным.

Программист, когда пишет функцию, он же представляет себе, что именно функция принимает и возвращает? Если нет, то это просто не имеет смысла: функция принимает на вход непонятно что и возвращает непонятно что. Над "непонятно чем" невозможно выполнить никаких операций. Очевидно, программист все же имеет в виду какой-то тип, пусть и не определенный формально и точно, но если над объектом производят хоть какие-то операции, то тип этими операциями и определяется.

С моей точки зрения, динамическая типизация является лишь неявной статической типизацией, просто, вместо явного объявления типа программистом, этот тип определяется через использование. Сам код задает контракт и, таким образом, тип.

Статическая типизация не просто "ограничивает", а определяет смысл выражений. У меня такое ощущение, что многие просто ее неправильно воспринимают, может быть, из-за отсутствия языков с адекватной типизацией.

Да и на практике в динамических языках все очень пошло заканчивается тем, что типы прописываются в комментариях, неформально и без проверки компилятором.

Возможно, я чего-то не понимаю.

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

N>

let foo f = (f fst, f snd)
    bar g = g (id, [])
  in (foo bar, foo map)

N>Вопрос: Есть ли статическая система типов, способная убедиться в типобезопасности приведённого выше выражения (хотя бы с вручную указанными аннотациями)? Если да, то какой тип она назначит функции foo?

Пример попроще:

foo 0 = 0
foo _ = []

какого типа foo?

N>Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию, с минимальными проверками на корректность (например, отвергать такие выражения, как head map или [] id), но позволять вручную указывать произвольные контракты (включая те, которые не выражаются в "обычных" системах типов, например, что функция принимает непустой список положительных целых чисел, не содержащий дубликатов).

Думаю такая "расширяемая типизация" при выводе типов будет бороться с проблемой останова, т.к. выводимый тип (контракт и тп) будет зависеть от алгоритма.

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

N>Ну вроде как инкапсуляция нарушается.
В каком месте?

N>И часто нужно модули в бинарной форме распостранять, без исходников.
Тут либо одно. Либо другое.

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

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

tnpo (Just x) = Just (Just (Just (tnpo x)))
tnpo Nothing = Just Nothing
collatz x = collatz3 x x x
collatz3 x (Just y) (Just (Just z)) = collatz3 x y z
collatz3 x y Nothing = collatz y
collatz3 x y (Just Nothing) = collatz (tnpo x)

И какой тип возвращаемого значения collatz (Just (Just (... (Just Nothing))...)? Я вот уверяю, что эта функция берет Maybe a и всегда возвращает Nothing. Докажи или опровергни :−)

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

_>Пример попроще:

foo 0 = 0
foo _ = []

_>какого типа foo?

Это уже действительно проще. Вот такой вот аналог этой функции успешно компилируется в Идрисе:

fooType : Nat -> Type
fooType O = Int
fooType _ = List Char

foo : (x:Nat) -> fooType x
foo O = 0
foo (S n) = []

Тут тип возвращаемого значения зависит от аргумента — инт для 0 и список символов для не нуля. Язык с зависимыми типами.

DM>Тут тип возвращаемого значения зависит от аргумента — инт для 0 и список символов для не нуля. Язык с зависимыми типами.

Даже вот так можно:

foo : (x:Nat) -> (if x==O then Int else List Char)
foo O = 0
foo (S n) = []

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

Этот вопрос к чему относится — нужна ли статическая типизация, или к проблемам вывода типов?

Проблема вывода типов, как и проблема автоматического доказательства, очевидно, сложна и упирается в теорему Геделя и разрешимость. Но я и не говорил, что вывод типов — это вообще хорошо и нужно.

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

Динамическая типизация — это частный случай статической, с одним вариантным типом.

Мне кажется странным по умолчанию использовать динамическую типизацию, так как это, по меньшей мере, неэффективно. Лучше уж по умолчанию использовать статическую, а если проблемы — делать fallback к динамической.

Про нужность вывода типов: программист, написавший код, что-то все равно имеет в виду, какой-то тип, иначе что это за бессмыслица, это же не "непонятно какие" манипуляции над "непонятно чем"? Так чтобы не путать коллег, читающих код, почему бы не указать явно, что ты имел в виду? Что за игра в прятки? Если машина в твоем коде не может разобраться, то что должен делать твой коллега?

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

DM>Это уже действительно проще. Вот такой вот аналог этой функции успешно компилируется в Идрисе:
DM>

DM>fooType : Nat -> Type
DM>fooType O = Int
DM>fooType _ = List Char

DM>foo : (x:Nat) -> fooType x
DM>foo O = 0
DM>foo (S n) = []
DM>

DM>Тут тип возвращаемого значения зависит от аргумента — инт для 0 и список символов для не нуля. Язык с зависимыми типами.

Зависимые типы — это хорошо. Но (foo _) должен принимать любое значение любого типа, которое можно сравнить.

псевдохаскель c классами типов в роли типов

foo :: Eq -> ОбщиеКлассыТипов (0, [])
или
foo :: Eq a -> ЗависмыйТип a

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

E>Здравствуйте, Roman Odaisky, Вы писали:

E>Этот вопрос к чему относится — нужна ли статическая типизация, или к проблемам вывода типов?

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

Но даже наличие "ленивой" (нормальной) типизации есть теорема Геделя о неполноте, так что можно будет найти корректные выражения, которые невозможно типизировать.

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

N>Взгляните, например, на это выражение (псевдокод, синтаксис Haskell/Ela):
N>

N>let foo f = (f fst, f snd)
N>    bar g = g (id, [])
N>  in (foo bar, foo map)
N>

Всё работает :

	head
	#include <boost/range/adaptor/transformed.hpp> #include <initializer_list> #include <iostream> #include <utility> using namespace std; template<typename F> struct Transformer { F f; // need C++14 polymorphic lambda :crash: template<typename R> auto operator()(const R &x) const { return boost::adaptors::transform(x, f); } }; struct EmptyList{} const empty_list; #define UNARY_FUNC(name, body) \ struct AUX_ ## name \ { \ template<typename T> \ auto operator()(const T &x) const \ { \ return body; \ } \ } const name \ /**/ UNARY_FUNC(fst, x.first); UNARY_FUNC(snd, x.second); UNARY_FUNC(id, x); UNARY_FUNC(map, (Transformer<T>{x}) );

UNARY_FUNC(foo, make_pair(x(fst), x(snd)) );
UNARY_FUNC(bar, x(make_pair(id, empty_list)) );

int main()
{
    auto result = make_pair(foo(bar), foo(map));
    auto data = {make_pair(1, 11), make_pair(2, 22)};

    for(auto z : result.second.first(data) )
        cout << z << " ";
    cout << endl;

    for(auto z : result.second.second(data) )
        cout << z << " ";
    cout << endl;
}

Вывод:

1 2 
11 22

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

G>Но даже наличие "ленивой" (нормальной) типизации есть теорема Геделя о неполноте, так что можно будет найти корректные выражения, которые невозможно типизировать.

"Типизировать" в каком смысле? Вывести типы автоматически или написать руками?

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

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

G>>Но даже наличие "ленивой" (нормальной) типизации есть теорема Геделя о неполноте, так что можно будет найти корректные выражения, которые невозможно типизировать.

E>"Типизировать" в каком смысле? Вывести типы автоматически или написать руками?
В смысле найти тип, который будет удовлетворять условиям. Руками или автоматически — неважно.

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

N>Я всегда был убеждённым сторонником статической типизации.
N>Я постепенно склоняюсь к мысли, что язык по умолчанию должен иметь большей частью динамическую типизацию

Уточни, пожалуйста, что именно ты называешь статической и динамической типизацией. К примеру, шаблоны C++ с их утиной типизацией, воплощаемой в конкретные типы во время компиляции — это что?

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

N>>Ну вроде как инкапсуляция нарушается.
WH>В каком месте?

В том месте, где библиотечные кишки становятся видны пользователю кода. ))
Только это не называется "инкапсуляция". Кишки происходящего видны и в дотнетных сборках, а т.н. их обфускация ничем не хуже обфускации на уровне исходников. Более того, можно составить однозначное отображение одного в другое.