型理論 なんて自分には関係ないと思っているあなたへ
24. ...... Lemma reduce_lemma : forall ctx (ctx' : seq (term * typ)) t ty, typing ([seq Some p.2 | p <- ctx'] ++ ctx) t ty -> Forall (fun p => reducible ctx p.1 p.2) ctx' -> reducible ctx (substitute_seq 0 [seq p.1 | p <- ctx'] t) ty. Proof. move => ctx ctx' t ty; elim: t ty ctx ctx'. - move => /= n ty ctx ctx'. rewrite /substitute_seqv typvar_seqindex subn0 size_map shiftzero. elim: ctx' n => [|
ラムダ計算の勉強のしかた、プログラム意味論 - きしだのHatena
先日のエントリで手続きを記述するという側面と、式を記述するという2つの側面があるということを書きました。 プログラムの理論とはなにか そして、手続きの性質として代表的な、アルゴリズムについての勉強のしかたについてまとめてみました。 アルゴリズムの勉強のしかた そこで、今回は、式を記述するという側面の勉強のしかたと、あとこの分野は自分でもまだ全然勉強してなかったので、これからどういう本を読もうと思っているかをまとめてみます。 プログラム意味論 プログラムは必ずプログラム言語、少なくとも記号で記述します。*1 そこで、プログラムの勉強という点では、どのように動くかというアルゴリズムの勉強だけではなく、どのように書けるか、書いたものにどのような性質があるのかということも知る必要があります。 例えば、2005年あたりからRubyのような動的型付け言語が流行りだし、Javaなどの静的型付けの言語との
モナドはメタファーではない · eed3si9n
2011-05-28 Scala界の関数型プログラミング一派を代表する論客の一人、@djspiewak が 2010年に書いた “Monads Are Not Metaphors” を翻訳しました。翻訳の公開は本人より許諾済みです。翻訳の間違い等があれば遠慮なくご指摘ください。 2010年12月27日 Daniel Spiewak 著 2011年5月29日 e.e d3si9n 訳 僕は今、約束を破るところだ。およそ三年前、僕は絶対にモナドの記事だけは書かないと自分に約束した。既にモナドに関する記事は有り余っている。記事の数が多すぎてその多さだけで多くの人は混乱している。しかも全員がモナドに対して異なる扱い方をしているため、モナドの概念を初めて学ぼうとする者は、ブリトー、宇宙服、象、砂漠のベドウィン (訳注: アラブ系遊牧民) の共通項を探す努力をするハメになっている。 僕は、この混乱した
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 を用いて説明します。 関数の型 関数の型は、-> を使って書きます。例えば、Int を Char に変換する chr という関数の型は、以下のようになります。 chr :: Int -> Char 一引数の関数の型は、まぁこんなもんだと思えるでしょう。びっくりするのは、引数が増えたときです。たとえば、replicate という関数の型を見てみましょう。 replicate :: Int -> a -> [a] replicate は、第二引数で指定されたデータを第ー引数に指定された個数分用意して、リストにして返す関数です。([] は配列ではなく、リストです。) 次のように動きます。 > replicate 3 "foo" → ["foo","foo","foo"] a は型変数といって、任意の型を取れます。なじめない人は、具体的な型を当てはめてみ
AS3で関数のカリー化 – Rest Term
前回のエントリ、AS3でFunction.bind()に引き続き “関数 (function)” を扱ってみます。 今回は関数のカリー化 (currying)についてです。 とその前に、前回のエントリで示した Function.bind() について。 あれは昨今のAS3文化には馴染まないアプローチだったと思います。 特にAS3からFlashの世界に入った方は prototype に拒否反応があったりするかもしれません。 ということでよりAS3文化に馴染んだアプローチを探してみます。 たぶんきっと「関数を借りる」といったこともしないと思うので、 引数束縛だけを使うシチュエーションを考えます。 (もし、関数拝借を普通によくやってるFlasherの方がいたらごめんなさい。。) * 引数束縛して部分適用: Partial Application (ES5の Function#bind とは別モノ
デブサミ 2011 で F# について話してきました！ - ぐるぐる～
発表資料は slideshare にあげました。暇ができたらもうちょっと補足とか書きたいですね (書かないフラグ)。 ページ数は 273 ページと、ありえない枚数ですけど、内容としては 90 ページもないはず！ C#(VB)プログラマのためのF#入門View more presentations from bleis tift. 発表終了時間を 10 分勘違いしていて、かなり早めに終わってしまった・・・ 発表時の Twitter の様子は デブサミ2011【17-D-7】C#(VB)プログラマのためのF#入門 bleis-tift 氏 - Togetter をどうぞ。 ・・・なんかおかしいのも混ざってますけど気にしない方向で！
Functional Java
Functional Java is an open source library facilitating functional programming in Java. The library implements numerous basic and advanced programming abstractions that assist composition oriented development. Functional Java also serves as a platform for learning functional programming concepts by introducing these concepts using a familiar language. The library is intended for use in production a
関数型的正規表現マッチ - Preferred Networks Research & Development
最近ローソンでお菓子をたくさん買った田中です。 近頃読んで面白かった論文を紹介したいと思います。 A Play on Regular Expression 今年のICFPでFunctional Pearlとして発表されたものです。ICFP（International Conference on Functional Programming）というのは、関数プログラミングに関する国際学会で、Functional Pearlというのは、エレガントでためになる、関数プログラミングのテクニック集です。 この論文ではまず、正規表現マッチャを関数型言語(Haskell)でいかにエレガントに記述できるかが示されます。それから、エレガントさを保ったままの線形時間実装へ改良し、その実装がC++によるプロフェッショナルな実装(具体的にはGoogle re2)に匹敵するパフォーマンスを示すことが示されます。さら
inforno :: Scalaで無限リスト：Haskellライクに
ScalaにはStreamという無限リストがあるんだけど、微妙に使いづらい、というか分かりづらい。Haskellでいうcycleはどうだ、とかよく忘れるのでメモ。 1def repeat[T](a:T) = Stream.const(a) 2def cycle[T](a:Iterable[T]) = Stream.const(a).flatMap(v=>v) 3def iterate[T](f:T => T, x:T):Stream[T] = Stream.cons(x, iterate(f, f(x))) 4def replicate[T](n:int, elem:T) = Stream.make(n, elem) こんな感じかな。cycleは結構使うから、Streamに標準でありそうな気がするんだけど、ないような。というわけで上のような定義となる。 1repeat(1) take 10
visible true : Scalaで無限リストを使ってフィボナッチ数列
2010年10月22日00:53 カテゴリScala Scalaで無限リストを使ってフィボナッチ数列 元ネタ:基礎を終えた人のScalaミニtipslazy val fib: Stream[Int] = Stream.cons(0, Stream.cons(1, fib.zip(fib.tail).map(p => p._1 + p._2)))これ、Scalaで無限リストと遅延評価でフィボナッチ数列を実現してるんですが、 もう、何やってるかぜんっぜんわからなかったので、がんばってみました。 登場人物lazy valStreamStream.consStream.zipStream.tailStream.map_1, _2という表現Stream.takeこれ、これらが判ればきっと解る！ 1.lazy val 遅延評価! valとかにlazyとか付けると遅延評価になります！ 遅延評価ってなんだ
Rinkou - Types and Programming Languages
輪講スケジュール 読む本 B. Pierce: Types and Programming Languages お知らせ Bounded polymorphism 以降は秋口から行います。 参加者 大根田 末永 立沢 洪 小林 アフェルト 清木 前田 遠藤 川崎 川中 スケジュール
VBラムダ式 基礎文法最速マスター - ＠IT
■0. まえがき 本稿では、小さいテーマではあるが、まだまだ慣れ親しんでいない開発者が少なくないと考えられる「ラムダ式（VB：Visual Basic）」についての基礎文法を簡潔にまとめる（C#ラムダ式についてはこちら）。「ラムダ式、どう書くんだっけ？」という場合のリファレンスとして活用していただけるとうれしい。また、ラムダ式を敬遠しているという方は、まず本稿が学び始める取っ掛かりになるかもしれない（もちろん本稿の説明は充実しておらず、すべてを学べるわけではない）。 今年（2010年）に入ってインターネット上では、プログラミング言語の基本文法を簡潔にまとめた「○○言語 基礎文法最速マスター」（以降、最速マスター・シリーズ）というブログ記事が多数投稿されている。参考までに、そのいくつかを示そう（そのほかについては、こちらを参照されたい）。 VBA 基礎文法最速マスター：何かしらの言語による記
ArrowによるHaskellプログラミングの基礎。…パイプ感覚で順次/分岐/繰返し - よくわかりません
Programming with Arrowsを読んで理解したつもりのメモ。誤りなど乞うご指摘。 （復習）Arrowってなに？ と思って以前調べたメモが"3分で解るHaskellのArrowの基本メモ - よくわかりません"。それにちょっと補足というか観点を変えてまず感覚の整理。 Monadに色んな種類があるように、Arrowも色んな種類がある。 Monad: IO、Maybe、… Arrow: 関数そのまんま(->)、Kleisli m、… ある種類のMonadに色んな型の色んな値を入れられるように、ある種類のArrowに色んな型の色んな関数を入れられる。 Monad: Maybeの例→ 「Maybe Int」 にreturn 0もreturn 777もＯＫ。「Maybe Char」 にreturn 'a'もreturn ' 'もＯＫ。 Arrow: (->)の例→ 「Int -> In
第14回 型＝命題，プログラム＝証明
MLの型と型推論 この連載でも何回か触れたが，MLやHaskellなど多くの静的型付き関数型言語には，「型推論」という機能がある。これは，プログラム中の変数や関数の型を省略しても，「もっとも一般的」な型を言語処理系が勝手に推論してくれる，という機能だ。 例えば，次のように，二つの引数xとyを受け取って，(x, y)という組を返す関数pairを定義してみよう。 > ocaml Objective Caml version 3.10.0 # let pair = fun x y -> (x, y) ;; val pair : 'a -> 'b -> 'a * 'b = <fun> # このように，pairは「何らかの型'aを持つ値と，何らかの型'bを持つ値を受け取り，'a型の値と'b型の値の組を返す」と推論される。一般に，t1 -> t2は，型t1の値を受け取って，型t2の値を返す関数の型であ
Functional Javascript
Functional is a library for functional programming in JavaScript. It defines the standard higher-order functions such as map, reduce (aka foldl), and select (aka filter). It also defines functions such as curry, rcurry, and partial for partial function application; and compose, guard, and until for function-level programming. And all these functions accept strings, such as 'x -> x+1', 'x+1', or '+
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://pllab.is.ocha.ac.jp/~asai/jpapers/sakaue.pdf
転送中
Amazon.co.jp: 関数プログラミングの楽しみ: 山下伸夫 (翻訳), ＪｅｒｅｍｙＧｉｂｂｏｎｓａｎｄＯｅｇｅｄｅＭｏｏｒ (編集): 本
数理科学的バグ撲滅方法論のすすめ---目次 | 日経 xTECH（クロステック）
