This note aims at understanding the main codebase of Agda, i.e. the directory src/full/Agda/. For now, we focus on its type checking and reflection mechanism. In this note, a file path src/full/Agda/Foo/Bar.hs will be referred to as Agda.Foo.Bar, adapting the notation of Haskell's module system. Requirements We assume the reader has the following skills: Be familiar with basic concepts of compilers. Be familiar with Haskell and its toolchain Cabal or Stack. Have the experience with building Agda from source.

# 開源史就是電腦史 ## 從計算機到程式 <!-- > 簡介 > 開放原始碼（Open Source）在軟體界扮演了舉足輕重的角色，現在想要接觸程式設計、都必定要跟開源軟體打交道。又或者我們可以說，現代資訊世界的構築，與開源軟體早已密不可分。正是因為開放原始碼，軟體不再是一個個黑盒子，我們可以瞭解每天使用的軟體是怎麼被實作的、可以擁有選擇的自由、可以成為自己電腦的主人。 > > 開源社這學期的第一次講座我們要從電腦與程式的歷史講起，什麼是開源呢？為什麼要這麼做？現代的開源生態、或現代的資訊世界是怎麽被構建而成？ > 接著更進一步探討程式的概念——我們所開源的對象，也就是程式語言的代碼，又是從何而來、能夠如何學習與理解呢？ > > 不論你想學習如何寫程式、想瞭解開放原始碼的文化與歷史，或是單純想來聊天跟分享你的看法，都歡迎來聽這場講座。 > > 地點：臺灣大學第一活動中心 103 > 主講人：林子期 --> ---- ### 計算機始祖