プログラミング好きの備忘録

関数型言語とか、証明とか

すごいH写経:7章おしまい

前に出てきた"nudge"って単語の意味を調べてみました。意味は「そっと動かす」でした。moveとニュアンスが異なるようです

さて、すごいHの写経7章が終わりました。dataキーワードによる型の定義はすんなりと理解できたのですが、型クラス、またそのインスタンスについては今まで学んだことのない話なので難しかったです。

P142から抜粋
・型クラスは、特定の振る舞いを定義する
・定義されたとおりに振る舞うことのできる型は、その型クラスのインスタンスにされる

Functorについてはおぼろげながら理解。11章でまたやるらしいので、本気で理解するのはその時に。


:k というghciのコマンドは初めて知りました。
ghci> :k Int
Int :: *
これの意味するところは、「Intは具体型である」

ghci> :k Maybe
Maybe :: * -> *
「Maybeは1つの具体型を取って1具体型を返す型コンストラクタである」

減少性が示せない?

一日ごろごろしてました。
ほとんど成果ないですが、引っかかっているポイントが浮かび上がってきたので、メモしておきます。


Haskell
前回の畳み込みを使った表現がまだ解決していない

Coq
4で割ると3余るならば真を返す関数が定義できない

Fixpoint is_4n_3 (n:N) : bool :=
match n with
| N0 => false
| Npos xH => false
| Npos (xO xH) => false
| Npos (xI xH) => true
| Npos n => is_4n_3 (n-3)
end.

この関数を定義しようとすると、
Recursive call to is_4n_3 has principal argument equal to "n - 3"
というエラーメッセージが。
調べたところ、Coqさんが引数の減少性をわかってくれてくれていないとのこと。

なんで n > n-3 って当たり前のことをわかってくれないのかと思ったら、
N_scopeでの引き算では 0 - 3 = 0 になるからか。
パターンマッチの文脈的に、n>3の場合を考えているんだけど、その意を汲み取ってもらえなかった
いったいどうすれば。

まあ、今やりたいことをするだけだったらmodを使えばいいのですが。


知ったことメモ
Haskell divと(/)は型が違う
糖衣構文だと思ってました汗

すごいH写経:6章

8/30にやったことまとめ。執筆しているのは8/31なのですが、記事の日にちと一日ずれるのはどうかと思ったので昨日の日付で投稿します。

やったこと:すごいH本、6章写経(~P102,章の2/3くらいまで)
意外と進まなかったという印象。覚えたことやひっかかったところをメモしておきますね



Data.Listモジュール

nub :: (Eq a) => [a] -> [a]
リストから重複する要素を取り除く関数

gourp :: (Eq a) => [a] -> a
リスト内で、隣接する同一要素をリストでまとめる関数

isInfixOf :: (Eq a) => [a] -> [a] -> Bool
a `isInfixOf` b は、aがbの先頭に含まれているかを判定してBoolを返す

find :: (a -> Bool) -> [a] -> Maybe a
find p lst はリストの中でpがtrueになる最初の要素をMaybeに包んで返す。
見つからなかったらNothingが返る


Data.Charモジュール

digitToInt :: Char -> Int
'0'から'9','A'から'F','a'から'f'の文字を数字に変換する。
ASCIIコードを返すわけではないので注意。


わからなかったこと(P102)
findKey :: (Eq k) => k -> [(k,v)] -> Maybe v
findKey key xs = foldr (\(k,v) acc -> if key==k then Just v else acc) Nothing xs

再帰より畳み込みのほうが読み易く理解しやすい(誰が見ても畳み込みだと分かる)とのことなのですが、何をどう畳み込んでいるのかよくわかっていません。
Nothingでひっかかっているのか、そうではないのか。改めて考えます。

すごいH写経

「夏休み何してた?」という問いに対して胸を張って答えられるといいと思っています。

ソフトウェアの基礎はともかく、TAPLを進めるのはきつい… 当初よりだいぶ目標が下がっていますが、すごいHの写経を終わらせるのをあと1ヶ月の目標とします。

友人「夏休み何してたのー?」
私「すごいH写経した(ドヤ」
友人「キモッ」
こうなること請け合いですね!


そんなわけで、今日はすごいHの5章を写経しました。


覚えていなかったこと・もの

elem :: (Eq a) => a -> [a] -> Bool
aがリストに含まれているかを判定する関数

replicate :: Int -> a -> [a]
replicate n a はaをn回繰り返したリストを返す関数

otherwiseはガードの時だけではなくパターンマッチの時にも使える(当たり前なんだけど…)

明日は一日フリーなので、6章と7章が進められるんじゃないかと思っています。
10章あたりまでは知っていることの再確認なので素早く進められるはず。

ソフトウェアの基礎、継続中

ソフトウェアの基礎、115ページまで。

演習問題はoptional,recommendedであるものはやってません。

多相性の部分はXをどこに置くのかはっきり理解しておらず、コンパイルエラーが起きているので後回しに。先に高階関数のほうに進みます。


いずれは証明駆動開発をしてみたいので、ためしにExtractionコマンドを使ってみた。
fanc関数をHaskellに変換する場合は、

Extraction Language Haskell.
Extract Inductive list => "()" ["" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".

Extraction "foo.hs" fanc

しかし、
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".
の部分でなぜかコンパイルが通らない。謎。

ググってみても、CoqからHaskellへのに関する日本語のページが少なすぎる。英語読まなきゃだめか?

この部分をコメントアウトすると変換は一応できるが、HaskellのInt型ではなくて(Coqのような)Nat型になってしまう。

時間ばかり食うので、Haskellへの変換は後回しにすることにした。


TAPL
まったく進んでない...


明日からサークルの合宿です。移動時間が片道2時間だから、TAPL持っていって読もうかな

ソフトウェアの基礎

今日は8月に入って初めての、予定がまったく入っていない日でした。
自分で設定した、夏休みの課題を推めることにしました。

・TAPL
読み始めると(遅々ながら)のめり込むことができる。でも、とっかかりが難しい。

というわけで、今日はTAPLは進まなかった(意志を強く持て!)

・ソフトウェアの基礎
TAPLの作者が書いた本、の翻訳版。媒体は電子書籍。Coqの入門書。
これを進めました。主に写経です。

今日の進捗は15ページから初めて64ページまで。文字が大きいせいもあって、本全体では1134ページ


学んだこと
・列挙型の宣言
・simpl, intros, rewrite, destruct, case, inductionなど。このへんは前にCoq触ったときに使ったことがある。

レベル3以上の練習問題が解けなかった。日を改めて、あきらめずに再挑戦しよう。


#Coqはおもしろいんだけど、こればっかやってるとJavaが身につかないんだよな...