このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

%E3%82%B9%E3%83%86%E3%83%95%E3%82%A1%E3%83%8D%E3%82%B9%E3%82%AF, %E9%95%B7%E8%B0%B7%E5%B7%9D の検索結果:

型理論が気持ちよく出来る圏とは

デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ(あくまで“感じ”)の圏を考えましょう。内容: 実用上必要そうな型 どんな圏ならいいのか トレース付きデカルト圏 実用上必要そうな型プログラミング言語でサポートされているのが望ましい型には、次のものがあるのでしょう。 幾つかの組み込み型 直積型 関数型 シグマ型 パイ型 再帰的型 組み込み型につ…