yhsiang: 掉隊了，邊看書補 type theory 邊打混...