先週、以下のように書きました。 という項には、という型がつく という項にはという型がつく これらを組み合わせても、の型検査を通すことができない しかし、は、簡約が停止する この矛盾がよくわからなかったのですが、詳しく調べたところ分かったので書い…

論理体系のうちの一つとしてのCoCではなくて、ラムダキューブの位置頂点であるλCと言った方が適切かもしれません。 λCは、全称型・型演算子・依存型をすべて含む、非常に表現力の高い型付きラムダ計算の体系です。 表現力が高いにもかかわらず、型検査が通れ…

切り替えて時間を有効に使いたい

void explicit_bzero(void* s, size_t n)という関数があります。これの動作は、void bzero(void* s, size_t n)という関数と同じです。 void bzero(void* s, size_t n)という関数は、memset(s, '\0', n)と同じ動作をします。つまり、memset関数の方が上位互換…