mzp

わかめモナ化: Maybeモナドの証明 + Coq入門

証明の重要性

• うかつにモナドと言うと刺される

例: jQueryはモナドだ - id:anatooのブログ

「jQueryはモナドである」と主張したけど、証明はなかったのですぐに刺された。

JQueryがモナドかどうかとか - たけをの日記＠天竺から帰ってきたよ

kazu-yamamoto

module Main where

import Control.Monad
import Control.Monad.Free
import Prelude hiding (putChar, getChar)
import qualified System.IO as IO
import Test.QuickCheck

----------------------------------------------------------------
-- Our DSL

myuon

\abf.fab
= \abf.(I f)(K (ab)f)
= \ab.SI(K(ab))
= \ab.(K(SI)(ab))(K(ab))
= \ab.S(K(SI))K(ab)
= \ab.(K(S(K(SI))K) b)(a b)
= \ab.S(K(S(K(SI))K))ab
= S(K(S(K(SI))K))

nna774

-- オセロ
--import Data.Functor
import Maybe
import Control.Monad

data Color = Black | White deriving (Eq, Show, Read)

type Cell = Maybe Color

type Board = [[ Cell ]]

penguin2716

#-*- coding: utf-8 -*-
Plugin.create :gray_protected_users do
  UserConfig[:protected_users_background_color] ||= [0xcccc,0xcccc,0xcccc]

  filter_message_background_color do | mp, array |
    if mp.to_message.user[:protected] == true
      array = UserConfig[:protected_users_background_color]
    end
    [mp, array]
  end

yukelog.rb

#! /usr/bin/ruby -Ku

$udid = 'aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa'
HOST = 'yukeyusha4iphone.appspot.com'
YYVER = '3.0.1'

require 'net/https'
require 'rubygems'
require 'json'