CoqからHaskellのコードを生成する
Extraction
という機能を使うとできるらしい。Coq
で証明してHaskell
で動作させる感じなのか。
単純な方の定義
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の入門記事
記事を読むには以下のextension
の理解が必要。
KindSignatures
ExplicitForAll
MagicHash
ConstraintKinds
DataKinds
PolyKinds
TypeInType
どこかに日本語訳があるはずなのだが、見つけられなかった。
ラムダ式があのように表現されている意図
ラムダ計算を学ぶときに最初に読んでおくとよいと思った。(というか自分にとっては今が最初だけど)
"f(x)"という表記法の欠陥は、高校の数学までではほとんど表面化しませんが、 大学に入ってから定義域や値域が関数の集合になるような 高階関数(オペレータとか作用素とも呼びます)を扱いだすとすぐわかります。
http://www.fuka.info.waseda.ac.jp/~onono/ProgLang/charts/pl2007-CS-09-LambdaCalculus.pdf
写像としての関数fそのものを表しているのか(つまり、xは特定の要素ではなく、定義域中の任意の要素を表す変数として書かれている)。それとも、特定の要素xへの適用を表しているのか、文脈によっては不明瞭になる
あと、定義域、値域を決めたうえでの関数を考えているわけではないことも。
分った積りの積分定数
例えば、
- 数学の不定積分の説明 不定積分|もう一度やり直しの算数・数学
不定積分とは、積分の範囲をどこからどこまで、という範囲を指定していませんので、積分の範囲が不定になっている積分のことです。
(中略)
※記号のCは積分定数なのでその中身はいくつの数でも構いません。Cを置くことにより原始関数の全ての数が1つの関数として表わされます。
とあって、確かに、そのように高校で授業で習った(学習した)記憶があります。ただ、正直「モヤモヤ」感は残っていました。
下記のページを読んでいたら、「モヤモヤ」感が晴れる感じがしてきました。
不定積分について izumi-math.jp
積分定数とは何だったのか tsujimotter.hatenablog.com
「積分定数が記載された時の=は、暗黙的に同値類を考慮している」っていう雑な理解であっているのかな。
また、記事を書いた目的は違うけど、二人が同じ数式log(1/|x|)
を取り扱っているのが興味深いですね。
variantの小さなサンプルを書いてみた
extensible
パッケージのvariant
の使い方を確認するために小さなサンプルを書いてみました。
やりたいことは、
data A = AX | AY deriving (Show, Eq) data B = BY | BZ deriving (Show, Eq)
と定義したときに、A
とB
を合わせたデータ(構造)を(簡単に)定義し、(簡単に)つかいたい
ということです。
data AB = A A | B B deriving (Show, Eq)
このように定義できますが、AB
型でのデータコンストラクタA
,B
が冗長なので何とかしたいということです。
extensible
のvariant
でなんとかなるとおもったのですが、実際に書いてみると、それはそれで記述量が多くなると感じました。
データコンストラクタを書かなくてよいのですが、代わりに、ラベルを書く必要があるので、今回のやりたいことの場合extensible
をつかうメリットはないかなと思いました(まだ理解できていないだけかも)。