Skip to content

Instantly share code, notes, and snippets.

@krtx

krtx/tapl24.f

Created June 8, 2017 03:27
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save krtx/6fe5c14beab0815fa3a6d5bcbb4b7ffd to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save krtx/6fe5c14beab0815fa3a6d5bcbb4b7ffd to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. krtx created this gist Jun 8, 2017.
    484 changes: 484 additions & 0 deletions tapl24.f
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,484 @@
    /* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */

    Pair = lambda X. lambda Y. All R. (X -> Y -> R) -> R;

    pair = lambda X.
    lambda Y.
    lambda x: X.
    lambda y: Y.
    lambda R.
    lambda p: X -> Y -> R.
    p x y;

    fst = lambda X. lambda Y. lambda p: Pair X Y.
    p [X] (lambda x: X. lambda y: Y. x);
    snd = lambda X. lambda Y. lambda p: Pair X Y.
    p [Y] (lambda x: X. lambda y: Y. y);

    List = lambda X. All R. (X -> R -> R) -> R -> R;

    nil = lambda X.
    (lambda R. lambda c: X -> R -> R. lambda n: R. n)
    as List X;

    cons = lambda X. lambda hd: X. lambda tl: List X.
    (lambda R. lambda c: X -> R -> R. lambda n: R. c hd (tl [R] c n))
    as List X;

    isnil = lambda X. lambda l: List X.
    l [Bool] (lambda hd: X. lambda tl: Bool. false) true;

    diverge = lambda X. lambda _: Unit. fix (lambda x:X. x);

    head = lambda X. lambda l: List X.
    (l [Unit -> X]
    (lambda hd: X.
    lambda tl: Unit -> X.
    lambda _: Unit.
    hd)
    (diverge [X]))
    unit;

    tail = lambda X. lambda l: List X.
    (fst [List X] [List X] (
    l [Pair (List X) (List X)]
    (lambda hd: X. lambda tl: Pair (List X) (List X).
    pair [List X] [List X]
    (snd [List X] [List X] tl)
    (cons [X] hd (snd [List X] [List X] tl)))
    (pair [List X] [List X] (nil [X]) (nil [X]))))
    as List X;

    iseven =
    fix (lambda f: Nat -> Bool. lambda x: Nat.
    if iszero x then true
    else if iszero (pred x) then false
    else f (pred (pred x)));

    plus =
    fix (lambda f: Nat -> Nat -> Nat.
    lambda x: Nat.
    lambda y: Nat.
    if iszero x then y
    else succ (f (pred x) y));

    times =
    fix (lambda f: Nat -> Nat -> Nat.
    lambda x: Nat.
    lambda y: Nat.
    if iszero x then 0
    else plus y (f (pred x) y));

    equal =
    fix (lambda f: Nat -> Nat -> Bool.
    lambda x: Nat.
    lambda y: Nat.
    if iszero x then iszero y
    else if iszero y then false
    else f (pred x) (pred y));

    /* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */

    p = {*Nat, {a=5, f=lambda x: Nat. succ x}}
    as {Some X, {a: X, f: X -> X}};

    p1 = {*Nat, {a=5, f=lambda x: Nat. succ x}}
    as {Some X, {a: X, f: X -> Nat}};

    p2 = {*Nat, 0} as {Some X, X};

    p3 = {*Bool, true} as {Some X, X};

    /* 実用的な例 */

    p4 = {*Nat, {a=0, f=lambda x: Nat. succ x}}
    as {Some X, {a: X, f: X -> Nat}};

    p5 = {*Bool, {a=true, f=lambda x: Bool. 0}}
    as {Some X, {a: X, f: X -> Nat}};

    /* 演習24.1.1. 有用でない例 */

    /* 返り値の型が全て隠蔽されているのでモジュールの外で利用できる値がない */

    p6 = {*Nat, {a=0, f=lambda x: Nat. succ x}}
    as {Some X, {a: X, f: X -> X}};

    p7 = {*Nat, {a=0, f=lambda x: Nat. succ x}}
    as {Some X, {a: X, f: Nat -> X}};

    /* 型がすべて Nat なので隠蔽する意味がない */

    p8 = {*Nat, {a=0, f=lambda x: Nat. succ x}}
    as {Some X, {a: Nat, f: Nat -> Nat}};

    /* 存在型の除去 */

    let {X, x} = p4 in (x.f x.a);
    let {X, x} = p4 in (lambda y: X. x.f y) x.a;

    /* x.a を具体的な数として扱うことは許されていない */

    /* let {X, x} = p4 in succ x.a; */

    /* 結果の型 t2 は X を自由に含むことができない */

    /* let {X, x} = p4 in x.a; */

    /* 存在型によるデータ抽象 */

    counterADT =
    {*Nat,
    {new = 1,
    get = lambda i: Nat. i,
    inc = lambda i: Nat. succ i}}
    as {Some Counter,
    {new: Counter,
    get: Counter -> Nat,
    inc: Counter -> Counter}};

    let {Counter, counter} = counterADT in
    counter.get (counter.inc counter.new);

    let {Counter, counter} = counterADT in
    let add3 = lambda c: Counter. counter.inc
    (counter.inc
    (counter.inc c))
    in
    counter.get (add3 counter.new);

    let {Counter, counter} = counterADT in

    let {FlipFlop, flipflop} =
    {*Counter,
    {new = counter.new,
    read = lambda c: Counter. iseven (counter.get c),
    toggle = lambda c: Counter. counter.inc c,
    reset = lambda c: Counter. counter.new}}
    as {Some FlipFlop,
    {new: FlipFlop,
    read: FlipFlop -> Bool,
    toggle: FlipFlop -> FlipFlop,
    reset: FlipFlop -> FlipFlop}} in

    flipflop.read (flipflop.toggle (flipflop.toggle flipflop.new));

    /* プログラムの残りの部分が get と inc 以外の方法で Counter
    のインスタンスにアクセスすることはできない、ということが
    保証されているので、Counter の ADT を別実装に置き換えられる */

    counterADT =
    {*{x: Nat},
    {new = {x=1},
    get = lambda i: {x: Nat}. i.x,
    inc = lambda i: {x: Nat}. {x=succ i.x}}}
    as {Some Counter,
    {new: Counter,
    get: Counter -> Nat,
    inc: Counter -> Counter}};

    /* 演習24.2.1 (数の)スタックの抽象データ型 */

    stackADT =
    lambda X.
    {*List X,
    {new = nil [X],
    push = cons [X],
    top = head [X],
    pop = tail [X],
    isempty = isnil [X]}}
    as {Some Stack,
    {new: Stack,
    push: X -> Stack -> Stack,
    top: Stack -> X,
    pop: Stack -> Stack,
    isempty: Stack -> Bool}};

    let {Stack, stack} = stackADT [Nat] in
    stack.top
    (stack.push 3
    (stack.push 2
    (stack.push 1 stack.new)));

    let {Stack, stack} = stackADT [Nat] in
    stack.top
    (stack.pop
    (stack.push 3
    (stack.push 2
    (stack.push 1 stack.new))));

    let {Stack, stack} = stackADT [Nat] in
    stack.isempty
    (stack.pop
    (stack.pop
    (stack.push 3
    (stack.push 2
    (stack.push 1 stack.new)))));

    let {Stack, stack} = stackADT [Nat] in
    stack.isempty
    (stack.pop
    (stack.pop
    (stack.pop
    (stack.push 3
    (stack.push 2
    (stack.push 1 stack.new))))));

    /* 演習 24.2.2 書き換え可能なカウンタのADT */

    counterRefADT =
    {*(Ref Nat),
    {new = lambda _: Unit. ref 1,
    get = lambda c: Ref Nat. !c,
    inc = lambda c: Ref Nat. (c := succ (!c); c)}}
    as {Some Counter,
    {new: Unit -> Counter,
    get: Counter -> Nat,
    inc: Counter -> Counter}};

    let {CounterRef, counterRef} = counterRefADT in
    counterRef.get
    (counterRef.inc
    (counterRef.inc
    (counterRef.new unit)));

    Counter = {Some X,
    {state: X,
    methods: {get: X -> Nat,
    inc: X -> X}}};

    c = {*Nat,
    {state = 5,
    methods = {get = lambda x: Nat. x,
    inc = lambda x: Nat. succ x}}}
    as Counter;

    let {X, body} = c in body.methods.get body.state;

    sendget = lambda c: Counter.
    let {X, body} = c in body.methods.get body.state;

    sendget c; /* = 5 : Nat */

    /* 型変数 X が let の本体の型として自由に出現するためエラー */
    /* let {X, body} = c in body.methods.inc body.state; */

    /* inc を呼び出したあとカウンタオブジェクトとして再パッケージする
    必要がある */

    c1 = let {X, body} = c in
    {*X,
    {state = body.methods.inc body.state,
    methods = body.methods}}
    as Counter;

    /* より一般的に、カウンタに「incメッセージを送る」関数 */

    sendinc = lambda c: Counter.
    let {X, body} = c in
    {*X,
    {state = body.methods.inc body.state,
    methods = body.methods}}
    as Counter;

    sendget (sendinc c); /* = 6 : Nat */

    /* カウンタに対する、より複雑な操作 */

    add3 = lambda c: Counter. sendinc (sendinc (sendinc c));

    sendget (add3 c); /* = 8 : Nat */

    /* 演習24.2.3 Counter オブジェクトを内部表現の型として使って FlipFlop
    オブジェクトを実装せよ */

    counterNew = lambda a: Nat.
    {*Nat, {state = a,
    methods = {get = lambda x: Nat. x,
    inc = lambda x: Nat. succ x}}}
    as Counter;

    counterZero = counterNew 0;

    FlipFlopType =
    {Some X,
    {state: X,
    methods: {read: X -> Bool,
    toggle: X -> X,
    reset: X -> X}}};

    f =
    {*Counter,
    {state = counterZero,
    methods = {read = lambda c: Counter. iseven (sendget c),
    toggle = lambda c: Counter. sendinc c,
    reset = lambda c: Counter. counterNew 0}}}
    as FlipFlopType;

    sendread = lambda f: FlipFlopType.
    let {F, body} = f in body.methods.read body.state;
    sendtoggle = lambda f: FlipFlopType.
    let {F, body} = f in
    {*F,
    {state = body.methods.toggle body.state,
    methods = body.methods}}
    as FlipFlopType;
    sendreset = lambda f: FlipFlopType.
    let {F, body} = f in
    {*F,
    {state = body.methods.reset body.state,
    methods = body.methods}}
    as FlipFlopType;

    sendread f; /* 0 (true) */
    sendread (sendtoggle f); /* 0 -> 1 (false) */
    sendread (sendtoggle (sendtoggle f)); /* 0 -> 1 -> 2 (true) */
    sendread (sendtoggle (sendreset (sendtoggle f))); /* 0 -> 1 -> 0 -> 1 (false) */

    /* 演習24.2.4 状態を持つ Counter オブジェクト */

    cref =
    {*(Ref Nat),
    {state = ref 1,
    methods = {get = lambda x: Ref Nat. !x,
    inc = lambda x: Ref Nat. (x := succ (!x); x)}}}
    as Counter;

    let {C, c} = cref in
    let cref =
    {*C,
    {state = c.methods.inc c.state,
    methods = c.methods}}
    as Counter in
    let {C, c} = cref in
    c.methods.get c.state;

    sendget (sendinc cref);

    EqCounter =
    {Some X,
    {state: X,
    methods: {get: X -> Nat,
    inc: X -> X,
    eq: X -> EqCounter -> Bool}}};

    eqCounterObj =
    {state = 0,
    methods = {get = lambda i: Nat. i,
    inc = lambda i: Nat. succ i,
    eq = lambda i: Nat.
    lambda c: EqCounter.
    let {X, cbody} = c in
    equal i (cbody.methods.get cbody.state)}};

    /* なんか駄目 */
    /* eqCounter = {*Nat, eqCounterObj} as EqCounter; */

    /* 演習 24.2.5 以下の型も使えない */

    NatSet =
    {Some X, {state: X,
    methods: {empty: X,
    singleton: Nat -> X,
    member: X -> Nat -> Bool,
    union: X -> X -> X}}};

    /* union を実装することはできるが、異なる２つのオブジェクトを開いたときに
    型変数も異なるため、union に引数として与えることができない */

    natset1 =
    {*(List Nat),
    {state = nil [Nat],
    methods = {empty = nil [Nat],
    singleton = lambda x: Nat. cons [Nat] x (nil [Nat]),
    member = lambda s: List Nat. lambda x: Nat. false,
    union = lambda s: List Nat.
    lambda t: List Nat. nil [Nat]}}}
    as NatSet;

    /* 自分自身を与えることはできる */
    let {NS1, ns1} = natset1 in
    {*NS1,
    {state = ns1.methods.union ns1.state ns1.state,
    methods = ns1.methods}}
    as NatSet;

    natset2 =
    {*(List Nat),
    {state = nil [Nat],
    methods = {empty = nil [Nat],
    singleton = lambda x: Nat. cons [Nat] x (nil [Nat]),
    member = lambda s: List Nat. lambda x: Nat. false,
    union = lambda s: List Nat.
    lambda t: List Nat. nil [Nat]}}}
    as NatSet;

    /* NS1 != NS2 なので parameter type mismatch */
    /* let {NS1, ns1} = natset1 in */
    /* let {NS2, ns2} = natset2 in */
    /* ns1.methods.member (ns1.methods.union ns1.state ns2.state) 10; */

    /* 全称型で存在型を表現する */

    /*
    以下の存在型で実装された counter を全称型で表現する

    counterADT =
    {*Nat,
    {new = 1,
    get = lambda i: Nat. i,
    inc = lambda i: Nat. succ i}}
    as {Some Counter,
    {new: Counter,
    get: Counter -> Nat,
    inc: Counter -> Counter}};

    let {X, c} = counterADT in c.get (c.inc c.new);
    */

    CounterType =
    lambda X. {new: X,
    get: X -> Nat,
    inc: X -> X};

    /* パッケージ化 */
    counterADTAll =
    lambda Y. /* 結果の型 */
    lambda f: (All X. CounterType X -> Y). /* 継続 */
    f [Nat] {new = 1, /* 　 */
    get = lambda i: Nat. i, /* 最終的な結果 */
    inc = lambda i: Nat. succ i}; /* 　 */

    /* アンパッケージ化 */
    counterADTAll [Nat] (lambda X. lambda x: CounterType X. x.get (x.inc x.new));
    /* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    * = f
    * f は ADT が提供する操作(get, inc, new)だけを用いて結果を計算している
    * 内部の具象表現型 X には直接アクセスできない
    */

    negb = lambda b: Bool. if b then false else true;

    counterADTBoolAll =
    lambda Y.
    lambda f: (All X. CounterType X -> Y).
    f [Bool] {new = true,
    get = lambda b: Bool. if b then 0 else 1,
    inc = lambda b: Bool. negb b};

    counterADTBoolAll
    [Nat]
    (lambda X. lambda x: CounterType X.
    x.get x.new);
    counterADTBoolAll
    [Nat]
    (lambda X. lambda x: CounterType X.
    x.get (x.inc x.new));
    counterADTBoolAll
    [Nat]
    (lambda X. lambda x: CounterType X.
    x.get (x.inc (x.inc x.new)));
    counterADTBoolAll
    [Nat]
    (lambda X. lambda x: CounterType X.
    x.get (x.inc (x.inc (x.inc x.new))));