T>Именно поэтому я и считаю, что твоё сравнение неправильно.
Покажи правильное по твоему.
T>Вложи в оптимизатор ATS сравнимое со вложенным в оптимизатор С количество человеко-лет, тогда можно будет сравнивать.
Опять при чем тут оптимизатор?
Сравнивался только размер исходников, ATS из-за деклараций типов получается более многословным чем си, хотя сам язык по выразительности близок к ML.
FR>>Насчет оптимизатора, он просто попытался повторить "подвиг" автора языка D который несколько лет назад тоже ваяя язык в одиночку и вообще умудрился занять весь топ на http://shootout.alioth.debian.org/ это совершенно ничего ни говорит о быстродействии языка, это говорит только о том что можно легко подогнать язык под тесты.
T>Или насколько просто на нём оптимизировать программы.
Ничего это не значит, кроме того, что возможна откровенная подгонка.
Кроме D еще несколько авторов языков занимались такой же фигней. Плюс качество многих тестов на этом ресурсе очень слабое, хотя в пследнее время есть прогресс.
T>>Именно поэтому я и считаю, что твоё сравнение неправильно. FR>Покажи правильное по твоему.
Учти время написания оптимизатора. Сколько лет ATS? Сколько лет Си?
T>>Вложи в оптимизатор ATS сравнимое со вложенным в оптимизатор С количество человеко-лет, тогда можно будет сравнивать. FR>Опять при чем тут оптимизатор? FR>Сравнивался только размер исходников, ATS из-за деклараций типов получается более многословным чем си, хотя сам язык по выразительности близок к ML.
Дай ссылку на тесты с ATS. Доступный мне shootout его не содержит.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Учти время написания оптимизатора. Сколько лет ATS? Сколько лет Си?
Опять при чем тут оптимизатор?
Тот же OCaml с никаким оптимизатором там же в одно время стоял по многим тестам на первых местах, часто опережая C++, просто нашелся человек нормально написавший тесты.
FR>>Сравнивался только размер исходников, ATS из-за деклараций типов получается более многословным чем си, хотя сам язык по выразительности близок к ML.
T>Дай ссылку на тесты с ATS. Доступный мне shootout его не содержит.
Здравствуйте, FR, Вы писали:
FR>Здравствуйте, thesz, Вы писали:
T>>Учти время написания оптимизатора. Сколько лет ATS? Сколько лет Си? FR>Опять при чем тут оптимизатор? FR>Тот же OCaml с никаким оптимизатором там же в одно время стоял по многим тестам на первых местах, часто опережая C++, просто нашелся человек нормально написавший тесты.
Я думаю, что надо подождать. И для ATS такой найдётся.
FR>>>Сравнивался только размер исходников, ATS из-за деклараций типов получается более многословным чем си, хотя сам язык по выразительности близок к ML. T>>Дай ссылку на тесты с ATS. Доступный мне shootout его не содержит. FR>Так выше уже давал FR>http://shootout.alioth.debian.org/u32/benchmark.php?test=all&lang=ats&lang2=ocaml&box=1
По моему ты вообще не читаешь что тебе пишут.
Я уже надцать раз тут повторил что меня не интересует быстродействие и оптимизатор,
особенно на этом ресурсе, который знаменит подгонками.
Мне интересна цена в выразительности которую надо платить за зависимые типы. Поэтому
все кроме объема исходников меня в этих тестах не интерсует, и по этому параметру
ATS конкретно сливает.
Здравствуйте, FR, Вы писали:
FR>Здравствуйте, thesz, Вы писали:
T>>Я думаю, что надо подождать. И для ATS такой найдётся. FR>Уже нашелся, сам автор языка.
Да, пропустил. Но по остальным параметрам он выигрывает.
FR>>>http://shootout.alioth.debian.org/u32/benchmark.php?test=all&lang=ats&lang2=gcc&box=1
T>>Отличие в скорости незначительно (не два раза), в размере исходников значительно.
FR>По моему ты вообще не читаешь что тебе пишут. FR>Я уже надцать раз тут повторил что меня не интересует быстродействие и оптимизатор, FR>особенно на этом ресурсе, который знаменит подгонками.
Так вот, возьми и напиши что-либо реальное на обычном ЯП и на ЯП с зависимыми типами. Чего на шутаут кивать, который — о, ужас! — знаменит подгонками?
FR>Мне интересна цена в выразительности которую надо платить за зависимые типы. Поэтому FR>все кроме объема исходников меня в этих тестах не интерсует, и по этому параметру FR>ATS конкретно сливает.
Может, писавший решения задач шутаута ориентировался на скорость, а не на объём исходников? Может, писавший решения задач шутаута только начал использовать свой язык и не подобрал подходящих выразительных приёмов? Может, библиотека языка пока ещё слаба и в решениях находится то, что должно быть в библиотеке?
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Для OCaml писал Xavier Leroy?
Хорош тролить
T>Так вот, возьми и напиши что-либо реальное на обычном ЯП и на ЯП с зависимыми типами. Чего на шутаут кивать, который — о, ужас! — знаменит подгонками?
ATS меня заинтересовал, но времени совсем нет
Так что жду хоть небольших примеров от евангилистов
FR>>Мне интересна цена в выразительности которую надо платить за зависимые типы. Поэтому FR>>все кроме объема исходников меня в этих тестах не интерсует, и по этому параметру FR>>ATS конкретно сливает.
T>Может, писавший решения задач шутаута ориентировался на скорость, а не на объём исходников? Может, писавший решения задач шутаута только начал использовать свой язык и не подобрал подходящих выразительных приёмов? Может, библиотека языка пока ещё слаба и в решениях находится то, что должно быть в библиотеке?
Здравствуйте, FR, Вы писали:
FR>Здравствуйте, thesz, Вы писали:
T>>Для OCaml писал Xavier Leroy? FR>Хорош тролить
Тем же концом и тебя.
T>>Так вот, возьми и напиши что-либо реальное на обычном ЯП и на ЯП с зависимыми типами. Чего на шутаут кивать, который — о, ужас! — знаменит подгонками? FR>ATS меня заинтересовал, но времени совсем нет FR>Так что жду хоть небольших примеров от евангилистов
Сам разберёшься. Не много-то и надо.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, thesz, Вы писали:
T>Тем же концом и тебя.
T>>>Так вот, возьми и напиши что-либо реальное на обычном ЯП и на ЯП с зависимыми типами. Чего на шутаут кивать, который — о, ужас! — знаменит подгонками? FR>>ATS меня заинтересовал, но времени совсем нет FR>>Так что жду хоть небольших примеров от евангилистов
T>Сам разберёшься. Не много-то и надо.
Что-то в последнее время евангилисты жидкие пошли, немерлисты не ленились простыни кода выкатывали
Здравствуйте, FR, Вы писали:
FR>Мне интересна цена в выразительности которую надо платить за зависимые типы. Поэтому FR>все кроме объема исходников меня в этих тестах не интерсует, и по этому параметру FR>ATS конкретно сливает.
Согласен. Но нет четкого доказательства, что сливает они из-за применения зависимых типов, а не почему-то еще (например, из-за кривого синтаксиса или выбора более быстрого, но более пухлого алгоритма).
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, FR, Вы писали:
FR>Здравствуйте, thesz, Вы писали:
T>>Тем же концом и тебя.
FR>
T>>>>Так вот, возьми и напиши что-либо реальное на обычном ЯП и на ЯП с зависимыми типами. Чего на шутаут кивать, который — о, ужас! — знаменит подгонками? FR>>>ATS меня заинтересовал, но времени совсем нет FR>>>Так что жду хоть небольших примеров от евангилистов
T>>Сам разберёшься. Не много-то и надо.
FR>Что-то в последнее время евангилисты жидкие пошли, немерлисты не ленились простыни кода выкатывали
Как и я в своё время.
Сейчас я немного занят.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Здравствуйте, WolfHound, Вы писали:
WH>Это позволяет доказывать кучу утверждений и как следствие не писать код обработки подавляющего большинства нештатных ситуаций ибо их просто не может быть.
Как я понимаю, код обработки нештатных ситуаций никуда не девается. Просто в случае его отсутствия программа не скомпилируется. Например, прежде чем передавать произвольные списки a : Vec A n и b : Vec B m на вход нашему zip-у, необходимо чтобы компилятор увидел код в котором мы проверяем что для а и b справедливо n = m. В противном случае система вывода типов не даст скомпилировать программу. Поэтому код проверки строго говоря никуда не девается. Он остается. Просто само количество проверок может несколько оптимизироваться.
Здравствуйте, chukichuki, Вы писали:
C>Как я понимаю, код обработки нештатных ситуаций никуда не девается. Просто в случае его отсутствия программа не скомпилируется.
Он как минимум исчезает из собственно функции Zip.
Клиенты функции Zip могут также от него избавиться.
C>Например, прежде чем передавать произвольные списки a : Vec A n и b : Vec B m на вход нашему zip-у, необходимо чтобы компилятор увидел код в котором мы проверяем что для а и b справедливо n = m.
Если эти списки читаются из внешних источников то такой код необходим.
Ибо при чтении данных из внешних источников мы вообще ничего не можем гарантировать по этому все приходится проверять.
Если же мы говорим про списки внутри программы то у меня есть чувство что в подавляющем большинстве случаев (а может и вообще всегда) можно доказать что списки одинаковой длинны без проверок времени исполнения.
C>В противном случае система вывода типов не даст скомпилировать программу. Поэтому код проверки строго говоря никуда не девается. Он остается. Просто само количество проверок может несколько оптимизироваться.
Все проверки выдавливаются на уровень получения данных из внешних источников.
А внутри программы мы уже сидим на статических доказательствах.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
WH>Здравствуйте, chukichuki, Вы писали:
C>>Например, прежде чем передавать произвольные списки a : Vec A n и b : Vec B m на вход нашему zip-у, необходимо чтобы компилятор увидел код в котором мы проверяем что для а и b справедливо n = m. WH>Если эти списки читаются из внешних источников то такой код необходим. WH>Ибо при чтении данных из внешних источников мы вообще ничего не можем гарантировать по этому все приходится проверять.
WH>Если же мы говорим про списки внутри программы то у меня есть чувство что в подавляющем большинстве случаев (а может и вообще всегда) можно доказать что списки одинаковой длинны без проверок времени исполнения.
У меня есть два возражения. Во-первых в большинстве случаев как раз все промежуточные структуры данных, фигурирующие в программе, тем или иным образом зависят от данных полученных извне. В том числе и списки, в том числе и их размер. В противном случае это уже константы, а для работы с константами существуют гораздо более действенные методы.
Во-вторых, хоть я и незнаком с теоритическими основами зависимых типов, но инженерная интуиция заставляет сомневаться, что существует какой-то более менее серьезный метод доказательства, который можно легко внедрить в транслятор языка программирования, не сильно потеряв при этом в скорости компиляции. Скорее всего используется некая разновидность вывода типов, основанная на унификации термов первого порядка со специальной обработкой условий видa n == m.
Допускаю что я неправ. Было бы любопытно посмотреть на вывод типа для той же самой простейшей функции map, который по телу функции доказал бы что размер списка на входе равен размеру списка на выходе.
Здравствуйте, chukichuki, Вы писали:
C>У меня есть два возражения. Во-первых в большинстве случаев как раз все промежуточные структуры данных, фигурирующие в программе, тем или иным образом зависят от данных полученных извне. В том числе и списки, в том числе и их размер. В противном случае это уже константы, а для работы с константами существуют гораздо более действенные методы.
Вот при загрузки в программу проверили что все согласовано, а дальше будет следить компилятор.
Скажем в 3D для экономии памяти и вычислительных ресурсов используют индексированные меши.
Скажем определение типа меша может быть таким:
Индексер массива принимает не абы какой Integer, а LimitedInteger(0, <размер массива>)
В данном случае мы проверяем при загрузке что все индексы попадают в диапазон 0 <= i < vertecesCount после чего можем спокойно брать индекс из массива indeces и индексировать этим индексом массив verteces без всяких проверок времени исполнения.
C>Допускаю что я неправ. Было бы любопытно посмотреть на вывод типа для той же самой простейшей функции map, который по телу функции доказал бы что размер списка на входе равен размеру списка на выходе.
Вот код на языке agda делающий то что ты хочешь
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
vmap : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
vmap f [] = []
vmap f (x :: xs) = f x :: vmap f xs
Здравствуйте, chukichuki, Вы писали:
C>Допускаю что я неправ. Было бы любопытно посмотреть на вывод типа для той же самой простейшей функции map, который по телу функции доказал бы что размер списка на входе равен размеру списка на выходе.
Здравствуйте, lomeo, Вы писали:
WH>>Лично я не вижу что тут может тормозить при выводе типов. L>Конечно! Потому что в твоём примере нет вывода типов
Ну если в твоем понимании вывод типов это исключительно вывод сигнатуры функции то нету. В такой постановки вопроса и в немерле вывода типов нету.
Но если посмотреть повнимательней то ты наверное заметишь что внутри функции не указано ни одного типа.
Пусть это будет просто:
просто, как только можно,
но не проще.
(C) А. Эйнштейн
Здравствуйте, WolfHound, Вы писали:
WH>Ну если в твоем понимании вывод типов это исключительно вывод сигнатуры функции то нету. В такой постановки вопроса и в немерле вывода типов нету. WH>Но если посмотреть повнимательней то ты наверное заметишь что внутри функции не указано ни одного типа.
Это уже type checker.
А то так получится, что когда я в Яве пишу выражение, то и там вывод типов работает.
Здравствуйте, lomeo, Вы писали:
L>Это уже type checker.
Ерунду какую-то говоришь. Проверка типов есть в любом языке не зависимо от наличия в нем вывода типов.
L>А то так получится, что когда я в Яве пишу выражение, то и там вывод типов работает.
Так оно и есть. Только он там не полный. Точнее очень ограничены. В шарпе, например, вывод типов несколько усилили в 3-ей версии, но все равно не довели его до уровня когда внутри методов не нужно указывать типы. В немерел в телах методов типы почти не приходится указывать. Собственно если глянут на аккуратно написанные программы на хаскеле, то не трудно заметить, что там тоже типы не указываются не везде, а только для внутренней реализации (тел функций и функций скрытых в модулях).
Если это закрепить на уровне самого языка, то никто не пострадает. Так что твой аргумент, на мой взгляд, надуман.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
