問題を解決するつもりでキッチリ型を付けた先にある高い壁 - ぼくのぬまち 出張版
null安全おじさんになりかわりそれがしがお見せつかまつる 機械が理解できる複雑な契約の型表現がもたらすものは つまるところこのようなもの ずぶぶ(切った腹から証明オブジェクトを引き摺り出す)— Noriyuki OHKAWA (@notogawa) 2016年11月18日 過ぎたるは猶及ばざるがごとし． 最近null安全？だかの話のからみで，(静的な)型で契約云々を表現してシアワセになれるんだぜーと言うのをチラホラ見聞きする．たとえば，pythonで統計なり機械学習なりやっててnumpy弄るような人が，ndarray(多次元配列)のshape(多次元配列の形)が合わずエラーで落ちたりとかそういうアレについて云々という．なるほど型があれば実行前に止めることができ，実行時，エラー*1になってファーみたいなことは避けられるだろう． しかし，これが天国へ続く道かどうかはまた別の話．(依存)型で舗
実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道 - ぼくのぬまち 出張版
依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり， 依存型使わない場合とどう違ってくるのか 入出力から扱い始めるとどういった形のプログラムになるのか 大概どういう流れでプログラミングすることになるのか とか，そういった話を通しではそんなに見ないかなーという気がしたので，ごく基本的なものを一通りまとめておこうと思って． まず，説明に使う問題設定について．行列演算，特に行列積を考えてみる．ただし，行列の形(行はいくつ，列はいくつ)についてはプログラムの外から入力によって決定するような状況とする．これ自体は普通の問題設定だと思われる． 依存型を使わなければ特にどうということも無い．恐らく行列の型を次のように定義し， -- 形のみ持っておき，中身の数値については簡単のため省略 data Ma
stackを通してのコンパイルにとても時間がかかる条件 - ぼくのぬまち 出張版
ghc 7.10 からみられるようになった現象で，放置しているうちにやや旬を過ぎてしまっている感もある話題なのだが，その後特に改善してるわけでもないのと最近踏まれたのを見たので念のために記しておこうかなと． コンパイル時間ghc-7.8で1分40秒なやつがghc-7.10で6分かかるようになってて助けてクーガー兄貴— Noriyuki OHKAWA (@notogawa) October 31, 2015 結論から言うと，一定レベル以上の最適化付きで，大きな型レベル計算を含んだ型を持つインターフェースを含む場合…となる．このときコンパイルが遅い．厳密には遅いのはコンパイルではないが． 上記ツイートで問題にしてたJinja2サブセットのテンプレートエンジンであるhaijiは，hackageに上げる前のPoC段階で記事にもした． notogawa.hatenablog.com なのでここでは概
stackで行く地獄巡りの旅 - ぼくのぬまち 出張版
Haskell使い 十戒 一、常に型と共にあれ 一、不要な式より潰すなかれ 一、無益にIOするなかれ 一、つけられたらつけかえせ 一、つけられる前につけろ 一、一日一善 一、遅延を疑ってみよ 一、気を付けよ甘い型付けと暗い道 一、小さなコードで大きな仕事 一、あがめよ讃えよ汝の師匠 ﾁｬﾗﾗﾗﾗｰ ﾁｬﾗﾗﾗﾗｰ ﾁｬﾗﾗｰﾗ ﾗｰﾗ ﾗｰﾗﾗｰ ﾗﾗﾗｰ この記事はHaskell Advent Calendar 2015 - Qiitaの2日目の記事です． 今回は，stackにも使い慣れてきてそろそろhellが恋しくなってきた方々のため，stackに頼りつつもhellを拝むための方法を紹介する．ここでとりあげてるstackは0.1.6.0時点なので，後々なら何か変わってるかも やり方はとても簡単で，システムghcの依存するパッケージバージョンがstackのresolverに含まれるものと
ブラウザ上でAgdaを試せるサイトを作ってみた - ぼくのぬまち 出張版
この記事は Theorem Prover Advent Calendar 2014 の4日目の記事です． Agdaがコンパイルできないんだがとか，agda-modeってEmacsだけなんでしょ？とか，そういった話をちょくちょく耳にするし，ProofSummit2014で明日の記事担当のamutakeくんがブラウザからCoq使えるやつを発表してたりしたので，Try Agda というサイトを作ってみた． リポジトリはここ https://github.com/notogawa/agda-interactive-server バックエンドはHaskellでwai+warp+websocketでAgdaのライブラリからAgdaを直に利用．フロントはjquery+ACE editor．画面レイアウトはもちろんbiim兄貴リスペクトだ． サーバ強くないし，あんまりデカい証明に使ったりするとガバガバなリ
「美しい，だから正しい」より「正しくて，あわよくば美しい」がよい - ぼくのぬまち 出張版
関数プログラミング実践入門．発売されました．電子版もあります． 今回は本書の副題に関する話題．本書の副題には「正しい」を使っている．実際に価値を提供するのは「正しい」コードなのだが，プログラミング関連文書でよく目にするコードに対する修飾は「美しい」なのだ．これは何故だろう． といっても，大抵の人は経験などから「美しい*1」コードならば読み易く間違えにくいということを知っている．なので，この点についてそう深く考える必要は無いようにも思われる．「美しい」コードは善である． しかし，「正しさ」についてあまりにも「美しさ」に頼るようでは危険だ．「美しいから正しい」ことがわかる状態はつまり「ヒトが目を凝らすから正しい」ことがわかる状態ということに他ならない．ヒトは間違える．目も頭も疲れる． 通常，「美しい」コードに保つのは存外コストを要する作業である．お仕事であればザックリと事業戦略の正しさがまず前
Haskell定理証明士がEmptyCase拡張によって受ける恩恵と効能 - ぼくのぬまち 出張版
EmptyCaseが入ってきた．absurd pattern matchingがHaskellで使えるのでHaskell証明士には朗報だ． 具体的にEmptyCaseの有無で世界がどう変わるかを把握してる範囲で書く． まず，矛盾(bottom)の扱いについて．矛盾は「値を構成できない型」になればよいので，通常次のいずれかになる． data Bottom data Bottom = Bottom Bottom 直観主義における「矛盾からは何でも導ける(bottom elimination)」は，型としては， bottomElimination :: Bottom -> whatever となるが，今まではこれの実装は， bottomElimination bot = bottomElimination bot bottomElimination (Bottom bot) = bottomEl
copatterns概要 - ぼくのぬまち 出張版
ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ． タプルをレコードで定義すると，次のようになる． record _×_ (A B : Set) : Set where constructor _,_ field fst : A snd : B open _×_タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える． 通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる． pair : {A B : Set} →
IOアクションひとつひとつを利用許諾し・テスト可能にする - ぼくのぬまち 出張版
IOのテストってたいへんだ．これをどうにかするために，先人たちは色々考え， 利用対象の特定IOアクションを慎重に取捨選択し，MonadHogeIOのような型クラスによりインターフェースを与えてからそのインターフェース上のアクションとして実装する．実行時は目的のインスタンスの上で走らせるし，テスト時はMock用インスタンスの上で走らせる 同様に特定IOアクションを慎重に取捨選択し，FreeモナドやOperationalモナドによりインターフェースを与えて以下略．目的のランナーで走らせたり，テスト用のランナーで走らせたりする といった手段を取る． で，普通テスト用のものはピュアになるように実装し，テストしやすくする．具体的には，型クラスとモナドと Free モナド - あどけない話や，Freeモナドを超えた！？operationalモナドを使ってみよう - モナドとわたしとコモナドがわかりやす
孤独のHaskell - ぼくのぬまち 出張版
孤独のHaskellに行ってきた．ので，感想とそのフォローアップになりそうなことを書く． とてもいい会だったように思う． 遅刻して現場に付いたらRLEしてみようという例題("AABBCCC"を"A2B2C3"にする関数を書こう)をやっていて， id:khibino0 さんがおもむろに import Data.List ( group ) import Control.Arrow rle = concatMap (uncurry (:) . (head &&& show . length)) . group のような解をブッパしてたりするなど．で，各自自前実装してる人たちのコードとか見ると「細かい操作でボトムアップにやりたいことを実現しようとしてるなー」と感じることが多かった．Haskellの場合(なのかは知らないが)もっと大域的な変換からトップダウンに考えていったほうがシンプルでソレっぽい
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
