Про асерти і анархію інваріантів

[dmytrish]

Писав я тут вчора SECD-машину (сьогодні вона нарешті змогла додати 2+2 :) ) на хтонічному Сі, і все більше замислювався про корисність асертів у різних точках програми: вони дають можливість вивіряти навіть те, що не сильно помістилось би і навіть у систему типів Хаскеля: рантаймові властивості, властивості, що залежать від значення і так далі.

Comments

[ex_juan_gan]

Я как раз задумываюсь, а как, собственно, определить эту категорию (ну или систему типов), в которой наши частичные функции определены; для этого же нужно, чтобы на уровне компиляции были задаваемы типы "все целые, представимые в виде суммы двух простых.

[dmytrish]

Я вот знаю, что это куда-то в направлении dependent types, но пока что дальше хелоуворлда на Coq не прошел. А мои знания математики за всем этим меня вообще просто огорчают.

Что вы имеете в виду под частичными функциями?

[ex_juan_gan]

Ну вот возьмём Скалу, к примеру; там есть частичные функции - предикат, сужающий область определения, и функция, заданная только на этой суженной области определения. Не знаю, как это выразить на Хаскеле.

Проблема ещё в том, что предикат - похоже, единственный способ определить подтипы, а это уже влечёт теоретико-множественную аксиому выделения. Грубо говоря, в языках нынче типов маловато будет.

Кок с Агдой меня немного смущают, я вижу там сплошные "множества", а это не вполне адекватная база. Но у меня недостаточно знаний, чтобы точно судить.

[sassa_nf]

я, конечно, чайник, но не означает ли аксиома выбора возможность паттерн-матчить значение по его типу? т.е. Left отличить от Right?

Мне кажется, зависимые типы как-то с ко-продуктами должны быть связаны. У меня чёткой картины не получается, но такое ощущение, что тип, от которого зависимость - это индексирующий сетоид, как в определении ко-продукта. В таком случае, аксиома выбора здесь есть по построению.

[sassa_nf]

о, асерти - это вешчь

[dmytrish]

М-да, я тут зрозумів елементарне, див. апдейт до поста.

[sassa_nf]

Так, логічно. Я їх так і використовую. Деякі речі не вдається виразити асертами, бо, скажімо, посилаються на глобальний стан системи.

типу так:

QNode h=head;
for(p=h; p.next != null && p.next.t <= t; p=p.next);
if (!head.compareAndSet(h,p)) return;
// assert: we own nodes from h to p inclusive

[archervarius]

чувак, тебе треба срочно напоїть

[dmytrish]

До наступної твоєї рецензії напишу такий же комент)

[archervarius]

налякав їжака гузицею)