「型の理論入門」ページのリニューアルを行っています

【「型の理論入門」ページのリニューアルを行っています 】

現在、MaruLabo のページのリニューアルを行っています。

その一環として、以前公開した動画には音声が入っていないサイレントなものがあるのですが、そうした動画に音声での解説を入れ始めました。

今回、最初に選んだのは「型の理論入門」のページです。

「型があるウログラム言語」と「型のないプログラム言語」があることを、多くのプログラマーは知っていると思います。また、その「どちらがいいか」という「論争」があることも知っていると思います。自分が、日常的にどの言語を使うかは、自分で決めればいいことだと思います。

ただ、「計算」と「プログラム」の本質的な特徴を知るには、「型の理論」が不可欠だと丸山は考えています。

今回公開したのは、チャーチの「型のないラムダ計算」の前半部分です。

https://youtu.be/s-HrEz8a4B4?list=PLQIrJ0f9gMcPC8_eEnysTwZm14VRaQWCT

今回の話は、けっして難しいものではありません。

これを入口として、多くのプログラマーが「型の理論」を知ることを期待しています。

まとめページは、「型の理論入門 (トーキー版)」https://www.marulabo.net/docs/type-theory-talkie/ です。まだ、トーキー版完成していません。

少しお待ちください。

コメント

このブログの人気の投稿

マルレク・ネット「エントロピーと情報理論」公開しました。

初めにことばありき

宇宙の終わりと黒色矮星