IT練習ノート

IT関連で調べたこと(実際は嵌ったこと)を書いています。

CoqからHaskellのコードを生成する

Extractionという機能を使うとできるらしい。Coqで証明してHaskellで動作させる感じなのか。

coq.inria.fr

単純な方の定義

Inductive FBB : Type :=
  | Foo
  | Bar
  | Buzz.

Require Extraction.
Extraction Language Haskell.
Extraction "C:\work\FBB.hs" FBB.
module FBB where

import qualified Prelude

data FBB =
   Foo
 | Bar
 | Buzz

偶数判定は以下のように変換される。

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.
module Evneb where

import qualified Prelude

data Bool =
   True
 | False

data Nat =
   O
 | S Nat

evenb :: Nat -> Bool
evenb n =
  case n of {
   O -> True;
   S n0 -> case n0 of {
            O -> False;
            S n' -> evenb n'}}

Haskellのモナドを圏論的に理解するスライド

数学でいうモナドの定義と、Haskellで普段使っているモナドの定義は、一見違うように見えるが、実は、クライスリカテゴリを通じて、同じだという話(雑な理解)。

http://emorehouse.web.wesleyan.edu/research/talks/monad_rosetta.pdf

the seemingly different concepts of monad from category theory andfunctional programming actually coincide.

自分なりのイメージなので、このスライドを読んでいて気づいたこと(意味不明だけど)。 * 自然変換で、議論しているときに、コンポーネントに着目している場合がある。 * 自然変換の水平な合成は、ポイントワイズの値をプログラム言語のパラメータとしてみたときに、パラメータに対して、合成した自然変換を同時に処理するのではなく、合成前の自然変換を、順次パラメータを処理していく感じみたい。

Kindの入門記事

diogocastro.com

記事を読むには以下のextensionの理解が必要。

どこかに日本語訳があるはずなのだが、見つけられなかった。

ラムダ式があのように表現されている意図

ラムダ計算を学ぶときに最初に読んでおくとよいと思った。(というか自分にとっては今が最初だけど)

sites.google.com

 "f(x)"という表記法の欠陥は、高校の数学までではほとんど表面化しませんが、 大学に入ってから定義域や値域が関数の集合になるような 高階関数(オペレータとか作用素とも呼びます)を扱いだすとすぐわかります。

http://www.fuka.info.waseda.ac.jp/~onono/ProgLang/charts/pl2007-CS-09-LambdaCalculus.pdf

写像としての関数fそのものを表しているのか(つまり、xは特定の要素ではなく、定義域中の任意の要素を表す変数として書かれている)。それとも、特定の要素xへの適用を表しているのか、文脈によっては不明瞭になる

あと、定義域、値域を決めたうえでの関数を考えているわけではないことも。

分った積りの積分定数

例えば、

不定積分とは、積分の範囲をどこからどこまで、という範囲を指定していませんので、積分の範囲が不定になっている積分のことです。

(中略)

※記号のCは積分定数なのでその中身はいくつの数でも構いません。Cを置くことにより原始関数の全ての数が1つの関数として表わされます。

とあって、確かに、そのように高校で授業で習った(学習した)記憶があります。ただ、正直「モヤモヤ」感は残っていました。

下記のページを読んでいたら、「モヤモヤ」感が晴れる感じがしてきました。

積分定数が記載された時の=は、暗黙的に同値類を考慮している」っていう雑な理解であっているのかな。

また、記事を書いた目的は違うけど、二人が同じ数式log(1/|x|)を取り扱っているのが興味深いですね。

variantの小さなサンプルを書いてみた

extensibleパッケージのvariantの使い方を確認するために小さなサンプルを書いてみました。

やりたいことは、

data A = AX | AY deriving (Show, Eq)
data B = BY | BZ deriving (Show, Eq)

と定義したときに、ABを合わせたデータ(構造)を(簡単に)定義し、(簡単に)つかいたい

ということです。

data AB = A A | B B deriving (Show, Eq)

このように定義できますが、AB型でのデータコンストラクA,Bが冗長なので何とかしたいということです。

extensiblevariantでなんとかなるとおもったのですが、実際に書いてみると、それはそれで記述量が多くなると感じました。

データコンストラクタを書かなくてよいのですが、代わりに、ラベルを書く必要があるので、今回のやりたいことの場合extensibleをつかうメリットはないかなと思いました(まだ理解できていないだけかも)。

Variant sample

catamorphism, anamorphism, histmorphism, dynamorphismの概要をつかむ記事

45deg.github.io

個人的に慧眼だったのは、不動点の節の説明での発想の転換の部分でした。

そもそもリストを関手で表現したいならば、こう定義した方がよさそうに見えます。 (2) List:=1+Int×List

しかしこれでは定義自身にList

が含まれる、いわゆる再帰的定義となってしまいます。

そこで、(2)を「方程式」とみなし、その方程式を満たすような List を「リストを表すデータ型」とする発想の転換をします。しかし、型同士の等式は = ではなく 同型 ≃ で結びます。