デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル - 檜山正幸のキマイラ飼育記 (はてなBlog)
最近、「おおおー、これは凄い、すんばらしい！」と思ったことがあるので、それについて書きます。 最初に言葉についてのお断り； "categorical"の訳語をどうしようか？ と。片仮名で「カテゴリカル」が無難ですが、漢字で書きたい。「圏論的」が落ち着きがいいようですが、必ずしも「論」の意味を含まないときもあります。そこで、以下、「圏的」を使います。 [追記 date="2013-02-12"]入門的解説を書きました。→「衝撃的なデータベース理論・関手的データモデル 入門」[/追記] スピヴァックと関手的データモデル デイヴィッド・スピヴァック（David I. Spivak, http://math.mit.edu/~dspivak/）は、MITの研究者です。 彼は圏的情報学（categorical informatics）を提唱しています*1。圏的情報学の中心的な概念が関手的データモデル
関手的データモデル入門 2：統一的に制約を書く方法 - 檜山正幸のキマイラ飼育記 (はてなBlog)
夢のような話も楽しいけど、今日は地道に行きましょう。様々なスキーマ制約を、単純な発想だけを使って、すべて一様に扱う方法を紹介します。 それにしても、「入門 2」なんて番号付けていいんでしょうかね？ 「衝撃的なデータベース理論・関手的データモデル 入門」を「入門 1」とみなすつもりですが、「入門 3」「入門 4」があるかどうか不安。 内容： データたちのいるところ 集合と部分写像 従業員と事業所の例 主キーと外部キー 従属性（冗長性） ビジネスルール スキーマにおける制約記述法のまとめ データたちのいるところ 関手的データモデルは、データベース理論を極限まで単純化します。基本概念は、テーブル、カラム、制約の3つだけです。この3つだけであらゆることを記述しようとします。背後に、対象、射、可換図式だけであらゆることを記述する圏論があるので大丈夫、ってことです。 そうはいっても現実は複雑です。複雑
Tagged union - Wikipedia
In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type, or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which type is in use. It can be thought of as a type that has s
JSX のアレな所 - ぐるぐる～
注意！このエントリは既に古いので、JSX の進化速度が半端ない - ぐるぐる〜もあわせて読んでください。最新のコードを参照するのが手っ取り早いです。 JSX なる言語がリリースされました。 この言語が謳っているのが、 高速 安全 簡単(生産性が高い、とも) という 3 点です。 高速と安全はまぁいいでしょう*1。 問題は、はたしてこの言語は簡単なのか？という点です。 簡単かどうかは人によるのでアレなのですが、まぁ一部の人にとっては簡単とは言えない (というか書く気がしない) 書き方を強制されるのです。 関数型 数値を受け取って文字列を返す関数を表す型は、JSX では以下のように書きます。 function(:number):string これ単体で見ると分かりやすそうな気配はします。 では、これ読めますか？ function f(g: function(:number):number):
fogus: A Functional Programming Influence Graph
Send More Paramedics λ λ λ Fogus' Thoughts on life, programming, and thinking ❤ c clj erl pl frink fth cl org pure icl qi ❤ Follow me on Twitter... or RSS... Run this blog in mobile 2023 2022 2021 2020 2019 2018 2017 2016 2015 2014 2013 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 May 2, 2012 With the help of Twitter friends1 I developed a directed graph of traditionally functional progr
CS61A, Spring 2012 Online Textbook
CS61A: Online Textbook This book is derived from the classic textbook Structure and Interpretation of Computer Programs by Abelson, Sussman, and Sussman. John Denero originally modified if for Python for the Fall 2011 semester. It is licensed under the Creative Commons Attribution-ShareAlike 3.0 license. Contents HTML Versions Chapter 1: Building Abstractions with Functions Chapter 2: Building Abs
関数型言語の技術マップ
要求開発アライアンスの定例会で『Object-Functional Analysis and Design: 次世代モデリングパラダイムへの道標』というタイトルでセッションを行うことになりました。 セッション時間が50分なので、かなり俯瞰した形での全体像の説明になりそうですが、関連する要素技術の数が多いのと、内容が込み入っているので、ブログで補足説明をすることにしました。 今回はその第一弾です。 「関数型言語の関連技術」として用意した以下の図を説明します。関数型プログラミング言語レベルの説明はScalaを対象にします。 Disclaimer2008年にScalaをはじめて足掛け4年、関数型プログラミングとは、どうも数学を使ってプログラミングしていくことらしい、ということが分かってきました。 ScalaをBetter Javaとして使うのであれば、そこまで頑張らなくてもよいのですが、関数型言
Iterator パターンの本質 · eed3si9n
2011-12-17 これは Scala Advent Calendar 2011 の 17日目の記事です。 specs2 の作者であり、@etorreborre としても活発に発言を続けるシドニーの強豪 Eric Torreborre さんが書いた “The Essence of the Iterator Pattern” を翻訳しました。翻訳の公開は本人より許諾済みです。翻訳の間違い等があれば遠慮なくご指摘ください。 2011年6月24日 Eric Torreborre 著 2011年12月17日 e.e d3si9n 訳 去年読んだ論文で一番気に入ったのは “The Essence of the Iterator Pattern”（以下、EIP）だ。これを読んだ後で、今まで何年も使い続けてきたあるものに対する考えがガラリと変わった。それは、for ループだ。 この論文の中からいくつか
Haskellの講義に関するQ&A - あどけない話
岡山大学で、関数プログラミングの講義を一コマ担当しました。資料は、函数プログラミングの集いで使った関数プログラミングの道しるべを流用しました。ちゃんと用意しなくて、講義を受けた学生には申し訳ないです。 講義内容に関して質問を頂きました。同じような疑問を持つ人も多いと思いますので、担当教官の許可を得てここに公開します。 永続データプログラミングの意義は分かったが，破壊しないと効率が悪いのではないですか．配列のような構造が世の中には多い気がします．メモリは足りなくなりませんか． 基本的に永続と呼ばれているデータは、共有の効率が高く、しかも不要になった部分はすぐに GC に回収されます。また、GHC の GC はすごく優秀であることが知られています。 Haskell では、下位のレイヤーではデータを破壊できて、たとえば固定長のバッファーを使い回すといったことも可能です。ただ、それは普通のプログラ
モナド則三度 - あどけない話
「モナド則再び」で書いた「モナド則1」は何の訳に立つのかという問題ですが、"Monads for functional programming" に答えが載っていました。 以下のような加算機を考えます。 data Term = Con Int | Add Term Term data M a = M a deriving Show instance Monad M where return x = M x M x >>= f = f x eval :: Term -> M Int eval (Con a) = return a eval (Add t u) = do a <- eval t b <- eval u return (a + b) 論文には、M の実装が載っていないので、適当に作りました。Maybe でもいいでしょう。 こういう風に動きます。 式1: eval (Add (Co
QAで学ぶMonad - あどけない話
この記事は、Monad でつまづいた Haskeller のための Monad 再入門です。 Monadとは何ですか？ Monad とは、単なる型クラスの一つです。難しいという風評もありますが、それ以上でもそれ以下でもありません。 この型クラスのメソッドは、return と >>= です。 class Monad m where (>>=) :: m a -> (a -> m b) -> m b return :: a -> m a つまり、以下を満たす型の集合が Monad です。 m a で表現できるように一つの型変数を格納するコンテナ型 >>= と return を実装 return は新しいコンテナを作り、>>= は二つのコンテナを合成します。 Monad のインスタンスは失敗系と状態系に大別できます。以下に代表的なインスタンスを示します。 失敗系: Maybe、[] (リスト)
カリー化談義 - あどけない話
最近、スタートHaskellで「カリー化された関数のメリットは何か？」という質問が出た。そのすぐ後に、kmizuさんがカリー化の誤用に対して警鐘を鳴らしてしていた。僕からするとkmizuさんの「カリー化の定義」も誤用に思えたので、調べるとともに考えたことのまとめ。 いろんな定義 「カリー化する」という用語は、すくなくとも以下の3つの意味で使われているようだ。 部分適用という意味 これは明らかに間違い 「複数の引数を取る関数」を「一引数を取る関数のチェインに直す」こと これはkmizuさんの定義。世間でもよく使われる。 「構造体を一つ取る関数」を「構造体のメンバーを複数の引数にばらし、一引数を取る関数のチェインに直す」こと これは僕の定義。というか、Haskellコミュニティの定義。 「部分適用」の意味で使うのは明らかに間違いのなで排除。定義2と3について議論する。あとで、部分適用とは何かに
Rubyで関数型プログラミング - 貳佰伍拾陸夜日記
Rubyでの快適関数型プログラミングライフを追求するあまり, 使えるのか使えないのかよくわからないものを作ってしまったという話. Rubyに不慣れな人や関数型プログラミングに不慣れな人に対して酷なのはまだわかるとしても, C++(というかboostでの関数型プログラミング)に不慣れな人も全力で置いてきぼりにする誰得記事になってしまった...... 経緯 そもそもRubyはだいぶLispっぽくて, ブロックとイテレータを使うだけで関数型プログラミングになってしまう. たとえばこんな感じで: %w|1 2 3 4 5|.map{|x| x.to_i} %w|1 2 3 4 5|は'1'から'5'までの文字列からなる配列で, その配列のメソッドArray#map*1に対して, 受け取った引数を整数化するブロックを渡してやると, 1から5までの整数からなる配列が得られる. たとえば関数型プログラミ
Asai Laboratory, Ochanomizu University
継続計算に対する仮想機械の導出 定理証明系Coqを使った各種継続計算の性質の証明 対称 λ 計算 shift/resetを含む部分評価器の実装 MinCamlコンパイラ，Caml Lightにおけるshift/resetの実装 証明木(ほか)の可視化 お茶大情報科学科の時間割自動作成 『四則演算インタプリタを作ろう！』 四則演算インタープリタをつくりましょう 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style) lexer（字句解析器）と parser（構文解析器）の作成 (サンプルコード) 局所変数の導入 関数(closure)の追加 大域脱出(exit)の追加 再帰関数の追加 FelleisenのCオペレータ リストの追加 Promptの導入 control/prompt から shift/reset への拡張 対称 λ 計算 Coq
drop して take すればリストに窓が開く
激しく時代遅れな話題ですが…… [1,2,3,4,5] が与えられたとき [[1,2][2,3][3,4][4,5]] を返すような関数を定義せよ http://valvallow.blogspot.com/2011/02/12345-12233445.html これは、窓をガラガラっと動かしながらリストを覗く、という問題です。ようするに、こういう話（n = 3 の場合）。 1 2 3 4 5 6 7 8 9 1 2 3 4 5 6 7 8 9 1 2 3 4 5 6 7 8 9 1 2 3 4 5 6 7 8 9リストに窓を作るには、drop して take するのが簡単です。窓をガラガラっと動かすほうは、この問題の場合にはリストを作ることになっているので、unfold 系の高階関数を使えばよいでしょう。Scheme よりすっきり書けるので Haskell で書きます。import Da
関数プログラミング入門
Proof Summit 2015 <http: /> で発表した、SAT/SMTソルバの仕組みです。 Proofということで、論理学的側面からの面白さを出来るだけ紹介しています。
トップ
第3楽章にはオーソドックスにスケルツォが配置されている。 この楽章は、単純な音型が基礎になっているものの、あまり展開はされない。最初はオクターブで進む単純な音型。 ここから左手に移る。 曲全体は、複合三部形式となっていて、短調のトリオが続く。 D.C.で最初に戻り、最初のテーマが繰り返されて終わる。 楽譜引用はヘンレ版から。 Apple Musicの方はこちら。 卯之吉が無くなった。 猫の老化は後ろ足から始まる。ジャンプできなくなり、そのうち前足もおぼつかなくなり、歩くこともままなくなる。 先週の木曜日あたりから容態が急に悪くなり、うなされ始めた。人のベッドの上にペットシーツを敷き、添い寝をした。 筋力が衰えた中、それでもしきりに這って擦り寄ってきて頭を押し付けてくる。呼吸が荒く苦しそうだ。うなされる声が「苦しいよ、辛いよ」と言っているかのようだ。自分には名前を呼び、頭をなでてやることしか
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Differences between pattern matching and unification?
型推論と型デバッグの現在
https://dl.acm.org/citation.cfm?doid=1292535.1292541