💖アイドルとして勤務する -理論と実践- #imas_hack - みずぴー日記
speakerdeck.com IM@S Engineer Talks - connpassで話した。 あいさつとアジェンダ こんにちは。mzpです。 本日はアイドルアバターで勤務する話をする。 背景: リモートワークの欠点 ボクの“副業”先はリモートワークを推奨している。これには雨の日は出社が面倒くさいと思う人が多かった、名古屋だけではエンジニアを集めれなかった、など様々な事情がある。 チームメンバーの半数は遠隔地に住んでいるため、リモートワークを前提とした働き方が必要となる。 リモートワークはいくつかの利点があるが、欠点もある。 今回は「自室から勤務する」という欠点にスポットをあてる。 カメラに写る範囲に変なものを置けない。 私はリモートワークをする直前に、カメラに写る範囲から物をどかすという作業をしている。 よく写るように、部屋の照明をだいぶ明るくする必要がある。 まぶしい。 この問
F*(F Star)の複雑な型システムの何が嬉しいのか？ - Amosapientiam
マイクロソフトが開発中のF* という依存型プログラミング言語を少し触ってみました。 この言語には強力で複雑な型システムが組み込まれています。 現状、依存型言語は世間にはあまり広まっていませんので F*とは？ 複雑な型ってなんだろう？ 複雑な型システムを組み込んで何が嬉しいんだろう？ 何が嬉しくないんだろう？ と疑問をお持ちになる方も多いだろうと思います。 この記事ではF*で使われている複雑な型の一部と、複雑な型を持つことの利点・欠点の一部を述べ、それを簡単なコード例を通じて体感してみます。 疑問に対する答え F*とは？ マイクロソフトと Inria が開発中のプログラミング言語です。 依存型や monadic effect などが組み込まれており、複雑な仕様が型で表現できます。構文は OCaml や F#などのML系関数型言語に似ています。 詳しくは下記のリンクたちを参照。 F* (プログ
きたない requirements.txt から Pipenv への移行 - 株式会社カブク
ソフトウェアエンジニアの花岡です。今回は、きたない requirements.txt から Pipenv に移行し pipenv graph を使って依存ライブラリを管理しやすくする方法について書きました。 きたない requirements.txt とは、依存ライブラリとその依存ライブラリの指定が混在している requirements.txt ファイルのことです。たとえば $ pip install flask $ pip freeze > requirements.txt のように生成した requirements.txt を使っているとき、本記事ではその requirements.txt を、きたない requirements.txt と呼ぶことにします。 きたなくない requirements.txt とは pip の constraints の正しい用途のように、直接依存している
静的解析の限界、現実世界との境界
2018年に静的解析をとにかく強力につけまくるのは多分あんまりコストに見合わないのでよくない じゃあ静的解析を窓から投げ捨ててよいかというとそれはただの愚行 (以下、静的解析を普通に使えてる人には自明なことしか言いません) 私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき 依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。 一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。 例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
