законтачился о монадные трансформеры, реализовав их (заодно манатки, заодно do-нотацию, заодно доказательства законов монад и трансформеров) в coq.

Fixpoint test1 (lst : list nat)
: idents_state Res MRes (list (nat * S.string))
:=
match lst with
| nil => ret nil
| cons h t =>
match h with
| 0 => lift (throw _ Examples.DBZ)
| n =>
id ← gen_ident;;
rest ← test1 t;;
ret (cons (n, id) rest)
end
end
.

говно, тяжёлое (по типам внутренностей), мутное, но работает, и, что удивительно, даже понравился опыт.

#onoiso

add comment recommend bookmark subscribe