Dependent Types

[voidex]

Не раз видел упоминания на www.rsdn.ru, где говорилось, что с их помощью можно написать функцию, соединяющую 2 списка, при этом гарантирующую, что длина результата будет суммой длин аргументов.
Теперь, что меня интересует. Как выглядит реализация? Пишу на Си++, ибо в нем мне легче понять, во что это превратится в конечном итоге:
1.

template int L> class List { ... };

template int L1, unsigned int L2>
List concat (List const &Left, List const &Right) { ... }
template int L>
bool equal (List const & Left, List const & Right) { ... }Syhi-подсветка кода

2.

class BaseList { public: virtual unsigned int Length() const = 0; }
template int L> class List : public BaseList {
public: unsigned int Length() const { return L; }
... };

BaseList & concat (BaseList const &Left, BaseList const & Right) { ... }
bool equal (BaseList const &Left, BaseList const & Right) {
  if (Left.Length() != Right.Length()) { /* функция не подходит */ }
  ...
}Syhi-подсветка кода

В первом случае мы обязаны знать на этапе компиляции длину списка, т.е. прочесть список из файла не получится.
Во втором мы это можем сделать, но тогда мы можем получить два списка, длина которых при компиляции будет неизвестна,
и что тогда произойдет, если два списка с разными длинами передать в equal?