Agda セミナー一日目に行ってきた

Agda

Erlang Super Lite をサボって何をしてたかというと．
Agda を勉強してきた．
初日は午後 13:00-17:00 でした．

  • 12 人居る
  • 駅から遠い．雨が降ってれば尚更
  • Haskell がわかれば，とりあえず最初の一日目は付いていける
  • 資料に文句をつけてみた．
  • Set と where を毎回書くのが面倒過ぎる
  • 依存型とかで型をメタな感じで定義するのがおもろい
    • data Aaa (A : Set) : (B : Set) -> Set where みたいな
  • Emacs 含めた統合環境というのがいい
  • そこは，flymake でいーんじゃないか？

初日なので様子見的な立ち位置でした．

Real World Haskell 読み始めてて良かったと思いました．
明日からはもうちょっと証明っぽいことをやるかなぁ？