(blog ‘lucindo)

… vem o Herrmann e manda:

Herrmann (5:49):
Cara, minha revelação do dia: me liguei que o axioma K (L(p>q)>(Lp>Lq)) de lógica modal é isomórfico ao operador de aplicação de mônadas (ap :: Monad m => m (a -> b) -> m a -> m b), de acordo com o isomorfismo de Curry-Howard
Herrmann (5:50):
Acho que rola usar um método de tableaux analítico pra ajudar a compilar
Lucindo (5:50):
entendi lhufas

Update: ele achou depois um link sobre isso. E eu continuo não entendendo.

Seguindo instruções do Herrmann..

algor:~ lucindo$ ghci
   ___         ___ _
  / _  /  // __(_)
 / /_// /_/ / /  | |      GHC Interactive, version 6.6.1, for Haskell 98.
/ /_\/ __  / /___| |      http://www.haskell.org/ghc/
____// /_/____/|_|      Type : ? for help.

Loading package base ... linking ... done.
Prelude> let fibs = 1 : 1 : zipWith (+) fibs (tail fibs)
Prelude> take 10 fibs
[1,1,2,3,5,8,13,21,34,55]
Prelude> zip [1..] "lisp"
[(1,'l'),(2,'i'),(3,'s'),(4,'p')]
Prelude>

Achei muito doce.