なのログ

だから見てて下さい・・・俺の・・・変身

型システム入門を読んでいます(第1回)

第1回です。
はじめ第2回と書いてしまい消しました。やっぱ0オリジンってクソだわ。

それでですね、わりかし元気に読んでおります。
今3章です。と言うと進みが良いように感じられるかもしれないんですが、

1章「はじめに」:型システムとは何か、型研究の歴史とかをちょっと紹介
2章「数学的準備」:これから使っていく、集合関連の定義や帰納法の準備

といった内容です。つまりは場合によっては読まなくていいエリア。なんだこの牛歩。
ちなみに続きは、

3章「型無し算術式」:実際に(極簡単な)構文を定義して、それについて考える
4章「算術式のML実装」:まだよんでないからわかんないよ!

となっております。
そのまま32章まで。魔界かな?


で。

僕がこの本を開いて、初めにネットの海に訪ねたことを書きましょう。

記号 説明
a∈A aはAの要素 Aはaを(1要素として)含む
A⊂B 部分集合 AはBの部分集合
A∪B 和集合
A∩B 積集合
Φ ゼロ集合
/A 補集合

是非「マジかよ」と思って頂きたい。
(要するに、2章「数学的準備」の内容です)
(そして冊子中では説明されないレベルの常識)(ぶっちゃけ高校数学)

いやその、これに関しては微妙に事情がありまして、
僕、学生の頃にこの内容を勉強してないんですよね。

とはいえ、論理学っていう題目ではやることをやっていたり、
論理の証明の背理法とか帰納法っていう言葉に覚えはあったりとするので、
だいたいは大丈夫なはずです。しかし記号を扱ったことがマジで一切無かった。

というわけでググりました。
和集合と積集合がほんとにもう入ってこなくて、
ぶっちゃけこれまで生きてきた中でもこの記号達を見ては
「どっちがキャップでどっちがカップこの野郎もっとわかりやすくしろ
とブチギレていた訳ですが、今回やっと覚えられたと思います。
なんか上からきたやつ全部受け止めそうな形してるから和集合。こんなん。

ほんと、正直な願望を言うと記号に+とか✕とかORとかANDとか
書いておいて欲しすぎましたね。なんやねんこの視覚的になんでもねえ記号。(キレすぎ)

まあこんな部分で文字を連ねても仕方がないので、
つらつらと読んでいる事でも書いていこうと思います。

ぶっちゃけわからん所はわからんままに読んだりしているんですが、
とりあえず一旦一周(あるいは11章らへんまで)読んでみて、
後から見返すなどしてみたいところです。※「11章らへんまで」の理由↓
数学初心者のための「型システム入門」入門 - 廻る技術の覗き穴


3章「型無し算術式」

この章に入ったところ、すぐに言語体系が定義されました。

値として3つ

true  (定数:真)
false (定数:偽)
0     (定数:ゼロ)

関数、式(演算子)として4つ

succ t    (tの後の値)
pred t    (tの前の値)
iszero t  (tのゼロ判定)
if t then t else t (条件式)
※tは任意の項

なのやつ氏はなんだかこの時点で何もわからないまま
「お、それっぽい~」などと言いながら手を叩いて喜んでいます。猿か。

なんだか、
「とりあえず確かに?機械語寄りに考えて?どんな値でも作れそうだな?」
とか感じ取っています。

そして次のページで一文あり「っはぁ~~型無し算術式完全に理解した」とか言い始めます。

この項の構文は succ true や if 0 then 0 else 0 のような怪しげな項の形成を許すことに注意されたい。このような項については後でもっと述べることとしよう。実際、ある意味まさにこうした例のおかげで、この小さな言語が本書の目的から見て興味深いものとなっている。 (ページ18)

「それなんだよな~~俺言われる前から思ってたわ~~完全に理解した」

要は「"trueの次の値"って何だよ?」とか「"もし:0"って何がだよ?」となるよねという話で、
(Cあたりの経験のせいで"if 0"は定義できそうな気がしてしまうものの、)
「それを許す許さないってまさしく型の話~~ハァ勝った~~~」とか言っています。

余裕やな!型無し算術式!


そうは問屋が卸すめえ。

次の見開きの一角です。

[具体的な項の定義] 各自然数について、集合Siを以下のように定義する。

S0      = Φ
S(i+1)  =   {true, false, 0}
        = ∪ {succ t1, pred t1, iszero t1 | t1 ∈ Si}
        = ∪ {if t1 then t2 else t3 | t1, t2, t3 ∈ Si}

「は~~ うん ちょろい ちょr・・・ ? はい? 何て?

ここを噛み砕くのに結構かかりました。
要は冒頭の集合の記号の確認に戻ったりしました。

今はなんとかわかります。これをした意図は微妙に謎ではあるんですが。
要は「が処理ステップみたいなもので、その処理ステップ内で表現できる値を全部出しました」
みたいなことだと思っています。

ステップ数0だとなんにもなくて、
ステップ数1だとはじめから定義されている値3つ(true,false,zero)、
ステップ数2だとそいつらにそれぞれ前とか後とかゼロ判定とかifとかかけたやつ...
と、どんどん増えていく感じです。
if ~ then ~ else ~ の種類が3乗のオーダで増えていくので、わりと爆発的なやつです。

と、まあ「書いてあることはわかったけど何故それを書いたのかはわかんねえな」
という感じでここは納得をしました。
上述の処理ステップ的な事で正解してろ・・・!という気持ちしかない。

あとなんかSiに含まれる項tに対して、
内部に現れる定数の集合を Const() とする定義、
性質として
Size()(直線に連なった処理の数)と
Depth()(分岐の中で一番処理が多い数)というものが導入されました。

「せやな」と思って流し読みました。
使われる様子が出てこないと・・・わからないんだ・・・俺・・・。


3.5 「評価」

章は少し進みまして、3.4 「意味論のスタイル」とかを軽く読み飛ばしつつ
現在この部分を読んでいます。

さっきまで処理ステップが進むたびにいたずらに長くなっていた式に対して、 ifとかの処理を進めて評価して、結果的にこの値だよね、ということをするのが書いてあるっぽいです。
それとなくプログラミング屋に馴染みのありそうな内容な気がして、するっと読めそうな気はします。

ぶっちゃけあと2ページとかで3.6「注記」を含めて3章が終わるところまで読んでいるんですが、
わりと文字を連ねた気がするのでここで区切っておきます。

次回はこの型無し算術式を解析して評価する感じだと思います。そいでは。

ぐだぐだクソコード vol.1 はじめてのテトリス by F#

こんにちはこんばんは。

皆様お待たせ致しました。ぐだぐだクソコードの時間です。
(※元ネタです: だらだらクソデッキ vol.1 - | 晴れる屋

諸般の事情によりテトリスを作ることとなり、
あろうことかF#で挑んできました、という回です。

いや、どうやらちゃんとした人たちからすれば
ちゃんとしたコードを書けるらしい >Tetris | F# Snippets んですが、

長らく自分の頭で考える事の無いコーディングしかしないクソ作業員であった僕は
やはり(プログラマとして)ちゃんとした人などでは全くなかったらしく、
書きはしたもののとんでもねえクソコードを生み出す結果になってしまったため、
反省と精進のため、ここに公開セルフコードレビュー記事を起こそう、となった次第です。

f:id:nanoyatsu:20180918230632p:plain
図1.「とりあえず動いたよ」アピに必死ななのやつ氏

続きを読む

型システム入門を読んでいます(第0回)

どうしてまたそんな・・・

  • ~よくわからない方向け~
    これです↓

    型システム入門 −プログラミング言語と型の理論−

    型システム入門 −プログラミング言語と型の理論−

    • 作者: Benjamin C. Pierce,住井英二郎,遠藤侑介,酒井政裕,今井敬吾,黒木裕介,今井宜洋,才川隆文,今井健男
    • 出版社/メーカー: オーム社
    • 発売日: 2013/03/26
    • メディア: 単行本(ソフトカバー)
    • クリック: 68回
    • この商品を含むブログ (11件) を見る

  • ~あらすじ~
    Kotlinを書いているぼく「なんか型推論微妙だなあ」
    その発言を感知した知人「F#と比べるのはさすがに・・・」
    型の技術とかよくわかってないぼく「エッそういうもんなの?どういうのが違うの?」
    自称つよくないつよいプログラマの知人「型システム入門を読み切ったらまた会おう・・・」
    無知無知ボディ(?)のぼく「なにそれは」
    言うより手を動かす知人「スッ(amazonリンク)」
    手がすべりやすいぼく「手がすべった!!!!!(購入)


・・・というわけで、完全に超難易度の書籍なんですけど、買ってしまったからには読む所存です。
計画(?)としては、普段の開発をしつつぼちぼち読み、
週イチくらいで読書記録を記事にしていけたらなあという気持ちです。

昨日の夜買って寝る前に1時間くらいページをめくった訳ですが、
なんかしんどい所を多少読み飛ばしたにも関わらず、Kindleが指しているのは20ページ目でした。ワハハ。
(ページカウント前の序文とかもあったはあったわけですが)

まあそんな感じです。
難度はこれから上がっていく一方です。確実に寄り道して予習が必要だと思います。どうなる次回。

ではまた!

なんか書いとかな回

なんか色々していますというおはなし。

前回が8/3。

  • その時点でなんか書こうとしていたもの:
    Unityで地図のパズルとか作っていたので、そのときに学んだことでもメモっておこうかな

  • それ以降から今に至るまで書けるなとおもったもの:
    Unityで知育ミニゲームを作ったので、そのときに学んだことでもメモっておこうかな
    F#でWPFをしたので、そのときに(ry
    F#でテーブルゲーム(QUARTO!)を実装しようとしてやめた
    昨日からAndroidStudio でKotlinをしはじめました

とかとかそんなんこんなん。
そしてそれらの内一つも記録にしていないので僕は弱いな・・・みたいなお話。

あとはgithubに初めてリモートリポジトリを立てたりしました。
クソコード置いてます。はずかしいのでまだリンク置けません。(今更)

まあそんなんです。
とりあえずKotlinをさわりだしたので、今日1日でAndroidでなんか動くやつできたらなあという感じです。

おわり。


ついき。(2018/09/12)
Androidのやつ、「なんか動く」モンなんかできやしねえよといいますか、
ローカルから画像ファイルを選んで表示する、ってだけのことができただけで「やったああああああ」って叫んでるレベルでした。
そのへんの中身のはなし(ていうか画像いじって保存するところまでいきたい)はまたこんど。

はじめまして回

とりあえず作っただけなんですけど、の回。

 

プログラム書く人です。メモを置いていこうという話です。

Qiitaのnanoyatsu 

qiita.com

Twitterのnanoyatsu

twitter.com

 

こいつです。(どちらも同じくほぼまっさら)

 

ブログとqiitaを両方持つ行為、なかなかどうして意味を見失いそうなんですけど、まあとりあえずですよね、とりあえず。(とりあえずと言えば許されるのか)

 

Unityでちょっとモノをつくったので、

まずはそのときに使ったことのメモでも置くかー、という気持ちです。

 

それではまたかきます。