Idris 2の数量的型が解決した問題、導入した問題

関数型言語Idrisの次世代版として開発されているIdris 2の大きな特徴の1つとして型システムに数量的型理論(Quantitative Type Theory)を導入していることが挙げられます。このシステムではIdris 1にあった証明環境での利用可能な値の問題や、本来ならば実行時に不要な型を持ってしまっていた問題を解決します。一方で数量的型を便利に使うための仕組みであった多重度の部分型付けにより非健全性が入るなどの問題もありました。本発表ではIdris 2の数量的型のそういった特徴を紹介します。

今さら聞けないアヴィウムプルヌス入門

ハ〜イ、κeenさんだよー。今日は年度が変わって大学でプログラミングをはじめたり、新卒でプログラマになったりする人もいるでしょうということでアヴィウムプルヌスについて解説したいと思います。アヴィウムプルヌスは慣れると便利に使えますが最初はとっつきにくいですよね。