Intuitionism

    The Rise of Intuitionistic Logic

    Intuitionism Zh

    直構邏輯的崛起

    Coinduction

    There’s only one way, namely impurity, to produce an instance of a coinductive type. What I was wondering is, in comparison, why can we build inductive types anywhere?

    Monads in Category Theory for Laymen

    Chinese version: here

    我的monad教學

    英文版:這裡

    The need for another hierarchy of universes in system programming languages

    In the first edition of Martin-Löf’s type theory preprinted in 1971, Martin-Löf introduced a universe, normally called \(\mathcal{U}\), in his theory.
    It contains (i.e. is the type of) all types including the universe itself.
    After the theory was quickly found to be inconsistent by Girard, Martin-Löf then presented a so called “predicative” theory, with a hierarchy of universes, each usually written with a subscript, e.g. \(\mathcal{U}_0\), \(\mathcal{U}_1\), \(\mathcal{U}_2\) …, and the type of each universe is the higher one universe.
    So, for example, the type of \(\mathcal{U}_0\) is \(\mathcal{U}_1\), and the type of \(\mathcal{U}_1\) is \(\mathcal{U}_2\), and going on and on.
    In this article, I exploit the need for (at least) one other hierarchy of universes, written \(..\mathcal{U}_n\), in which \(n\) is a natural number in the metatheory, as in the above notation \(\mathcal{U}_n\).

    Lambda Calculus (8 - Martin-Löf Type Theory: recursors)

    之前在講解Curry-Howard correspondence時
    我用的理論基礎是CoC
    而CoC最大的問題在於:
    它無法證明數學歸納法
    為什麼呢?
    首先來看看CoC中的自然數
    還記得我最最前面在untyped lambda那篇介紹的定義嗎……

    Lambda Calculus (6 - Curry-Howard correspondence)

    這篇文章會討論有點不同的主題
    從這個問題開始:
    你要怎麼寫一個term
    使得他的type為\(\forall X. X\)?

    Modes: An Ubiquitous yet Overlooked Concept in Programming

    The first programming language that I learned seriously is Java.
    I’ve quickly come out with an interpretation that whatever language features in Java correspond to parts of speech.
    Variables are nouns;
    this is the subject and the arguments after the name of the method call are objects;
    methods are verbs and interfaces are adjectives.

    abstract algebra (1 - group)

    在抽象代數中
    一個很重要的概念是群(group)
    一個群定義了一個集合和其上的一個二元運算的關係
    在介紹群之前
    我要先介紹比群更簡單的結構

    CTAGI (1.1 - The very idea of a category)

    1.1 The very idea of a category

    CTAGI (1.2 - The category of sets)

    1.2 The category of sets

    CTAGI (1.3 - More examples)

    1.3 More examples

    CTAGI (0 - A very short introduction)

    新連載:D
    先介紹一下這系列文章會出現的背景吧

    Lambda Calculus (7 - PTS)

    PTS是lambda cube的再度延伸
    在CoC中
    \(\star\)和\(\Box\)被稱為sort
    sort是什麼呢?
    它是較低層一般型別的型別
    舉例來說
    \(\forall A. A \to A: \star\)
    \(\star \to \star: \Box\)
    但假如我們有個從一般kind到一般kind的lambda
    它的型別不會是\(\Box\)
    而會是\(\Box \to \Box\)

    Jekyll(3)

    我決定重新來過
    砍了整個repo
    然後建立一個預設的新專案觀察一個Jekyll網站的架構

    Jekyll(1)

    我想把部落格轉移到Jekyll
    為什麼用Logdown撰寫文章不好呢?
    原因有二:

    Jekyll(2)

    看了一下
    Jekyll實在很複雜
    看起來是滿通用的一套架構
    但也因為如此不好理解
    我想先套用Jekyll Bootstrap
    之後再慢慢修改它的程式碼使其符合自己需要
    首先刪除掉原有repo的所有檔案
    在命令提示字元中輸入

    git clone https://github.com/plusjade/jekyll-bootstrap.git AndyShiue.github.io
    cd AndyShiue.github.io
    git remote set-url origin git@github.com:AndyShiue/AndyShiue.github.io.git
    git push --force origin master
    

    注意我事實上修改了一些部分
    原本命令中的所有com都被我改成了io
    另外push後面加了參數--force
    這樣才對

    Lambda Calculus (5 - CoC)

    現在我們要再加入term到type的函數
    這樣的系統被稱為CoC(Calculus of Constructions)
    來整理一下目前的狀況

    Lambda Calculus (4 - system Fω)

    開門見山
    system F導入了type到term的函數
    system Fω則再導入了type到type的函數
    現在我們要導入type的型別
    還記不記得一開始在用untyped lambda的時候是沒有型別的
    這麼一來能寫出\(\Omega\)之類的無窮迴圈
    假如type到type的函數是無型別的話
    那不就也能在type階層上跑無窮迴圈了嗎QAQ
    不……

    Lambda Calculus (3 - system F)

    在之前STLC的教學中
    我們的世界被分成了兩個階層:term和type
    接下來
    我們會希望這兩者的差別變得更模糊
    為什麼要這麼做?
    因為lambda calculus可以被當作是程式語言的核心
    在寫程式的時候
    建立抽象是必要的過程
    有了高層次的抽象
    能讓不同的東西被視為一樣的
    減少重複的冗餘程式碼
    因此程式語言上也應該提供更高的抽象能力以幫助使用者

    Lambda Calculus (2 - STLC)

    講完untyped lambda
    接下來就要講typed lambda啦
    顧名思義
    typed lambda就是有type的lambda
    因此必須要被type check
    一個合理的type checker不會讓所有程式都type check成功
    而是只接受特定的一些「正確的」程式
    因此讓程式的錯誤能在編譯時期就被找出來

    Lambda Calculus (1 - untyped lambda)

    來寫教學吧
    畢竟我最喜歡寫教學了…XD
    這次要來說的是untyped lambda

訂閱RSS