Чтобы добавлять сообщения и комментарии, .

@qnikst:
qnikst

#2862276/1433 @vt почини или сними лимит на сообщения из жаббера, пожалуйста

@qnikst:
qnikst

У идриса какая-то проблема, если понимать что делаешь то можно вывести все доказательства показать пруфы и даже отрицания, и даже тоталити чеккер что-то разумное делает. Но если не понимать, то можно получить совершенно безумные доказательства, точнее выводы, хотя в разумном языке просто ничего не должно получаться. Надо будет потом попробовать агду затестить или даже сразу кок и посмотреть что во взрослых языках

@qnikst:
qnikst

plus_right_zero : (n, m : Nat) -> n + m = n -> m = 0
plus_right_zero _ Z Refl impossible
plus_right_zero (S ) Refl impossible

вот это мне сгенерировал идрис, и это прошло totality check, по его мнению n+m=n на натуральных числах невозможно

@qnikst:
qnikst

via #2862770 . Кстати, из серии q1,q2,q3... самые низкие требования к сети были у q2.
В него реально было играть на модеме 11k (блин я забыл скорости) при аналоговой аст, кроме этого ещё red alert нормально работал. Когда атс сделали цифровой, то можно было играть даже в half-live 1..

// интересно сколько фактических ошибок и неправильных терминов у меня в посте

@qnikst:
qnikst

А в tmux есть какой-нить режим подсвечевания нужных слов по регекспам разными цветами, чтобы логи глазами парсить

@qnikst:
qnikst

Кому книжка нужна?

@qnikst:
qnikst

У тут есть:
data Foo = Bar | Baz
есть класс
class FooBool (t::Foo) where toBool :: proxy t -> Bool
instance FooBool 'Bar where toBool _ = False
instance FooBool 'Foo where toBool _ = True

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

@qnikst:
qnikst

как отучиться путать ветки then и else и не сойти с ума?

@qnikst:
qnikst

И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?

@qnikst:
qnikst

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

@qnikst:
qnikst

на прогулке
— сейчас 274 по кельвину!

@qnikst:
qnikst

вот почему написано, что все хорошо, ведь если lock сервис не находится в том же месте что и storage, то у нас тот же race?

@qnikst:
qnikst

ну наконец-то этот пылесос хоть как-то начал работать.. теперь ещё отлаживать целый день

@qnikst:
qnikst

Если вы встретите человека, который говорит что Haskell должен быть строгим по умолчанию — предложите ему пописать на Idris недельку

@qnikst:
qnikst

Кто-нить в lmdb шарит?

#if SIZE_MAX > MAXDATASIZE
if (data->mv_size > ((mc->mc_db->md_flags & MDB_DUPSORT) ? ENV_MAXKEY(env) : MAXDATASIZE))
return MDB_BAD_VALSIZE;
#else


вот кусок кода, у меня стоит MDB_DEVEL, поэтому MAX_KEYSIZE=0, поэтому если запрос запускается с MDB_DUPSORT, то получается, что я всегда попадаю в data->mv_size > 0 => MDB_BAD_VALSIZE?

это так и задумано или бага?

@qnikst:
qnikst

а у каких плашнетов не будет проблем с linux (nixos, gentoo) и вообще какие хорошие?

@qnikst:
qnikst

НЕНЕВИЖУ! НЕНАВИЖУ этих highlevel программистов, которые делают охренено умные высокоуровневые обёртки к низкоуровневым либам, при этом обрезая очень важные возможности!

Вам это не нужно говорили они! это усожняет интерфейс говорили они! вы сделаете все медленным говорили они!!!!!!!!!!

@qnikst:
qnikst

1.hs:46:44: error:
    • Could not deduce: q ~ (a0 -> q0)
      from the context: Cxq t q
        bound by the type signature for:
                   foo :: Cxq t q => V t -> [Def] -> [Val] -> q -> Exq t q
        at 1.hs:44:1-55
      or from: t ~ 'S a
        bound by a pattern with constructor:
                   :. :: forall (a :: S). String -> V a -> V ('S a),
                 in an equation for ‘foo’
        at 1.hs:46:6-12
      ‘q’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (t :: S) q.
                 Cxq t q =>
                 V t -> [Def] -> [Val] -> q -> Exq t q
        at 1.hs:44:8
    • In the second argument of ‘(.)’, namely ‘q’
      In the first argument of ‘(=<<)’, namely ‘foo ss df vals . q’
      In the expression:
        foo ss df vals . q =<< fs =<< getValue s defs vals
    • Relevant bindings include
        q :: q (bound at 1.hs:46:23)
        foo :: V t -> [Def] -> [Val] -> q -> Exq t q (bound at 1.hs:45:1)


проблема т.к. у меня kind q зависит от значения (и типа) V t, если это V Z то kind *,  если V (S t) то * -> *.
это как-нить вообще обходится?

@qnikst:
qnikst

есть монатка (оперэйшнл, который интрепретируется), есть в ней всякие методы например:
insert :: Node -> Device -> Location -> Blah Q z ()
есть логирование, оно достаточно хитрое, оно создает контексты работы с элементом, т.е.
сказали что работаем с нодой Q, и дальше до конца фазы или контекста стейт машина логов будет это знать.
соотественно, в insert хорошо бы гарантировать, что контексты для Node,Device созданы и передавать тупо Location.
Но как это сделать непонятно, вариант 1 это делать implicit-aми, но у нас их считают bad practice, второе это делать какой-то хитрый Reader по гетерогенному рекорду, ещё вариант какой-нить monad-classes или что там у Ромы было?
С последними, я не уверен, что это не усложнит интерпретатор, по хорошему интерпретатор в другой либе вообще не должен меняться

@qnikst:
qnikst

TFW приходишь в детскую библиотеку, а там книг многих интересных авторов меньше, чем дома