Among Us の Discord Overlay タスクするクルー

猫も杓子も Among Us なので Discord StreamKit Overlay Custom CSS Generator for Among Us Streamer 作ったという話.年末にやっとこさ重い(石によるものではない)腰を上げてSwitchを買ったので配信環境を整えだした.以前WoWsとかちょこちょこやってたと…

詠唱は不可解だったが、その効力には間違いがなかった。

すっかり年1だけどあんまり長いこと書かないのもアレなのでたまに近況くらいは書いておこうかと 2020年は世の中的にもそうだけど,個人としてもあんまり良い感じではなく総じて謎の石に悩まされる年であった.昨年末年始あたりからVC6とかいうリファレンスも…

singletonsの型レベル関数を使ってしまうと示せない性質の例

↓の話実際singletonsが乱舞するんだけど,singletonsから提供されてる型レベル関数の中には使うと「それ以上証明が進まなくなる」やつが結構な割合で含まれてて,面白味のあるない以前に怒りが先行してしまう.あれは型レベル計算のためのライブラリでしかな…

cerealのgetFloat*多用はメモリ長者にのみ許されし贅沢

約1年も書いてなかったのか. ここ2,3年はそこそこのサイズの配列をどうこうする機会が多く,そういうとき特に何も考えなければ Data.Vector に突っ込んでおきたいキモチになる.で,実際に大きな配列をHaskellで扱うとメモリ不足でOOM Killerに殺されたりす…

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…