Idrisは超ざっくり言うと文法はHaskellにそっくりで機能的にはCoqに近い、依存型を使う言語です。Idris自体の簡単な紹介は前に書いたスライドがあるので、興味がある方はそっちを読んでみてください。 yoda-jp.hatenablog.com 今回は Type Driven Developmen…