Deep Learning Acceleration勉強会 で発表してきました

Deep Learning Acceleration勉強会 - connpass にてスライドはこちら Using Raspberry Pi GPU for DNN from notogawa www.slideshare.net普段は出ても関数型言語やら形式手法やらの勉強会とかなため,アウェー感にややソワソワしていた.なんかこの発表で低…

ICFP Programming Contest が本当に縛っていたもの

以前,ここ数年のICFP Programming Contestについて思っていることについてのツイート(群の一部)が, Rustが最強のプログラミング言語である証明 — hayato.io で取り上げらたため, @chokudai さんに届いて反応してくれたようでうれしい.一連の氏のツイート…

TensorFlowで訓練したパラメータをChainerのモデルにrestoreする

何がどうなってか深層学習〜的なものに触れる機会が増えたので,何かそれっぽい話を「他のフレームワークに比べてなんだか学習済み(pre-trained)モデルが公開されてないような?」Chainerを使ってみた深層学習マンはきっとこのお気持ちになったことがあるん…

コンテキストの順番を入れ換えると互換性が崩れることがある

(注:この記事はかなり前に書いて公開し忘れていたことに今日気付いたものです.もう当たり前になってるかもしれないけどもったいないので一応)ghc8以降TypeApplications拡張が入ったこともあり一応の注意喚起.たとえば,次のように関数fとgを定義する.時系…

問題を解決するつもりでキッチリ型を付けた先にある高い壁

null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)— Noriyuki OHKAWA (@notogawa) 2016年11月18日 過ぎたるは…

実世界を扱う依存型プログラミングのたぶん基本~外界から安全な世界までの道

依存型ならさらに安全にプログラミングできちまうんだ!と言ったところで,「無料で遊べちまうんだ!」とか「3000円払えば無料で10連まわせる」みたいな感があり, 依存型使わない場合とどう違ってくるのか 入出力から扱い始めるとどういった形のプログラム…

stackを通してのコンパイルにとても時間がかかる条件

ghc 7.10 からみられるようになった現象で,放置しているうちにやや旬を過ぎてしまっている感もある話題なのだが,その後特に改善してるわけでもないのと最近踏まれたのを見たので念のために記しておこうかなと.コンパイル時間ghc-7.8で1分40秒なやつがghc-…

関数プログラミング実践入門が増補改訂です

関数プログラミング実践入門という本を書きました - ぼくのぬまち 出張版 に引き続き,よろしくおねがいします.[増補改訂]関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)作者: 大川徳之出版社/メーカー: 技術評論社発…

Hackageメタデータの依存関係だけ更新してどうするの?

(追記) cabal update で反映される模様?Agda-2.4.2.5のDependenciesで,unordered-containersを見て欲しい.依存関係が >=0.2.5.0 && メタデータのみをパッケージアップロード後に編集したもので,実際2016/1/25現在見えているメタデータはrev 1となってい…

stackで行く地獄巡りの旅

Haskell使い 十戒 一、常に型と共にあれ 一、不要な式より潰すなかれ 一、無益にIOするなかれ 一、つけられたらつけかえせ 一、つけられる前につけろ 一、一日一善 一、遅延を疑ってみよ 一、気を付けよ甘い型付けと暗い道 一、小さなコードで大きな仕事 一…

Travis CI等でstackのresolverにstackage latest nightlyを使う

stackでstackage nightlyのresolverを使おうとしても,stack.yamlには resolver: nightly-2015-10-27のように日付まで用意しないと使えない.lts-2やlts-3についても同様で,lts-3.*まで指定する必要がある.Travis CI等で各resolverについてマトリクステス…

Jinja2サブセット的な型付きテンプレートエンジンhaiji

年末年始なので何か作ろうかなと思いhaiji*1というライブラリを作ってみてる. まぁ,なんというか最近ansible*2よく使ってたこともあってイロイロ思うトコロあったりなかったり.大概のテンプレートエンジンにおいて,個人的にイマイチ気に入らないトコロは…

ロジックパズルの解説

この記事は Haskell Advent Calendar 2014 6日目の記事です.関数プログラミング実践入門 第6章 最終節にあるロジックパズルは,一体なにをどうやるとこのインターフェース設計になるのかという話.元々内容的に入門っぽくならないものないんだけど,特徴的…

ブラウザ上でAgdaを試せるサイトを作ってみた

この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です.Agdaがコンパイルできないんだがとか,agda-modeってEmacsだけなんでしょ?とか,そういった話をちょくちょく耳にするし,ProofSummit2014で明日の記事担当のamutakeくんがブラウザからC…

「美しい,だから正しい」より「正しくて,あわよくば美しい」がよい

関数プログラミング実践入門.発売されました.電子版もあります. 今回は本書の副題に関する話題.本書の副題には「正しい」を使っている.実際に価値を提供するのは「正しい」コードなのだが,プログラミング関連文書でよく目にするコードに対する修飾は「…

関数プログラミング実践入門という本を書きました

是非手に取ってみて下さい.よろしくおねがいします.関数プログラミング実践入門 ──簡潔で、正しいコードを書くために (WEB+DB PRESS plus)作者: 大川徳之出版社/メーカー: 技術評論社発売日: 2014/11/14メディア: 単行本(ソフトカバー)この商品を含むブ…

Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能

EmptyCaseが入ってきた.absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ.具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く.まず,矛盾(bottom)の扱いについて.矛盾は「値を構成できない型」になればよいので,…

copatterns概要

ghc-7.8でビルドできるAgdaマダカナーとか思いつつ,Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら,実験的機能としてcopatternsってやつが入ると書かれている.余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつ…

ghc-mod-4 でfaceを反映させる

ghc-mod-4以降ではghc-modiを使うためにflymakeへの依存を切っており,flymake的な挙動は自前で実現している.そのため,今まで反映されていたflymake用のface設定が反映されなくなるので,バージョンアップ後急にさびしい絵面になったりする.もし, (set-f…

IOアクションひとつひとつを利用許諾し・テスト可能にする

IOのテストってたいへんだ.これをどうにかするために,先人たちは色々考え, 利用対象の特定IOアクションを慎重に取捨選択し,MonadHogeIOのような型クラスによりインターフェースを与えてからそのインターフェース上のアクションとして実装する.実行時は…

CPS変換もいいけど融合変換もね

継続渡しなHaskellライフ - モナドとわたしとコモナド の流れで. 要約すると,元々 fb :: Int -> Either Int String fb n = case n `gcd` 15 of 15 -> Right "FizzBuzz" 5 -> Right "Buzz" 3 -> Right "Fizz" _ -> Left n fizzbuzz1 :: Int -> String fizzb…

「依存関係のある値のうちの一部をrewriteしようとしたときの問題」をAgdaで書くとどうなるか

依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか. こういうことだろうか? module AC-2013-5 where open import Data.Nat import Relation.Binary.PropositionalEquality …

パッケージを跨いだ再exportの危険性

この記事は Haskell Advent Calendar 2013 1日目後半の記事です.前半の記事もよろしく. 「ある露出モジュールAで隠蔽モジュールA.Xをimportし,AでA.Xのシンボルを選択的に(あるいはモジュールごと全部のシンボルを)露出させることで,AとA.Xを含むパッケ…

砂場遊びは地獄のかほり

この記事は Haskell Advent Calendar 2013 1日目前半の記事です.後半の記事もよろしく. cabal sandboxは便利だけどdep hellが無くなったわけではない.ほとんどにわかに見えなくなっただけだ.むしろsandboxに甘えて針穴通すようなbuild-dependsを書いてし…

CoqのtacticやコマンドとAgda上操作の対応

この記事は Theorem Prover Advent Calendar 2013 1日目の記事です. 注意事項がひとつあります.本記事にはAgdaコードを含めようとしていますが,記事内でちゃんと書けてない文字があるかもしれません.だが私は悪くねぇ! ハヽ/::::ヽ.ヘ===ァ {::{/≧===≦V…

cabal sandbox環境のpackage DBを参照する(改)

前回の記事は調査不十分だった.まず,sandbox環境では, cabal install --only-dependencies --enable-tests cabal configure --enable-tests cabal build cabal test を実行したときと, cabal install --enable-tests を実行したときで,config dist pref…

cabal sandbox環境のpackage DBを参照する

cabal-install-1.18 がきた.全国のHaskeller待望のcabal sandboxが使える.cabal-devさん今までありがとう.さようなら. この記事は余計なことをしている可能性があります! さて,テスト時にプログラムをビルドする必要があるとする.これは*.cabalファイ…

ICFP Programming Contest 2013

今年ものとがわさんパンピーやった(1年ぶりn度目) 問題はここ.64bit非負整数に対する限られた関数と単純なlambda式からなるプログラムがコンテストサーバ側にいっぱいあってIDが付いている.サーバ側にある各プログラムの具体的な形はわからない.プログラ…

anarchy proofのAgda版作った

全国一億三千万のAgdarの皆様に送る Agda Challenge最近chaton haskellがchaton agdaと化していたりすることもあり,anarchy proofがうらやましくてAgda版が欲しい人いっぱいいるのではないかと思って作ってみた.開発中にステージング環境を作り近くの数人…

Agdaとフォントと微妙な設定

Agda書くとみんなフォントに困る…と,思う.Agda標準ライブラリの時点で_⊔_とか_⊎_とか⟨_⟩とか普通のランゲッジでは使わないような文字入りの演算が目白押しだ.当然下手なフォント設定すると正しく表示されない.プログラミングに適したmonospaceのフォント…