タグ

ブックマーク / mandel59.hateblo.jp (3)

  • プログラム意味論の分かりやすい紹介 - Ryusei’s Notes (a.k.a. M59のブログ)

    巷に膾炙しているプログラム意味論の説明は、正直言って何を言っているのか、部外者にはよく分からないように感じられる。プログラムの意味を論じる「プログラム意味論」の意味がよくわからないというのは末転倒だろう。ここでは、プログラム意味論を分かりやすく紹介したい。 プログラムの意味 プログラム意味論とは、プログラムの意味に関する理論だ。 そもそも「意味」とはなんだろうか。「意味」の意味を知るために、デジタル大辞泉で調べてみよう。 1 言葉が示す内容。また、言葉がある物事を示すこと。「単語の―を調べる」「愛を―するギリシャ語」 2 ある表現・行為によって示され、あるいはそこに含み隠されている内容。また、表現・行為がある内容を示すこと。「慰労の―で一席設ける」「―ありげな行動」「沈黙は賛成を―する」 3 価値。重要性。「―のある集会」「全員が参加しなければ―がない」 いみ【意味】の意味 - goo国

    komlow
    komlow 2019/06/24
  • Phantom property pattern - Ryusei’s Notes (a.k.a. M59のブログ)

    TypeScriptは、JavaScriptエンジンの動的セマンティクス上に、静的な型システムのセマンティクスが重なっているものです。ここで、JavaScriptとしては正しく実行できても、TypeScriptの型システム上ではちゃんと型が付かないという場合もあります。ときには、TypeScriptで型がつくように大幅に書き換えないといけない場合も出てきたりして、そうなると大変です。それでも、TypeScriptの型システムは高度な機能を持っているので、大体の場合は、うまく表現してやると、JavaScriptらしい書き方のままで型をつけることができてしまいます。今回は、JavaScriptでよくある、プリミティブ値をそのまま取り回すパターンに型を付けたいと思います。 プリミティブ型を扱うプログラミングは、素朴でわかりやすいですが、型の考えからするとかなり悪いものです。こういうプログラミング

    Phantom property pattern - Ryusei’s Notes (a.k.a. M59のブログ)
  • 依存型の表現力と逆問題 - Ryusei’s Notes (a.k.a. M59のブログ)

    Idrisみたいに、函数プログラミングを前提にしている言語には函数を合成する演算が標準で用意されているよね。 (.) : (b -> c) -> (a -> b) -> a -> cこの演算子を使うと、函数を合成してくれる。函数の合成を使えば、プログラムを変数を使わないで書くことができる。 整数を文字列にする : Integer -> String 整数を文字列にする = show 最初の文字を得る : String -> Char 最初の文字を得る = strHead 整数を文字列にして最初の文字を得る : Integer -> Char 整数を文字列にして最初の文字を得る = 最初の文字を得る . 整数を文字列にするPrologよりも簡単だね。 でも、プログラミングでは、引数を複数持つ函数を使うことはよくあることだ。そして、函数プログラミングを前提にしている言語では、そういう函数は普通

    依存型の表現力と逆問題 - Ryusei’s Notes (a.k.a. M59のブログ)
  • 1