(empty log message)
experimental/typing/typed/core.ml (diff)
experimental/typing/typed/memo.txt (diff)| @@ -12,10 +12,34 @@ | ||
| 12 | 12 | |
| 13 | 13 | def evil_id = evil (\x.x); |
| 14 | 14 | |
| 15 | +def evil_id' = (\f. | |
| 16 | + let r = ref {} in \x. | |
| 17 | + let y = !r in let _ = := r {f x} in | |
| 18 | + if (is_nil y) (hd (!r)) (hd y)) (\x.x) | |
| 15 | 19 | |
| 20 | +---> rがクロージャに閉じ込められる | |
| 21 | + => 同じになるはず | |
| 22 | +def r0 = !(ref {}); | |
| 23 | +def r1 = ref {}; | |
| 24 | +def r2 = let r = ref {} in r; | |
| 25 | +def r3 = let r = ref {} in !r; | |
| 16 | 26 | |
| 17 | ----> rがクロージャに閉じ込められる | |
| 18 | 27 | |
| 28 | +(\<t0>.(\<t1>.(\<t2>. | |
| 29 | +(\f':(t0(2) -> t1(1)). | |
| 30 | + (let r:(<t0'> => (Ref (List t0'(0)))) | |
| 31 | + = (\<t0'>.(((ref <(List t0'(0))>) <*>) (nil <t0'(0)>))) | |
| 32 | + in (\x:t0(4). | |
| 33 | + (let y:(<t0'> => (List t0'(0))) = | |
| 34 | + (\<t0'>.((! <(List t0'(0))>) (r(2) <t0'(0)>))) | |
| 35 | + in | |
| 36 | + (let _ :(List t1(5)) = (((:= <(List t1(5))>) (r(2) <t1(5)>)) (((cons <t1(5)>) (f'(3) x(1))) (nil <t1(5)>))) | |
| 37 | + in ((((if(12) <t2(5)>) ((is_nil(10) <X57(rank:0)>) (y(1) <X57(rank:0)>))) ((hd(11) <t2(5)>) ((! <(List t2(5))>) (r(3) <t2(5)>)))) ((hd(11) <t2(5)>) (y(1) <t2(5)>)))) | |
| 38 | +) | |
| 39 | +) | |
| 40 | +) | |
| 41 | +) | |
| 42 | +))) | |
| 19 | 43 | |
| 20 | 44 | |
| 21 | 45 | "Syntactic approach to type soundness" |