2012-01-01から1年間の記事一覧

ラムダ計算で代数的データ型を表現する方法

ラムダ計算でEither Either型の値をパターンマッチする状況を考えます。 「データコンストラクタのパターンマッチ」は,下図のようにしてラムダ計算で表現できます。 ラムダ計算でBool 今度は,Bool型の値をパターンマッチする状況を考えます。 TrueやFalse…

Boolの代わりにEither () ()を使って,論理演算をポイントフリースタイルで定義

Bool Either () () true Left false Right この記事では,上記の対応付けを使って,ポイントフリースタイルで論理演算を定義します。 否定 not の定義 a not a true false false true notを定義するには,ArrowChoiceの(|||)を使います。 not :: Either () (…

curry,(&&&),(|||)の型が,指数法則と対応している

3つの指数法則 指数法則を数式から型に書き換える 数式 型 b -> a Either a b (a, b) この表の通りに指数法則を書き換えると,こうなります。 (a, b) -> c = a -> (b -> c) (a -> b, a -> c) = a -> (b, c) (a -> c, b -> c) = (Either a b -> c) これらは,…

フィボナッチ数列は相互再帰だという話

この記事では,Haskellの記法を使います。 自然数は以下のように定義しておきます。 data Nat = Zero | Succ Nat フィボナッチ数列を計算する関数 典型的な定義 fib Zero = Zero fib (Succ Zero) = Succ Zero fib (Succ (Succ n)) = fib n + fib (Succ n) 2…