LINUX.ORG.RU

История изменений

Исправление quasimoto, (текущая версия) :

давай-ка это на один из известных мне ЯП переложим, хорошо?

Всё равно что говорить «давай-ка переложим шаблоны C++ на известный мне Си». Если Agda или подобный язык тебе не известны, то в C++ (или, там, Haskell) ты не найдёшь нужных для написания этой программы штук, так же как в Си не найдёшь шаблонов.

А то вот такая хрень: «ℕ» у мну никуда не лезет.

У тбу есть GMP и вообще — http://pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c/.

Если в C++ добавить парочку фич, то переписать можно так:

Nat fib1_rec(Nat a, Nat b, Nat n) {
    return n == 0 ? a : fib1_rec(b, a + b, n - 1);
}

Nat fib1(Nat n) {
    return fib1_rec(0, 1, n);
}

Nat fib2(Nat n) {
    return n < 2 ? n : fib2(n - 2) + fib2(n - 1);
}

template <Nat m, Nat n>
Eq<fib1_rec(fib2(m), fib2(m + 1), n), fib2(m + n)>
go() {
    return
        n == 0 ?
        cong(fib2, sym(n_plus_zero_eq_n<m>())) :
        trans(go<m + 1, n>(),
              cong(fib2, sym(m_plus_one_plus_n_eq_one_plus_m_plus_n<m, n>())));
}

template <Nat n>
Eq<fib1(n), fib2(n)>
fib1_eq_fib2() {
    go<0, n>();
}

где у Nat и его операций, у Eq, sym, cong, trans, n_plus_zero_eq_n, m_plus_one_plus_n_eq_one_plus_m_plus_n есть соответствующие определения (тоже требующие этих фич, но вполне пишущиеся).

Тут, кстати, видно почему запись ResultType f_name(ArgType) из C/C++/Java/C#... не Ъ и более удобна в перспективе (таких фич) запись f_name(ArgType) ResultType как в *ML/F#/Rust/Haskell/Scala/Agda/... (+ если учесть квантификации или implicits из Haskell или Scala/Agda — мы вводим имена на которые могут быть зависимости в типах слева на право, так что в сигнатурах можно обойтись вообще без свободных имён).

Исходная версия quasimoto, :

давай-ка это на один из известных мне ЯП переложим, хорошо?

Всё равно что говорить «давай-ка переложим шаблоны C++ на известный мне Си». Если Agda или подобный язык тебе не известны, то в C++ (или, там, Haskell) ты не найдёшь нужных для написания этой программы штук, так же как в Си не найдёшь шаблонов.

А то вот такая хрень: «ℕ» у мну никуда не лезет.

У тбу есть GMP и вообще — http://pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c/.

Если в C++ добавить парочку фич, то переписать можно так:

Nat fib1_rec(Nat a, Nat b, Nat n) {
    return n == 0 ? a : fib1_rec(b, a + b, n - 1);
}

Nat fib1(Nat n) {
    return fib1_rec(0, 1, n);
}

Nat fib2(Nat n) {
    return n < 2 ? n : fib2(n - 2) + fib2(n - 1);
}

template <Nat m, Nat n>
Eq<fib1_rec(fib2(m), fib2(m + 1), n), fib2(m + n)>
go() {
    return
        n == 0 ?
        cong(fib2, sym(n_plus_zero_eq_n<m>())) :
        trans(go<m + 1, n>(),
              cong(fib2, sym(m_plus_one_plus_n_eq_one_plus_m_plus_n<m, n>())));
}

template <Nat n>
Eq<fib1(n), fib2(n)>
fib1_eq_fib2() {
    go<0, n>();
}

где у Nat и его операций, у Eq, sym, cong, trans, n_plus_zero_eq_n, m_plus_one_plus_n_eq_one_plus_m_plus_n есть соответствующие определения (тоже требующие этих фич, но вполне пишущиеся).

Тут, кстати, видно почему запись ResultType f_name(ArgType) из C/C++/Java/C#... не Ъ и более удобна в перспективе (таких фич) запись f_name(ArgType) ResultType как в *ML/F#/Rust/Haskell/Scala/Agda/... (+ если учесть квантификации или implicits из Haskell или Scala/Agda — мы вводим имена на которые могут быть зависимости в типах слева на право, так что в сигнатурах и всех их частях можно обойтись вообще без свободных имён).