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

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

Так я же тебе объясняю

А я же объясняю — врапер вокруг теории пишется не сложнее врапера вокруг интерфейса (твой второй пункт).

а при добавлении зависимых типов объем работ возрастает на порядки

У меня evidence для такого факта нет.

И доказательства корректности, откуда и будет гора.

at : {A : Set} {n : ℕ} → Vec A n → (i : ℕ) → {_ : i < n} → A
-- 
-- ^ Вот, главным образом, то что ниже это деталь реализации для Vec (списки).
-- 
at [] _ {()}
at (x ∷ _) 0 = x 
at (_ ∷ xs) (suc n) {s≤s p} = at xs n {p}
-- 
-- С настоящим вектором будет просто
-- 
-- at x i = at# x i
-- 
-- где at# уже небезопасен, всё равно сигнатура знает что i < n.

xs : Vec ℕ 3
xs = 1 ∷ 2 ∷ [ 3 ]

t : ℕ → ℕ
t i with i <? 3
... | yes p = at xs i {p}
... | no _ = 0
-- 
-- ^ тут бы хотелось, чтобы p в первой ветке протаскивался автоматически, 
-- адаптация с заменой with (dependent pattern-matching) на dependent-if
-- и даст
-- 
-- if (i < 3) { return xs[i]; } else { return 0; }

не вижу никакой горы в данном случае.

Ну например как-то так

1) Это не Haskell98 и даже не Haskell2010 — если уж использовать расширения GHC, то сразу GHC 7.8 в котором это уже можно (?) сделать, но GHC это зависимые типы — http://stackoverflow.com/questions/12961651/why-not-be-dependently-typed#1324.... 2) -Wall — -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. 3) Тут типы вместо термов же для Nat. 4) Я просил компилируемый и работающий с main.

А вообще непонятно как это делать — c DataKinds непонятно как писать (n + m) в Array, с TypeLits computational не заводится (так что unsafeCoerce). С TypeFamilies всё ещё нужно костылять термы на типах:

{-# LANGUAGE KindSignatures, TypeFamilies, TypeOperators, GADTs #-}

data Z
data S a

type family x :+ y :: *
type instance Z :+ y = y
type instance S x :+ y = S (x :+ y)

infixr 5 :.
data Array (a :: *) :: * -> * where
  E :: Array a Z
  (:.) :: a -> Array a n -> Array a (S n)

infixr 4 ++.
(++.) :: Array a n -> Array a m -> Array a (n :+ m)
E ++. ys = ys
x :. xs ++. ys = x :. (xs ++. ys)

Если только TypeNats заработают в будущем релизе.

Берем обычную полиморфную функцию id: a -> a. Мы в нее на место типового аргумента может подставить значение синглтон, которое представляет тип на уровне термов (например там Bool, String и т.д.) и имеет тип Type. Вуаля, это зависимые типы!!11!

Ничего не понял. «представляет тип на уровне термов» — мозги динамикой сломал?

void f(size_t);
template <size_t n> void g() { f(n); }
void test() { g<5>(); }

size_t в шаблоне это обычный size_t, никакой не сахар.

Шаблоны плюсов - это по факту ограниченные макросы

#include <type_traits>
template <typename T> struct A { static_assert(false, "A"); };
template <typename T> struct B { static_assert(false, "B"); };
int main() { B<A<void>> x; }

Стратегия вычислений не macro-like (http://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion), а самая обычная. Ну и мне всё равно — я пишу программу с шаблонами которая компилируется или нет, что там внутри происходит меня не волнует (но на макросы не похоже, см. выше).

Ты показал _обычный полиморфизм_

Вот это — http://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A0-types, там даже пример такой же (Vec), http://en.wikipedia.org/wiki/Dependent_type#Systems_of_the_lambda_cube — first order dependent type theory. В «простой полиморфной лямбде» этого нет. Что такое «обычный полиморфизм» я не знаю. «макросы обычные syntax-rules» над «типизированной лямбдой» это в раздел НФ.

Если ты показываешь полиморфизм

А тут я показываю рекурсивную шаблонную структуру / функцию <typename, size_t> -> typename / Set → ℕ → Set, без всяких разночтений. Опять же, в обычном полиморфном (параметрически, с подтипированием) этого нет, но есть в зависимых типах, ну и в шаблонах C++ — почему я должен думать про какие-то левые макросы над лямбдой мне не понятно.

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