Є, значить, тут теоремка із першого розділу Software Foundations:

Theorem andb_eq_orb:
forall (b c : bool), (andb b c = orb b c) -> b = c.

( малозв’язні спроби довести >>> )

Стан справ у моїй віртуальній машині SECD: після того, як я таки наважився ввести в її пам’ять heap для масивів, все понеслось із великою швидкістю і зараз це уже більше Scheme, ніж PicoLisp ( Read more... )

CEK-машини взагалі уміють рахувати нумерали Чорча?

Прості приклади типу (λx.λy.x) 1 2 обчислюються, але коли я намагаюсь обчислити succ one, де succ = λn.λf.λx.f (n f x), one = λf.λx.f x, і мій доморощенний CEK-інтерпретатор, і я вручну упираємось у стан < clos(λf.λx.f (n f x), E1) | E1 | nil > де E1 = { n -> clos(λf.λx.f x, {}) }, хоча в ідеалі ( Read more... )

Чому монади ніхто не порівнює із stream? Поки що всі приклади монад, які я знаю, більш-менш вкладаються в поняття stream, потоку:

• [a] - потік даних, потенційно нескінченний. Причому, як мені зараз здається, варто було б розрізняти список як тип даних і як скінченний об’єкт у eager-сенсі і як контрольну структуру для виконання, lazy stream (простий ( Read more... )

Вчора довго намагався зрозуміти оце:

data Fin : Nat -> * where
Fz : {n : Nat} -> Fin (Succ n)
Fs : {n : Nat} -> Fin n -> Fin (Succ n)

Намагався розписати вручну елементи, присутні в Fin 2, це Fs 2 (Fz 2) та Fz 2, я правильно розумію? Тобто саме невизначеність того, чи Fz, чи Fs, дозволяє на кожному кроці або створити більше число, або ( Read more... )

Дивлюсь тут курс Function Reactive Programming від Одерського і сотоваріщі ( Read more... )

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

Колись давно я почав вчити Lisp із Common Lisp. Чому саме цей діалект? Це зрілий, випробуваний часом, стандартизований, потужний діалект, що допускав різноманітні підходи, тобто він відповідав всім вимогам, які тоді здавались мені хорошими. Тільки це викинуло зі мною злий жарт: я помилився в практично кожному із цих пунктів. «Зрілий і випробуваний ( Read more... )