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

Взгляните, например, на это выражение (псевдокод, синтаксис 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>В каком месте?

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

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

N>Взгляните, например, на это выражение (псевдокод, синтаксис Haskell/Ela):
N>[haskell]
N>let foo f = (f fst, f snd)
N> bar g = g (id, [])
N> in (foo bar, foo map)

Этот пример ничего не показывает кроме св-в конкретной системы типов. Ничего не мешает вывести типы абстрактно/неуточненно, если бы система типов некоего статически компиллируемого языка это позволяла.

В шаблонном коде "абстрактные" типы превращаются в реальные только в месте применения реальных же типов. По аналогии с С++, можно уточнять шаблоны конкретными типами, а можно так же шаблонными. Недобство в синтакцисе С++ тут в том, что каждый новый уровень шаблонов требует нового ключевого слова template. Если бы синтаксис позволял делать это автоматом и сколько угодно глубоко иерархически, то проблем с аналогами приведеного примера не было бы. Конкретные типы выводились бы в местах вызова с конкретными же типами. Чуть выше на макросах+шаблонах С++ показали абсолютно правильно.

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

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

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

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

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

VD>Можно производить частичную компиляцию. В бинарники можно АСТ или другое промежуточное представление засовывать, например.
Ты не хуже меня знаешь, что это фактически распространение в исходниках.
Декомпиляторов для .НЕТ тьма.

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

WH>Ты не хуже меня знаешь, что это фактически распространение в исходниках.
WH>Декомпиляторов для .НЕТ тьма.

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

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

VD>Знаю точно, что это не исходники. Декомпиляторы тут не причем. Решается не задача обфускации, а задача бинарного распространения библиотек. Те же макры без намного удобнее подключать к проекту в виде длл-без нежели тащить с собой проекты.
Ну, так можно просто закатывать исходники в архив и всё.
И будет бинарное распространение.

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

WH>Ну, так можно просто закатывать исходники в архив и всё.
WH>И будет бинарное распространение.

Это если ты инфраструктуру сделаешь. А просто зип будет такой же неудобный и проблемый как исходники.

Тут целью является достижение модульности. В сборке с АСТ-ом могут разные метаданные валяться.

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

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

VD>Тут целью является достижение модульности. В сборке с АСТ-ом могут разные метаданные валяться.
Больше чем в исходниках валяться не может. Единственное преимущество сериализованного АСТ перед архивом с исходниками это скорость работы.

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

WH>Ну, так и для сериализованного АСТ нужна инфраструктура.

Нужна, но я не о том.

WH>Больше чем в исходниках валяться не может. Единственное преимущество сериализованного АСТ перед архивом с исходниками это скорость работы.

Может. Информация о проектах. В исходнике банально может не хватать зависимостей.

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

RO>

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

Ты это сам придумал?! Но чёртвозьмихолмс, как?

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

Доказательство очень простое: единственная нерекурсивная ветка здесь — tnpo Nothing = Just Nothing.
Поэтому, если программа останавливается, то она останавливается на Just Nothing.
А проблема остановки решается очень просто: ставим хаскелл на Крэй-1 и ждём 6 секунд

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

RO>>

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

К>Ты это сам придумал?!

Нет, конечно, пытался как-то сделать тип, соответствующий гипотезе «3n+1». Там еще не хватает collatz (Just Nothing) = Just Nothing, чем всё и должно завершаться. Теперь компилятор, чтобы вывести тип, должен доказать гипотезу или опровергнуть.

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

VD>Может. Информация о проектах. В исходнике банально может не хватать зависимостей.
А в сборку их святой дух записывает?

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

VD>>Может. Информация о проектах. В исходнике банально может не хватать зависимостей.
WH>А в сборку их святой дух записывает?

Нет.

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

VD>>>Может. Информация о проектах. В исходнике банально может не хватать зависимостей.
WH>>А в сборку их святой дух записывает?
VD>Нет.
Так откуда она берётся? Правильно. Из исходников.
Вот я и говорю что единственная разница между сборкой и исходниками это потребление ресурсов на машине пользователя.

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

VD>>>>Может. Информация о проектах. В исходнике банально может не хватать зависимостей.
WH>>>А в сборку их святой дух записывает?
VD>>Нет.
WH>Так откуда она берётся? Правильно. Из исходников.

Из файлов проектов, из метаинформации других сборок.

Исходники не несут всей информации. Не будет у тебя какого-то класса и как понять что это?

WH>Вот я и говорю что единственная разница между сборкой и исходниками это потребление ресурсов на машине пользователя.

Разница в полноценности. Имея сборку можно определить зависимости. С исходниками же все сложнее. Им нужны проекты, мекфайлы, правильное расположение на диске, внешние утилиты... В общем, все это сложно.

Плсю в сборку можно положить не только АСТ, но и код его обработки. А это уже совсем другой уровень, как ты понимаешь.

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

WH>Вот я и говорю что единственная разница между сборкой и исходниками это потребление ресурсов на машине пользователя.

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

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

WH>>Вот я и говорю что единственная разница между сборкой и исходниками это потребление ресурсов на машине пользователя.

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

И что это даёт кроме того на что ты отвечаешь?

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

WH>>Так откуда она берётся? Правильно. Из исходников.
VD>Из файлов проектов, из метаинформации других сборок.
Ну, так архивы с их исходниками лежат рядом.

VD>Исходники не несут всей информации. Не будет у тебя какого-то класса и как понять что это?
Ту таки святой дух работает?

VD>Разница в полноценности. Имея сборку можно определить зависимости. С исходниками же все сложнее. Им нужны проекты, мекфайлы, правильное расположение на диске, внешние утилиты... В общем, все это сложно.
Те нужна инфраструктура. Но она и сборкам нужна.

VD>Плсю в сборку можно положить не только АСТ, но и код его обработки. А это уже совсем другой уровень, как ты понимаешь.
Я даже не понял выделенное. Это о чём?

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

WH>И что это даёт кроме того на что ты отвечаешь?

Гарантию отсутствия ошибок определенного рода. Я в свое время с питоном наелся подобного, когда скрипт где то внутри осыпается по непонятным причинам из-за того что где то что то неотресолвилось или отресолвилось неправильно.

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

AVK>Гарантию отсутствия ошибок определенного рода. Я в свое время с питоном наелся подобного, когда скрипт где то внутри осыпается по непонятным причинам из-за того что где то что то неотресолвилось или отресолвилось неправильно.
Мы же говорим про статическую типизацию? Так что питон тут вообще не причём.
А перед созданием архива исходники можно проверить.

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

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

по моему опыту работы, если речь идёт о крупной программе, то основная система типизации должна быть статической. она позволит реализовать 99% потребностей и обнаруживать ошибки во время компиляции. а для оставшегося 1% нужна динамическая типизация, ну как минимум в виде типа Variant. ну и дальше уже — статическая типизация должна быть как можно более мощной (хаскел рулит) чтобы покрыть больше нужд, макропрограммирование может использоваться чтобы ещё больше расширить её возможности, а использование дин. типизации требует повышенного покрытия тестами

для небольших/исследовательских проектов (write-only) дин. типизация предпочтительней

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

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

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

Вроде как это вполне естественное поведение. Какой бы крутой ни была система типов, все равно найдется примерчик, который она разгрызть не сможет. Это даже если смотреть на проблему с позиции, когда код в принципе можно типизировать, но на практике конкретная система типов его отвергнет. А ведь бывают и ситуации, когда код статически типизировать нельзя — например, тип функции может зависеть от рантайм-значений, и в одной ситуации это, скажем, a->b, а в другой — a->b->c, причем все зависит от того, какое *значение* будет у второго аргумента.

В Ela, например, есть библиотечка espec, которая реализует DSL для тестов, и спецификация теста выглядит так:

test1 = 
  test "Demonstration of espec"
  given [1..5]
    should contain 1
    shouldn't contain 3
    shouldn't contain 6
    when reverse
    should be [5,4..1]
    when tail
    should be [3,2..1]
    when head
    should be 4

Обычный хаскелевый синтаксис

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

ВВ> А ведь бывают и ситуации, когда код статически типизировать нельзя — например, тип функции может зависеть от рантайм-значений, и в одной ситуации это, скажем, a->b, а в другой — a->b->c, причем все зависит от того, какое *значение* будет у второго аргумента.

В зависимых типах можно же.

ВВ>В Ela, например, есть библиотечка espec, которая реализует DSL для тестов, и спецификация теста выглядит так:
ВВ> should be [5,4..1]
ВВ> when tail
ВВ> should be [3,2..1]

Баги, баги.. Не, не заменят тесты типов.

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

DM>Здравствуйте, Воронков Василий, Вы писали:
ВВ>> А ведь бывают и ситуации, когда код статически типизировать нельзя — например, тип функции может зависеть от рантайм-значений, и в одной ситуации это, скажем, a->b, а в другой — a->b->c, причем все зависит от того, какое *значение* будет у второго аргумента.
DM>В зависимых типах можно же.

В зависимых типах зависимость будет от типов, а не от рантайм-значений.

ВВ>>В Ela, например, есть библиотечка espec, которая реализует DSL для тестов, и спецификация теста выглядит так:
ВВ>> should be [5,4..1]
ВВ>> when tail
ВВ>> should be [3,2..1]
DM>Баги, баги.. Не, не заменят тесты типов.

Если ты про ошибку внутри теста, то она нарочитая — пример взят из доки, как раз показывает поведение теста в случае, когда ассерты падают. Кстати, как бы статическая типизация помогла в подобном случае? Ведь с типами-то все в порядке =)

Вообще мне довольно много приходится программировать на динамических языках, причем не самых лучших — JavaScript, Lua. Могу сказать, что нет каких-то заметных проблем с ошибками типов. В той же Луа до фига проблем, связанных с особенностями Луа ("юникодные" строки, например), но вот ошибки типа встречаются весьма редко. Да и, честно говоря, ревнители статической типизации зачастую забывают, что ООП мейнстримный — это уже наполовину динамика. Да и куча задач в проекте фактически приводит к тому, что у нас понятие статического типа низводится, скажем, до XML схемы, которая валидируется в рантайме или вообще каких-то рукопашных пассов, причем никто особо не страдает от этого.

Так ли страшен черт, как его малюют?

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

ВВ>В зависимых типах зависимость будет от типов, а не от рантайм-значений.

Неправда, даже в этой самой теме я уже показывал пример обратного:
http://rsdn.ru/forum/philosophy/5261900?tree=tree

Автор: D. Mon
Дата: 15.08.13

Зависимые типы зависят именно что от значений, а не только от типов.

ВВ>Если ты про ошибку внутри теста, то она нарочитая

А, ок.

ВВ>Так ли страшен черт, как его малюют?

Это вечная тема, и в некотором смысле религиозная, я не уверен, что хочу сейчас в нее ввязываться.