このエントリはML Advent Calendar 2020の17日目の記事です。空いてるのも寂しいので埋めます。

κeenです。俺たちのAdvent Calendarはまだまだ続くぜ！ Idrisの標準ライブラリ、preludeとbaseをサクっと解説していきます。

κeenです。Jeremy Gibbsons. 1995. “The Third Homomorphism Theorem” を読んだメモ。 いわゆるリストの第三準同型定理と呼ばれるものについて、原典をあたってみたのでメモを残しておく。

κeenです。俺たちのAdevnt Calendarはまだまだ終わらないぜ！ Idrisの標準ライブラリを含め、世間でモノイド（などの代数構造）とされる型クラスって正しくないよねという話と、正しい定義をする話をします。

このエントリはRust 3 Advent Calendar 2020の16日目の記事です。 前はbantechさんでactix-webでformいろいろ、後はkaz399さんで2020年 Rust で使える Bluetooth Low Energy ライブラリはどうなってるの (Windows10) - Qiitaでした。

空いている日を埋める担当のκeenです。 最近RustのMutexのPoisoningについて動向があったので紹介します。

このエントリはIdris Advent Calendar 2020の25日目の記事です。

今回はIdrisの面白機能の1つElaboratorのリフレクションを利用したメタプログラミング紹介しようと思います。 かなりコアな部分に踏み込むので分からなかったら「へー、そんな機能もあるんだ」と思っておいて下さい。

このエントリはIdris Advent Calendar 2020の24日目の記事です。 前はhiropon21さんでSnocList recursive viewを型駆動開発してみよう in Idris2 でした。 Idris2は1と比べて型システムが微妙に変わっており、ところどころ 0 a のようにその値を使える回数が表示されていたりしますね。

κeenです。今回はIdrisのFFIとCodegenについて触れたいと思います。

このエントリはIdris Advent Calendar 2020の22日目の記事です。

κeenです。今回は依存型を使って部分的に正しさを証明したデータ構造を作っていきたいと思います。 慣れてない人には難しめの内容になるかもしれません。

このエントリはIdris Advent Calendar 2020の21日目の記事です。 前はmock_beginnerさんでIdrisとはじめる型駆動開発でした。

κeenです。大ネタが続いたのでそろそろ小ネタでも。文芸的プログラミングの機能です。

このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。

κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。