2013-01-01から1年間の記事一覧
依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか． こういうことだろうか？ module AC-2013-5 where open import Data.Nat import Relation.Binary.PropositionalEquality …
この記事は 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を書いてし…
この記事は Theorem Prover Advent Calendar 2013 1日目の記事です． 注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！ ﾊヽ／::::ヽ.ヘ===ｧ {::{/≧=＝=≦V…
前回の記事は調査不十分だった．まず，sandbox環境では， cabal install --only-dependencies --enable-tests cabal configure --enable-tests cabal build cabal test を実行したときと， cabal install --enable-tests を実行したときで，config dist pref…
cabal-install-1.18 がきた．全国のHaskeller待望のcabal sandboxが使える．cabal-devさん今までありがとう．さようなら． この記事は余計なことをしている可能性があります！ さて，テスト時にプログラムをビルドする必要があるとする．これは*.cabalファイ…
今年ものとがわさんパンピーやった(1年ぶりn度目) 問題はここ．64bit非負整数に対する限られた関数と単純なlambda式からなるプログラムがコンテストサーバ側にいっぱいあってIDが付いている．サーバ側にある各プログラムの具体的な形はわからない．プログラ…
全国一億三千万のAgdarの皆様に送る Agda Challenge最近chaton haskellがchaton agdaと化していたりすることもあり，anarchy proofがうらやましくてAgda版が欲しい人いっぱいいるのではないかと思って作ってみた．開発中にステージング環境を作り近くの数人…
Agda書くとみんなフォントに困る…と，思う．Agda標準ライブラリの時点で_⊔_とか_⊎_とか⟨_⟩とか普通のランゲッジでは使わないような文字入りの演算が目白押しだ．当然下手なフォント設定すると正しく表示されない．プログラミングに適したmonospaceのフォント…
今年もよろしくおねがいします． 大晦日にghcjsのREADMEが更新され，ghc-7.6ベースになったり，これまで煩雑だったインストール作業がスクリプト化されたりするなど，いろいろと変更があった．実にはタイミングの悪いことに，このREADME更新が行われる直前，…
