Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- let f = fun(x) x in pair (f(3)) (f(true))
- A = { 3:int, true:bool, pair: forall alf, beta. alf->beta->(alf x beta) }
- AST:
- Let:t12
- / | \
- / | \
- / | \
- f:* x:* apply:t11
- / \
- / \
- / \
- apply:t7 apply:t10
- / \ / \
- / \ / \
- / \ / \
- pair:<I> apply:t6 f:<I> true:bool
- / \
- / \
- f:<I> 3:int
- *: GEN
- I: lookup(<ID>, A) and INST
- Derivation:
- --------------------
- x:X |- x:X | {} (VAR)
- -------------------
- |- \x. x: X->X | {} (ABS) FTV(<empty env/context>) does not contain X
- -------------------
- |- (\x. x): forall X. X->X (GEN)
- Hence, due to "Let f=fun(x) x in <body>", enter f: forall X. X->X into A.
- A = { 3:int, true:bool, pair: forall alf, beta. alf->beta->(alf x beta), f: forall X. X->X }
- --------------- ---------------------
- A |- 3:int | {} A |- f:t41->t41 | {} (INST)
- ---------------------- ------------------- ------------------------------ --------------------------------------
- A |- true:bool | { } A |- f:t81->81 | {} A |- pair:a1->b1->(a1xb1) | {} A |- f 3:t6 | { t41->t41 = int -> t6 } (pair via INST)
- ------------------------------------------------------- -------------------------------------------------------------------------
- A |- f true :t10 | {t81->t81 = bool->t10} A |- pair f 3:t7 | { a1->b1->(a1xb1) = t6->t7 }
- ---------------------------------------------------------------------------------------------------------------------------------
- A |- pair (f 3) (f true):t11 | {t81->t81 = bool->t10, t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7 = t10->t11 }
- ---------------------------------------------------------------------------------------------------------------------------------
- A |- Let ... pair (f 4) (f true):t12 | {t81->t81 = bool->t10, t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7 = t10->t11, t12=t11 }
- C = {t81->t81 = bool->t10, t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7=t10->t11, t12=t11}
- t = let f = \x.x in pair (f(3)) (f(true))
- S = t12
- T = SIGMA S
- X = { t81,t10,t41, t6, a1,b1, c1,t8, t11, t12}
- Unification steps:
- C = { t81 = bool, t81 = t10 , t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7=t10->t11, t12=t11 }
- SIGMA = {t81 |-> bool }
- C = { bool = t10 , t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7=t10->t11, t12=t11 }
- SIGMA = { t10 |-> bool } o {t81 |-> bool }
- C = { t41->t41 = int -> t6, a1->b1->(a1xb1) = t6->t7, t7=bool->t11, t12=t11 }
- C = { t41= int, t6 = int, a1->b1->(a1xb1) = t6->t7, t7=bool->t11, t12=t11 }
- SIGMA = { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- C = { a1->b1->(a1xb1) = int->t7, t7=bool->t11, t12=t11 }
- C = { a1 = int, b1->(a1xb1) = t7, t7=bool->t11, t12=t11 }
- SIGMA = {a1 |-> int} o { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- C = { b1->(intxb1) = t7, t7=bool->t11, t12=t11 }
- SIGMA = {t7 |-> b1->(intxb1) } o {a1 |-> int} o { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- C = { b1->(intxb1) = bool->t11, t12=t11 }
- C = { b1 = bool, (intxb1) = t11, t12=t11 }
- SIGMA = {b1 |-> bool} o {t7 |-> b1->(intxb1) } o {a1 |-> int} o { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- C = { (intxbool) = t11, t12=t11 }
- SIGMA = { t11 |-> (intxbool) } o {b1 |-> bool} o {t7 |-> b1->(intxb1) } o {a1 |-> int} o { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- C = { (intxbool) = t12 }
- SIGMA = {t12 |-> (intxbool) } o { t11 |-> (intxbool) } o {b1 |-> bool} o {t7 |-> b1->(intxb1) } o {a1 |-> int} o { t41 |-> int} o { t6 |-> int} o { t10 |-> bool } o {t81 |-> bool }
- T = SIGMA t12 = intxbool
- Instead of using GEN and INST, you could also use LETPOLY (make copies), and ABSINF (assign new type to each copy).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement