自己紹介

芳賀 雅樹 (はが まさき)

  • Web サービスの設計や開発を行う会社でパソコンをカタカタして働いている,修士 (工学) の社会人です.
  • しらそら (silasolla) というハンドルネームでインターネットを使っています.
  • ググると両手ピースしている恥ずかしい写真が出てくるのでググらないでください.

プログラミングについて

理論計算機科学 (プログラミング言語の基礎理論など) や,関数型プログラミングが好きです.プログラミング言語の意味論や型システム,またそれらの恩恵を得た,開発者に優しい言語やツールに興味があります.(業務では PHP ばかり書いていますが..)

大学在学中は,主に項書き換えや定理自動証明を専門としている研究室で,数理論理学を用いたソフトウェア基礎理論について研究していました.

卒論:循環証明体系の等式論理バージョンを作って,項書き換えに応用できないかなって考えてました.
修論:変数束縛を項書き換えで上手く取り扱う枠組みを研究していました.論文が PPL 2022 の査読に通って発表もしました.

プログラミング「言語」について

ソフトウェアを開発するための手段として,プログラムを書く体験だけではなく,プログラミング言語そのものに強い興味があります.この言語がこの言語から影響を受けているとか,この機能とこの機能はトレードオフの関係だとか,この言語は従来と別の手段で問題を解決しているとか,よく調べたりします.

以下のような性質を持ったプログラミング言語が好きです.

  • シンプルに書ける素直さ
  • 型安全で例外ばかり投げない誠実さ
  • 注釈なしでも型推論してくれる包容力
  • 代数的データ型やパターンマッチの柔軟性
  • 中二病心をくすぐるような黒魔術もできちゃうカリスマ性
etc.

ML (特に Standard ML)

特に型推論が優秀で,書き手に優しく Haskell よりもゆるくプログラミングできるのが好きです.臨機応変に逐次実行して,手続き型っぽく書けるのも良いです.研究室で出会ってから,ずっと触っています.システム開発での実用化を目指した SML# プロジェクトを応援しています.

Haskell

すごい Haskell を読んでから,関数型プログラミングの沼に引き込まれました.思い入れのある言語です.(一応正格評価にできるとはいえ) 非正格評価は難しいし,処理系の管理も大変ですが,面白い言語なので,死ぬまでには業務で使ってみたいです.

Elm (および Elm Architecture)

親切なコンパイルエラーをはじめとした,プログラマに寄り添うようなホスピタリティが好きな言語です.Haskell が引き合いに出されることも多いですが,洗練された設計で (良い意味で) 機能が絞られており,黒魔術しがちな Haskell とは正反対かなと思います.

Scheme

call/cc を使ったコードの解読ゲームとか面白いと思います.Common Lisp はあんま好きじゃない.

この他にも

  • WebAssembly
  • Koka
  • Scala
  • F# (とか F* とか)
  • Idris
  • Rust
  • PureScript
  • Agda
あたりには,興味があります.

好きなもの

音楽鑑賞

クラシックや現代音楽から世界の民謡やロックバンドまで,幅広く音楽を聴きます.

クラシックだと,特に Alkan, Liszt, Brahms, Bruckner, Franck, Sibelius, Webern, Varèse, Messiaen, Xenakis, Penderecki, Crumb, 諸井三郎, 湯浅譲二 あたりの作品が好きです.

ポピュラー音楽だと,King Gnu ってバンドがお気に入りです.どのアルバムも何周したかわからんくらい聴きました.

楽器演奏

母親がピアノの先生だった名残で実家にピアノが数台あるため,帰省したときによく練習しています.幼少期は指が届かなくて母のレッスンを拒否していましたが,大人になってから改めて弾いてみると,手が大きくなったぶん可能なことが増えて,楽しいなと感じています.最近は,木製のリコーダーを入手して,教本を読みながら練習しています.

あとは,Tuba を中学1年生から大学卒業まで,ずっと演奏していました.自分の楽器がほしいです.Vaughan Williams の Tuba Concerto とか,Penderecki の Capriccio とか,Nelhýbel の Ludus とか,おもしろいので聴いてみてください.

数学

数理論理学や基礎論ばかりやっていますが,代数などを中心にメタじゃないのも興味あります.演繹で理論全体が大きな生き物のように繋がっていて面白いなと思います.

歩くこと

Google Map には頼らずに,長めの散歩をよくします.買い物や通院や外食など,日常生活でも歩くことが多いです.2日で 42.195 × 2 km 歩いたこともあります.最近は,浅草から新宿まで歩きました.

読書

コンピュータや数学などの理工書を中心に,謎雑学系の本や,小説もちょいちょい読みます.小説だと SF (Asimov, Bradbury, Dick, Orwell など) を読みがちです.あと『空の境界』の原作小説を読んだりもしました.

けろけろけろっぴ

かわいい.とてもかわいい.人気投票で毎年投票してます.部屋のカーテンも文房具もよく使う LINE スタンプも全部けろっぴです.

けろっぴ > キキララ >>>> (可算無限個続く) >>>> {その他有象無象} だと思う.

おいしいものを食べること

  • 塩分無添加のトマトジュース
  • 焼き魚,刺身,お寿司
  • 揚げたての天ぷら
  • ラーメン (主に塩)
  • シュークリーム
  • クリームワッフル
  • じゃがいも
  • 高カカオチョコレート
  • 豆腐 (木綿と絹どっちも)

誰も傷つかないほのぼの系のアニメを見ること

もうこういうのばっか見てる.ごちうさを見ると心が満たされます.最近はお気持ちに余裕が出てきて,つらい話も見てるかも.

自己言及文,回文,駄洒落

言葉遊びが好きです

自分

他人に優しく,自分にちょー優しいです

苦手なもの

  • 税金
  • 騒音
  • 人混み
  • 財務省
  • 変電所
  • 巨大な鉄塔
  • 動的型付け
  • ゴシップネタ
  • 三人以上での雑談
  • ダブルスタンダード
  • 席を立つこと前提の大人数での飲み会
  • 共感性羞恥を刺激するドラマやアニメ
  • プロローグで主人公を虐げるシナリオ
  • リベラリズムを主張しながら他者から自由を略奪する思想