tapl24.f

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

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))));