6さいカンファレンス 第2回「数学の定理を自動で発見するAI を Haskellで作ろう！」まとめ
2012/09/13にくいなちゃんさん主催で開催された6さいカンファレンスのまとめ。 第2回は「数学の定理を自動で発見するAI を Haskellで作ろう！」です。 勝手にまとめてしまったので、何か問題があれば@shogo82148まで。 WELCOME TO HELL!! くいなちゃん: それでは、まず、数学の「定理」とは何か、について説明したいと思います。 みなさん、日常的に「定理」という言葉を使っていると思いますが、「定理」とは何か、説明できますか くいなちゃん: 「教科書に載っている公式が、定理だ！」と思うかもしれませんね。 確かに、教科書にも定理は載っています。 くいなちゃん: では、曖昧な理解の方のために、厳密かつ ゆるふわに説明しましょう。 くいなちゃん: 定理とは、次のように定義できます。 公理であるならば、定理である。 定理を推論規則によって推論したものは、定理である。
Windows8.1 Sublimetext3 で Haskellの環境構築 - momolog
前書き 前の記事では、emacsでHaskellのコードにシンタックスハイライトをつけようとして、うまくいかないという話をしていました。 そんなときにこんなリプライをいただきました。 Sublime text。なんでしょうそれは。 ぐぐってみたところ、最近話題沸騰中の素敵なエディタであるらしい。 Haskellのシンタックスハイライトつける機能あるの？と聞きましたら、 ということらしい。ふむ。 emacsに拘る理由もないし、いろんなエディタ試してみるのもよいかなと思いまして、SublimeText上でのHaskellプログラミング環境を作ってみることにしました。 本文 Windows8.1 Sublimetext3 で Haskellの環境構築をする手順です。 1.Sublimetext 3のインストールと初期設定 1-1.Sublimetext 3のインストール 公式ページ(http:/
第7章 型や型クラスを自分で作ろう 前編 - Rejasupoem
すごいHaskell楽しく学ぼう輪読会とは 経緯 2012年にSICP読書会に参加していてとてもためになったという話をしたのがきっかけで、社内でコンピュータサイエンスの勉強会をやろうということになりました。 そこで、2013年夏に社内でどの本を教科書にするかアンケートをおこないました。 教科書の候補に上がった本 計算機プログラムの構造と解釈(SICP) 言語：Scheme Web上での問題の解答の多さ(すくなくとも日本語での)は、他を圧倒してる。 関数プログラミング入門(IFPH) 言語：Haskell SICPよりちょっと難しい。一番最初にやる本ではない感じ(ってえらい人が言ってました)。 プログラミングの基礎 言語：Ocaml 著者による解答例あり。いまSICPを読むのは時間の無駄 - きしだのはてな プログラミング言語の基礎概念 言語：Ocaml 「プログラミング言語の基礎概念」とい
Haskellの多相性 - あどけない話
パラメータ多相(parametric) 型のパラメータ化。静的。 length :: [a] -> Int length [] = 0 length (x:xs) = 1 + length xs C++のテンプレート Javaのジェネリックス アドホック多相(ad-hoc) 型によって、異なる振る舞いを示す。静的。 class Shape a where display :: a -> String data Triangle = Triangle deriving Show instance Shape Triangle where display _ = " * \n" ++ " * * \n" ++ "*****\n" data Rectangle = Rectangle deriving Show instance Shape Rectangle where display _ =
Typeable and Data in Haskell
Data.Typeable and Data.Data are rather mysterious. Starting out as a Haskell newbie you see them once in a while and wonder what use they are. Their Haddock pages are pretty opaque and scary in places. Here’s a quick rundown I thought I’d write to get people up to speed nice and quick so that they can start using it.1 It’s really rather beautiful as a way to do generic programming in Haskell. The
hint 使って型推論、 haskell-src-exts を使って Parse - keigoiの日記
GHC API のラッパー hint を使えばHaskellでも手軽にリフレクションっぽいことができる。例えば動的にHaskellのソースをロードして関数を呼び出す、といったことが数行で書ける。 ところでリフレクション周りで色々やろうとすると、すぐに関数の型を解析したくなるのだけど、hint は 型推論の結果を文字列で返すのでHaskell的には使いにくい。情けない話だが、どうやら GHC APIがそうなっているので仕方ないようだ。Haskellのパーサが必要になる。 haskell-src-exts を使えば、Haskellの型をparse できる。 似たようなことをやる方法に template haskellとか haskell-src という標準のアレがあるけれど、いくつかの拡張構文をサポートしていない。その点 haskell-src-exts はほぼすべての GHC拡張をサポートし
GHC の STG に関するまとめ - あどけない話
理解が深まれば、適宜更新します。 G-machine グラフ簡約のためのスタックマシン 関数適用が連なる spine (背骨)を持ち、愚直にカリー化を実現する 簡約のたびに、それぞれの項を更新 ローカル関数はラムダリフティングしてグローバル関数に直す必要がある ラムダリフティングされた関数はスーパーコンビネータと呼ばれる Gコード push/enter 方式 Spineless G-machine Spineless: 引数が充足している関数は、一気に呼び出す このころまでに標準の G-machine も spineless だったらしい サンクは共有されているときだけ更新 (これが重要) G コードに対して 5 つの新しいコードを追加 push/enter 方式 Spineless Tagless G-machine Tagless: 統一された書式になって、先頭の tag がなくなった
foldlを直す - 純粋関数空間
http://www.well-typed.com/blog/90/ foldlに関するこの記事（英文）が面白かったので、勝手翻訳しました。 foldlなんとかなるといいですね。 foldlを直す foldl 関数は壊れている。壊れているとみんなが知っている。 四半世紀近く壊れたままだ。ついにこれを修正する時が来た！ 今日、私はPrelude.foldlをData.List.foldl'として知られる実装で再定義することを提案する。 foldlは壊れている！ 既にご存知だとは思うが、念のため… Haskellerが必ずfoldlではなく、foldrやfoldl'を使うように勧めてくることにお気づきだろうか？ 例えばReal World Haskellでは次のように言っている。 `foldl`のサンクの挙動のため、実アプリではこの関数を使わないようにするのが望ましい。 特に問題がない場合でも
Haskellのコンパイル中に現れるSTGと, GDBで見るC-backendなC-- - suztomoのはてなダイアリー
Haskellのプログラムの実行がGlasgow Haskell Compilerによるコンパイル後にどういう命令によって表現されているかに興味があったので調べてみました. 例えば関数がどのようにメモリ上に存在するかといった実装や, 数字がどうやって表現されているかをgdbを用いて調べてみます. この記事はpartake.inの12月24日分のものです。 Haskellのコンパイル順序 I know kung fu: learning STG by exampleによるとHaskellはGHCの中で次のような流れでコンパイルを進めます. Parse tree Core (Syntax sugarがなくなります) STG (Spineless Tagless G-machine language) C-- backend 下の中から一つ選ばれます LLVM IR (LLVM) Native
Ministg - HaskellWiki
Ministg is an interpreter for a high-level, small-step, operational semantics for the STG machine. The STG machine is the abstract machine at the core of GHC. The operational semantics used in Ministg is taken from the paper Making a fast curry: push/enter vs. eval/apply for higher-order languages by Simon Marlow and Simon Peyton Jones (hereafter referred to as the "fast curry" paper). Please cons
簡約!? λカ娘 Rock!の紹介とHaskell製Androidアプリの解説 - Metasepi
Table of contents Haskellで書いたAndroid NDKアプリってどんな感じ？ CubeVertices.hsファイルについて glVertexPointerとglColorPointerの呼び出し AndroidEngine型の状態変更 全てをつなげる簡易フレームワーク この記事は Android Advent Calendar 2013 - Qiita [キータ] の12/17(火曜)分じゃなイカ。 だいぶ息切れしてきた関数型プログラミングの本 簡約!? λカ娘 Rock! がコミックマーケット85 3日目 西地区 す-03a で出るでゲソ。みんな買ってほしいでゲソ! 第1章 λカ娘探索2? 第2章 僕のカノジョはスナッチャー # <= コレ書いた がもくじで、 @master_q は第2章を書いたらしいでゲソ。 この記事では Android NDK に付属して
Haskellのforallについて理解したことを書いておく(ランクN多相限定)。 - uehaj's blog
Haskellのforallについて理解したことを書いておくyo!(ランクN多相限定*1 )。 前提知識のおさらい: 型・多相型・型検査・型推論… 最初に基本概念を整理しておきます。 IntやInt->Intは単相型、aやa->aは多相型である。ここでaを型変数と呼ぶ。型変数を含む型が多相型ってわけです。 言語処理系の実装上、型という概念は型変数や型コンストラクタのツリー構造として表現される。Int,Char,[],->,(,),(,,,),IO aなどが型コンストラクタ。 a,bが型変数。組合せて(a->[Int])->[b]->(a,b)とか。::の右に書くやつです。 型は、プログラムの字面上に直接的実体がある関数や変数だけではなく、値を生じさせる部分式すべてに付随し、コンパイル時に決定されるべき情報である(値あるところに型がある。*2 )。それを決定しようというのが(静的)型検査であ
こわくない Idris (1) - Ryusei’s Notes (a.k.a. M59のブログ)
はじめに Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使えるものなんだぞって主張があるように思う。 そんなIdrisなんだけど、日本語による文献はとても少ない。今のところ、Idrisをやろうって人はまず英語のチュートリアル読まなきゃいけない。僕はIdris初心者でまだIdrisらしいプログラミングがどんなものか分からないのだけれども、日本語による学習ノートを残しておこうと思う。もしかしたらデタラメ書いてるかもしれないので、はてブかTwitter @mandel59で教えて下さい。 Idris Idris チュートリアル (英文) Programming in Id
Introduction to Fay - 純粋関数空間
Fay をいじってみたので、 せっかくだから記事を書いておこうと思います。 なお、Fayは新しい言語（というより、処理系と言った方が適切かな）ですので、 ここに書いてある情報は、来年か、あるいは半年後か、 それとももっとずっと早くに陳腐化する可能性がそれなりに低くないことを、 あらかじめお断りしておきます。 この記事執筆時に用いたFayのバージョンは、 fay-0.14.5.0 です。 デモ・前置き 特に何か作りたいものが有ったわけではなかったので、 今回作ってみたものは超どうでも良いツールです。 http://tanakh.jp/tools/sudden.html ＿人人人人人人＿ ＞ 突然の死 ＜ ￣Y^Y^Y^Y^Y￣ こういうテキストを生成するだけのツールです。 Fayのコード HTMLコード これらのコンパイルなどもhakyllでまとめて管理できるようにしました。 hakyllに
Haskellの演算子について纏めてみた - 開発やプログラミングや家族や思考
人が作ったHaskellのコードを読んでいると、記号の意味がわからなくて困ることが多々あったので纏めてみた。hrefでもGoogleでも検索できないしさ… Haskellの演算子で使える記号 !#$%&*+./<=>?@\^|-~ 及びUnicodeに含まれる記号(一覧が欲しい…けど√とか→とかもきっとそうだよね。) ただし「(),;[]`{}_:"'」は除く さらに、「:」で始まるのはデータコンストラクタで予約されているので演算子では使えない。 また、以下の記号列は予約されている 演算子 意味 .. リストの範囲指定。 : リストのcons。 :: 型指定 = 関数束縛。 \ ラムダ(無名関数)。 | パターンマッチのガード条件。data型enum定義。リスト内包表現。 <- リスト内包表現のジェネレータ。do記法での値束縛。 -> 関数の型定義。ラムダ(無名関数)定義。case式。 @
Haskellには副作用がないのか？ - あどけない話
ある人は、Haskell には副作用がないと言う。また、別のある人は Haskell には副作用があると言う。Haskell を学ぶ者にとって、こういった意見の食い違いが、Haskell を得体の知れない言語にし、学習の障壁となっているかもしれない。そこで、この記事では、なぜこのような意見の相違が生まれるのかについて説明したいと思う。 向心力か遠心力か？ 僕は高校三年になって受験勉強をするまで、物理の運動方程式が得体の知れないものに思えていた。 例として円運動を考えよう。ある説明では、円運動をしている物体には向心力が働いていると説明されている。また別の説明では、遠心力が働くと説明されている。一体、どういうことだろう？ 受験勉強でたくさんの問題を解いて、ようやく分かった。これらの説明はどちらも正しい。すなわち、観測者がどこにいるかによって、説明の仕方が異なるのだと。 観測者が円運動をする物体
C++ で Maybe モナド - 野良C++erの雑記帳
動機： C++ で Haskell の Either っぽい何かを作ってみた。 - 野良C++erの雑記帳 せっかく Either 作ったんだから Maybe モナドも作ろうぜ、という話。 まず Boost には、既に Maybe に相当する Boost.Optional が存在するので、 そいつをモナドの >>= に対応させてやればよい、 という考え方が最もストレートなものであり、 実際、そういう方針で書かれたコードは既に存在してたりします。 （例： C++でMaybeモナド - Faith and Brave - C++で遊ぼう） そこで、少し発想を変えてみることにしました。 まず、 Haskell のモナドを、そのまま C++ に持ち込むのは、やはりキモいです。 C++ には暗黙の型変換という文化があるので、その恩恵をフルに活用出来ないか。 また、 C++ における Maybe 相当
はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
自然言語をラムダ式で解釈する体系PTQのHaskell実装
GitHub - fumieval/Monaris: A simple tetris clone
