[haskell][quiz] (forall x. ((x->r)->r)->x) -> Either a (a->r) - ヒビルテ (2006-04-29)

λ. javascriptでRDFをパース やっぱし、やっている人はいるもんだな。 何かに使えそうな気がするのでメモ。 Simple javascript RDF Parser and query thingy Javascript-RDF Testbed λ. (forall x. ((x->r)->r)->x) -> Either a (a->r) 今日ちょっと混乱したことを元にクイズにしてみた。多分その手の人にはピンとくる問題。表記はHaskellのものを使ったが、実際には多相ラムダ計算の問題と考えていい。 問題 「(forall x. ((x->r)->r)->x) -> Either a (a->r)」という型を持つ関数を定義せよ。(ただし⊥が途中で現れたりする定義は禁止) この関数は何を表しているのだろうか? 解答編 問題の関数はこんな感じで定義できる。 notNotEM ::

[jrf]

(はてなでは msakai氏)

[motemen]

二重否定除去則から排中律