vecN

[gds]

Data.VecN в окамле: https://bitbucket.org/gds/vecn/src
И, чорт возми, опять зависимые типы не пригодились. Да что за беда...

Comments

[nicka_startcev]

Когда в руках молоток...

[gds]

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

[thedeemon]

А как будет выглядеть функция конкатенации двух векторов? Чтобы из vec n int и vec m int получить vec (m+n) int,

[gds]

конечно, никак.
вот что писал в чятик по этому поводу:
(2012-03-04 12:43:17) gds: и, понятно, на параметризованных типах легко делается +1 и -1, но вот сложение -- уже нет. лично я не знаю, как сделать. то есть, конечно, можно несложным образом сделать функции типа append{2,4,8,16} и из них комбинированием лепить append11 какое-нибудь, но 1. кривота, 2. на практике этот подход вообще не нужен.

с другой стороны, в Data.VecN этой функции тоже нет. (но там-то можно запилить её, арифметика на типах получше.)

[thedeemon]

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

[gds]

стыдоба -- Data.VecN? Согласен, нельзя. Но почему-то показывают.

А вот касаемо "векторов с длиной" -- я бы сказал, что такое вообще не нужно, и для использования в том числе (следовательно, и для кодинга, и для показа):
1. векторы/массивы (как и прочее мутабельное) имеет смысл использовать только в огороженных кусках кода, где проверки на попадание в границы разместить не западло, их там будет немного, и где наружу выйдет нормальный функциональный интерфейс.
2. зависимые типы работают только на этапе компиляции и только в пределах одного бинарника, то есть, при любом межпроцессовом взаимодействии им грош цена.