Эффективнее, чем что?

Нельзя купить плохую книгу на языке оригинала? Вон сколько помоев на автора practical ocaml вылили, думаю, не просто так.

Эффективнее чем ждать перевода + чем потом пытаться понять, что же хотел сказать автор и почему все так плохо в русском варианте. Хотя, конечно, книги от O'Railly, переведенные, если не ошибаюсь, издательством «Питер», как минимум несколько лет назад, были весьма неплохи.

[code

zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]

[/code] [code] zip7 as bs cs ds es fs gs = getZipList $ (,,,,,,) <$> ZipList as <*> ZipList bs <*> ZipList cs <*> ZipList ds <*> ZipList es <*> ZipList fs <*> ZipList gs [/code] Аппликативные функторы рулят и бибикают

> zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]

zip7 as bs cs ds es fs gs = getZipList $ (,,,,,,) <$> ZipList as <*> ZipList bs <*> ZipList cs <*> ZipList ds <*> ZipList es <*> ZipList fs <*> ZipList gs

Аппликативные функторы рулят и бибикают.

>> Его фишки - квинтенсенция всех успешных идей в программировании, за последние 20 лет в одном флаконе.

Нет там зависимых типов *хотя бы* на уровне с++ и системы эффектов.

Или capability calculus, например.

Кстати, в C++ нет зависимых типов.

только идиот будет пользоваться языком в котором пробелы имеют значение.

Э-э-э...

strlen("     ")

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

Можно пример плз какой-нить. Интересно на это глянуть.

Называется Haskell. «Пометка» пишется как [code] import System.IO.Unsafe [/code]

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

Можно пример плз какой-нить. Интересно на это глянуть.

Называется Haskell. «Пометка» пишется как

import System.IO.Unsafe

> зависимые типы: как на хаскеле сказать

const int n=17;

...

Z<n> f(int x) { return mod<n>(x+(n/2)); }

Оно станет зависимыми типами в тот момент, когда с n уберётся модификатор const.

> Оно станет зависимыми типами в тот момент, когда с n уберётся модификатор const.

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

> Кстати, в C++ нет

Смелый вывод.

Давай ссылку на 1) хорошее определение зависимых типов 2) описание задачи, которая требует зависимых типов и не ложится на плюсы (ну или наваяй тут)

> Или capability calculus, например.

опять же интересна ссылка

Capability Calculus, that supports region-based memory management, не?

> Capability Calculus, that supports region-based memory management, не?

Угу.

Давай ссылку на 1) хорошее определение зависимых типов

На строго формальное сходу не дам, но на вменяемое - http://en.wikipedia.org/wiki/Dependent_type

2) описание задачи, которая требует зависимых типов и не ложится на плюсы

Тип данных «список»; функция «убрать последний элемент», которая не позволит скомпилировать программу, если хотя бы в какой-то момент её применят к пустому списку (ещё раз: ошибка должна обнаруживаться при компиляции!); функция main, которая случайным образом выбирает число n от 0 до 10000, создаёт список длины n и применяет к нему предыдущую функцию n раз.

> Тип данных «список»; функция «убрать последний элемент», которая не позволит скомпилировать программу, если хотя бы в какой-то момент её применят к пустому списку (ещё раз: ошибка должна обнаруживаться при компиляции!); функция main, которая случайным образом выбирает число n от 0 до 10000, создаёт список длины n и применяет к нему предыдущую функцию n раз.

Я попробую, вполне возможно получится (тут нужны рассуждения на уровне succ pred zero).

Вот только после этого ты войдешь во вкус и объявишь, что этого мало, а еще требуются рассуждения на уровне «нечетное простое число представимо в виде суммы двух квадратов, экви оно равно 1 по модулю 4».

Это я к тому, что границу «где зависимые типы, а где нет» ты провел произвольно, и из твоей ссылки она не следует.

Под рассуждениями понимаются рассуждения времени компиляции.

> Я попробую, вполне возможно получится

Не получится. Ни на плюсах, ни на хаскеле. Если, конечно, не сделать ветвление на десять тыщ веток.

границу «где зависимые типы, а где нет» ты провел произвольно

Эта граница достаточно хорошо известна. По той же ссылке есть список языков, где зависимые типы есть (в той или иной мере). В C++ их нет.

Просто ТИП одной переменной может зависеть от ЗНАЧЕНИЯ другой (при том, что полностью сохраняется статическая типизация). В то время как в плюсовых шаблонах параметрами может быть только то, что при компиляции известно, то бишь - не переменные. И усё.

мне твой пример как-то не нравится (n-n=0)

поэтом я предлагаю свой

допустим, у нас есть тип Matrix<m,n> и операция умножения матриц

когда m,n — константы, то применимость умножения ясна

однако нам хочется запустить прогу, ввести в stdin натуральное число x, затем ввести пару матриц Matrix<m,х> и Matrix<х,n> (m,n — константы) и вычислить и вывести произведение этих матриц

система типов должна обеспечить невозможность умножить матрицы если x!=x (надеюсь, ясно о чем я)

это все делается в плюсах с полпинка.

> а еще требуются рассуждения на уровне «нечетное простое число представимо в виде суммы двух квадратов, экви оно равно 1 по модулю 4».

Под рассуждениями понимаются рассуждения времени компиляции.

Могут и пригодиться. В принципе, такие вещи вполне на языке зависимых типов доказываются.

> однако нам хочется запустить прогу, ввести в stdin натуральное число x, затем ввести пару матриц Matrix<m,х> и Matrix<х,n> (m,n — константы) и вычислить и вывести произведение этих матриц

система типов должна обеспечить невозможность умножить матрицы если x!=x (надеюсь, ясно о чем я)

это все делается в плюсах с полпинка.

OK, показывай, интересно. Думаю, если ты пропустишь сам процесс ввода матриц, я переживу.

> По той же ссылке есть список языков, где зависимые типы есть (в той или иной мере)

ключевые слова — в той или иной, и главное — там не приведен критерий по которому их туда запихали, а на тему почему нет с++ в обсуждении этой статьи тоже невнятное бормотание.

> ключевые слова — в той или иной

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

C++ туда не входит, потому что в нём нет типов, зависящих от рантаймового параметра.

> OK, показывай, интересно. Думаю, если ты пропустишь сам процесс ввода матриц, я переживу.

я видимо так и сделаю завтра в этом треде

однако надо решить принципиальный вопрос — если относительно целых чисел (от которых зависит тип Matrix) компилятору известно только то, что x==x, и *неизвестно* (и вероятно не может быть объяснено), что (3х-х)/2==х, будет ли это зависимые типы?

Кстати, хаскельный аналог целочисленных параметров в темплейтах тоже существует - type-level arithmetics.

Простейший вариант выглядит так: [code] data Z = Zero newtype S n = Succ n [/code] После чего вместо const int n = 3 можно использовать тип S (S (S Z)). Довольно стандартная техника, правда, в менее удобных обозначениях.

> однако надо решить принципиальный вопрос

А он важен для твоего решения?

Может, хоть намекнёшь, какая там идея?

Пдц.

data Z = Zero
newtype S n = Succ n

> что (3х-х)/2==х

на самом деле в это видимо можно заставить компилятор *поверить*, но только силой, и проверить он тебя не сможет

> Может, хоть намекнёшь, какая там идея?

параметром шаблона может быть любой статический объект, и сравнивать их адреса компилятор умеет

если это не покатит, есть другие варианты, надо пробовать все же

> А он важен для твоего решения?

да, важен — если нужна проверяемость логики вида (3х-х)/2==х (а не навязывание ее силой), то лучше и не браться

посему нужно полноценное определение зависимых типов

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

> По-моему, мы договорились уже: нужна проверяемость равенства размеров двух матриц (слушай, давай для простоты будем не произведение матриц, а скалярное произведение векторов считать?)

скалярное произведение векторов годится

а насчет проверяемости мне так и не понятно до конца, вот на псевдокоде:

std::cin >> x;
Vector<x> a;
Vector< 3*a.dim > b;
double z0 = b*a; // ошибка компиляции
Vector< (b.dim-a.dim)/2 > c;
double z1 = c*a; // х.з., скорее всего не смогу, но идеи есть.
Vector<x> d;
double z2 = a*d; // реально

> std::cin >> x;

Vector<x> a;

В этот момент всё и обломится. x - не константа и параметром шаблона быть не может.

> В этот момент всё и обломится. x - не константа и параметром шаблона быть не может.

я ж не дурак и сказал «на псевдокоде»

я тебя спрашиваю про «double z1 = c*a» — если ее компилятор не съест (ругнется), будет ли вектор зависимым типом?

Извини, псевдокод слишком неконкретен, чтобы я мог хотя бы понять твой вопрос.

На самом деле, статически гарантировать, что два вектора имеют ОДИНАКОВУЮ длину, в общем-то, несложно. В Хаскеле. А вот гарантировать, что они имеют длину, равную тому n, которое введёт пользователь - таки нельзя.

data Nil = Nil
data Succ a = Succ Float a
class Prod a where prod :: a -> a -> Float
instance Prod Nil where prod Nil Nil = 0
instance Prod a => Prod (Succ a) where prod (Succ f1 a1) (Succ f2 a2) = f1 * f2 + prod a1 a2
test :: Prod a => Integer -> a -> a -> Float
test 0 a1 a2 = prod a1 a2
test n a1 a2 = test (n-1) (Succ (n^2) a1) (Succ (n^3) a2)

> Извини, псевдокод слишком неконкретен, чтобы я мог хотя бы понять твой вопрос.

я думал ты поймешь.

а так придется тупо все переписывать словами, хотя это с другой стороны все-таки надо.

ладно, перепишу и запощу вместе с плюсовым кодом.

/me представил «менее удобные обозначения» для n=9000 и ужоснулсо...

> /me представил «менее удобные обозначения» для n=9000 и ужоснулсо...

Это же простейший вариант. Можно, например, двоичную систему сделать, будет короче.

$ ghci GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. Prelude> (. )( .) (\_ _ -> ()) () (\_->()) () () Prelude>

$ ghci
GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
Prelude> (. )( .) (\_ _ -> ()) () (\_->()) ()
()
Prelude>

О мой анонимный друг, пролей свет своей учёности на нас, необразованных, и объясни, на кой хрен ты это написал?

выглядит клёво, а это:

(. )( .)

как бэ намекает на молодежную ориентированность языка

Ну да, функция «сиськи», открыли Америку.

Вы ещё про значение «жопа», обозначаемое (_|_), вспомните.

Оно вызывает плохие ассоциации у адептов. Ведь это символ всего, что не хаскель.

Анонимус вероятно хотел попугать нас ASCII-артом.

Я же запостил свой вариант на с++ (а не псевдокоде) в development:

http://www.linux.org.ru/view-message.jsp?msgid=4299185

OK, переехали туда.

Да я понимаю, но выглядит все-равно по марсиански. Впрочем, те же решения я видел и в HOL, но там они прикрыты синтаксическим сахаром.

>Сделали же они из окамла F#. Вот можд теперь и за хаЦкель решили взяться... :)

- http://php.cin.ufpe.br/~haskell/haskelldotnet/
- http://www.galois.com/~sof/hugs98.net/

не? :)

Пусть их... :)

Похоже, они умерли ещё в 2003

> http://php.cin.ufpe.br/~haskell/haskelldotnet/

Releases

No releases yet.

Latest News

2003-12-13 Haskell.NET website released

http://www.galois.com/~sof/hugs98.net/

The latest release (March 2003) is available in Windows Installer form via http.

Ну, значит, оно им не надо :)