Skip to content

Instantly share code, notes, and snippets.

@krtx
Created June 8, 2017 03:27
Show Gist options
  • Save krtx/6fe5c14beab0815fa3a6d5bcbb4b7ffd to your computer and use it in GitHub Desktop.
Save krtx/6fe5c14beab0815fa3a6d5bcbb4b7ffd to your computer and use it in GitHub Desktop.
/* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */
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 を実装することはできるが、異なる2つのオブジェクトを開いたときに
型変数も異なるため、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))));
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment