January 8th, 2009

with Cat The Cat

Наткнулся.

У обычных векторов типы элементов не зависят от позиции. Это просто вектора, вектора векторов (матрицы) и тп.

Но можно определить вектор, у которого тип элемента от позиции зависит:
data DVec {n : Nat} {e : Nat -> Set} : Set1 where
    DNil : DVec zero (e zero)
    DCons : {n : Nat} -> {e : Nat -> Set} -> (e (succ n)) -> DVec n e -> DVec (succ n) (e (succ n))
(Agda2, не проверял за отсутствием на компьютере)

Это нижне-треугольные матрицы, ленточные матрицы (ну, нижняя часть ленты).

Вроде, полезная штука.

Однако реализацию операции reverse я для неё придумать не могу.

reverse можно определить для векторов фиксированной длины. Наверное. ;)
with Cat The Cat

Почему не .Net.

Mono 2.0.

Вкратце - сборщик мусора и кодогенератор работают плохо. Поэтому производительность программ на Mono значительно ниже производительности на .Net. Плюс, утечки памяти на Mono.

Поэтому .Net всё ещё остаётся вотчиной Microsoft.

Хочешь переносимости - не используй .Net.

via c_void.