История изменений
Исправление quasimoto, (текущая версия) :
let n = 10 in n, терм «n» тут какой - нормализованный, ненормализованный?
Ну let обычно добавляют (http://www.cis.upenn.edu/~bcpierce/sf/MoreStlc.html#lab613) в конструкторы термов вместе с правилами редукции и типизации, так что let n = 10 in n =>beta 10.
Ну так что, значит нельзя в агде применить zip к спискам, чья длина неизвестна на момент компиляции? Но при этом присутствует доказательство равенства их длины?
В агде? Вообще zip _уже_ принимает списки одинаковой длины, так что вопрос откуда они взялись — 1) они по построению могут быть такие, 2) есть статические регионы, то есть проверили один раз в рантайме каким-то предикатом (не имеет отношения с Vec или zip) и передаём всё со свидетельствами в zip, либо вопрос в функциях вида 3) {n : Nat} -> List A -> Vec A n, 4) {n : Nat} -> Stream A -> Vec A n, 5) g : IO Nat, f : (n : Nat) -> Vec A n, f <$> g — 3) {A : Set} → (xs : List A) → Vec A (length xs), а List тут откуда взялся? сводится к 5), 4) наверно, это будут CoVector с Coℕ, так что сводится к 3), также, сама коиндукция отдана на откуп компилятора или интерпретатора (примитивы в нормальной форме), 5) IO отдано им же (тоже), про то что MAlonzo позволяет конструировать типы динамически я уже говорил.
А вот в C++, DML, ATS (хотя про эти два я точно не знаю — может как-то можно, но я сомневаюсь) только 1) и 2) в силе (или около того).
Ничего, что это про омегу?
В зависимых типах — тем более (если уже в омеге).
Вот и в плюсах твоих - ага, редуцируется
Ну так я говорю:
#include <cstddef>
template <size_t x> struct f { enum { result = x * 2 }; };
constexpr size_t g(size_t x, size_t y) {
return x * y * x * y;
}
#include <cstdio>
int main() {
printf("%d\n", f<g(2 * 4 + 3 * 5, 6 * 8 + 7 * 9) + 100500>::result);
}
// movl $.L.str, %edi
// movl $13236618, %esi # imm = 0xC9F98A
// xorb %al, %al
// callq printf
во что там у тебя m+n редуцируется, позволь-ка узнать?
Есть для него правила редукции? Нет, всё что есть для _+_ это 0 + y => y и suc x + y => suc (x + y), так что будут редуцироваться все константы и все термы с переменные по графу таких редукций.
А все что ты описываешь - это редукция в омеге.
Ну а начиная с LF так же и термы редуцируются (там в синтаксисе T t).
А если выразительность систем совпадает, то..? Сам закончишь?
Удобство, не? Подоказывай ты теоремки и свойства на ATS и на GHC (там же _можно_ накостылять всё на типах и операторах, в принципе).
Исходная версия quasimoto, :
let n = 10 in n, терм «n» тут какой - нормализованный, ненормализованный?
Ну let обычно добавляют (http://www.cis.upenn.edu/~bcpierce/sf/MoreStlc.html#lab613) в конструкторы термов вместе с правилами редукции и типизации, так что let n = 10 in n =>beta 10.
Ну так что, значит нельзя в агде применить zip к спискам, чья длина неизвестна на момент компиляции? Но при этом присутствует доказательство равенства их длины?
В агде? Вообще zip _уже_ принимает списки одинаковой длины, так что вопрос откуда они взялись — 1) они по построению могут быть такие, 2) есть статические регионы, то есть проверили один раз в рантайме каким-то предикатом (не имеет отношения с Vec или zip) и передаём всё со свидетельствами в zip, либо вопрос в функциях вида 3) {n : Nat} -> List A -> Vec A n, 4) {n : Nat} -> Stream A -> Vec A n, 5) Ex {n : Nat} -> IO (Vec A n) — 3) {A : Set} → (xs : List A) → Vec A (length xs), а List тут откуда взялся? сводится к 5), 4) наверно, это будут CoVector с Coℕ, так что сводится к 3), также, сама коиндукция отдана на откуп компилятора или интерпретатора (примитивы в нормальной форме), 5) IO отдано им же (тоже), про то что MAlonzo позволяет конструировать типы динамически я уже говорил.
А вот в C++, DML, ATS (хотя про эти два я точно не знаю — может как-то можно, но я сомневаюсь) только 1) и 2) в силе (или около того).
Ничего, что это про омегу?
В зависимых типах — тем более (если уже в омеге).
Вот и в плюсах твоих - ага, редуцируется
Ну так я говорю:
#include <cstddef>
template <size_t x> struct f { enum { result = x * 2 }; };
constexpr size_t g(size_t x, size_t y) {
return x * y * x * y;
}
#include <cstdio>
int main() {
printf("%d\n", f<g(2 * 4 + 3 * 5, 6 * 8 + 7 * 9) + 100500>::result);
}
// movl $.L.str, %edi
// movl $13236618, %esi # imm = 0xC9F98A
// xorb %al, %al
// callq printf
во что там у тебя m+n редуцируется, позволь-ка узнать?
Есть для него правила редукции? Нет, всё что есть для _+_ это 0 + y => y и suc x + y => suc (x + y), так что будут редуцироваться все константы и все термы с переменные по графу таких редукций.
А все что ты описываешь - это редукция в омеге.
Ну а начиная с LF так же и термы редуцируются (там в синтаксисе T t).
А если выразительность систем совпадает, то..? Сам закончишь?
Удобство, не? Подоказывай ты теоремки и свойства на ATS и на GHC (там же _можно_ накостылять всё на типах и операторах, в принципе).