# Lesson XII The brush may be steady, yet a fine stroke asks for ink that will not run. ## Try ```prolog ?- E = kernel, infer(E, [dup, add], Scheme). Scheme = scheme([requires(numeric, A)], effect([A|S], [A|S])). ?- E = kernel, infer(E, [dup, eq], Scheme). Scheme = scheme([requires(equatable, B)], effect([B|T], [bool|T])). ?- E = kernel, infer(E, [push(bool(true)), dup, add], Scheme). Scheme = scheme([requires(numeric, bool)], effect(S, [bool|S])). ``` ## Lesson We encoded capability choices by writing separate concrete rows, such as equality for int and equality for bool. Replace those rows with constrained polymorphic rows because the important fact is not the concrete type alone but the required capability. Inference now returns a scheme carrying obligations, and `find`, `apply`, and `infer` are modified so those obligations stay attached to the stack effect instead of being lost during lookup. > [!info]- Change > ```diff > - word(kernel, dup, [A|S] -- [A, A|S], true). > - word(kernel, drop, [_|S] -- S, true). > - word(kernel, swap, [A, B|S] -- [B, A|S], true). > - word(kernel, over, [A, B|S] -- [B, A, B|S], true). > - word(kernel, add, [A::int, B::int|S] -- [C::int|S], C is B + A). > - word(kernel, sub, [A::int, B::int|S] -- [C::int|S], C is B - A). > - word(kernel, mul, [A::int, B::int|S] -- [C::int|S], C is B * A). > - word(kernel, eq, [A::int, B::int|S] -- [Bool::bool|S], (A == B -> Bool = true ; Bool = false)). > - word(kernel, eq, [A::bool, B::bool|S] -- [Bool::bool|S], (A == B -> Bool = true ; Bool = false)). > - word(kernel, lt, [A::int, B::int|S] -- [Bool::bool|S], (B < A -> Bool = true ; Bool = false)). > - word(kernel, gt, [A::int, B::int|S] -- [Bool::bool|S], (B > A -> Bool = true ; Bool = false)). > - > - find(Env0, Word, InOut, Goal) :- > - nonvar(Env0), > - word(Env0, Word, StoredInOut, StoredGoal), > - copy_term(word(Word, StoredInOut, StoredGoal), word(Word, InOut, Goal)). > - > - apply(Env, Word, Stack0, Stack) :- > - find(Env, Word, InPattern -- OutPattern, Goal), > - bind(InPattern, Stack0), > - call(Goal), > - build(OutPattern, Stack). > - > - infer(_, [], effect(Stack, Stack)). > - infer(Env, [Word|Words], effect(Stack0, Stack)) :- > - infer1(Env, Word, Stack0, Stack1), > - infer(Env, Words, effect(Stack1, Stack)). > - > - infer1(Env, push(Value), Stack, [Type|Stack]) :- > - !, > - lit(Env, Value, Type). > - infer1(_Env, call, [quote(Effect)|Stack0], Stack) :- > - !, > - copy_term(Effect, effect(Stack0, Stack)). > - infer1(Env, Word, Stack0, Stack) :- > - find(Env, Word, InPattern -- OutPattern, _Goal), > - types(InPattern, Stack0), > - types(OutPattern, Stack). > - > - unpack(int, int(Int), Int) :- > - integer(Int). > - > - unpack(bool, bool(Bool), Bool) :- > - ( Bool == true ; Bool == false ). > - > - pack(int, Payload, int(Payload)) :- > - integer(Payload). > - pack(bool, Payload, bool(Payload)) :- > - ( Payload == true ; Payload == false ). > - > - lit(Env, quote(Words), quote(effect(In, Out))) :- > - infer(Env, Words, effect(In, Out)). > ``` ```prolog append([], Ys, Ys). append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs). word(kernel, dup, [A|S] -- [A, A|S], [], true). word(kernel, drop, [_|S] -- S, [], true). word(kernel, swap, [A, B|S] -- [B, A|S], [], true). word(kernel, over, [A, B|S] -- [B, A, B|S], [], true). word(kernel, add, [A::T, B::T|S] -- [C::T|S], [requires(numeric, T)], C is B + A). word(kernel, sub, [A::T, B::T|S] -- [C::T|S], [requires(numeric, T)], C is B - A). word(kernel, mul, [A::T, B::T|S] -- [C::T|S], [requires(numeric, T)], C is B * A). word(kernel, eq, [A::T, B::T|S] -- [Bool::bool|S], [requires(equatable, T)], (A == B -> Bool = true ; Bool = false)). word(kernel, lt, [A::T, B::T|S] -- [Bool::bool|S], [requires(numeric, T)], (B < A -> Bool = true ; Bool = false)). word(kernel, gt, [A::T, B::T|S] -- [Bool::bool|S], [requires(numeric, T)], (B > A -> Bool = true ; Bool = false)). find(Env0, Word, InOut, Constraints, Goal) :- nonvar(Env0), word(Env0, Word, StoredInOut, StoredConstraints, StoredGoal), copy_term(word(Word, StoredInOut, StoredConstraints, StoredGoal), word(Word, InOut, Constraints, Goal)). ``` Fixed words project through primitive rows. ```prolog apply(Env, Word, Stack0, Stack) :- find(Env, Word, InPattern -- OutPattern, Constraints, Goal), bind(InPattern, Stack0), holds(Constraints), call(Goal), build(OutPattern, Stack). infer(Env, Words, scheme(Constraints, effect(In, Out))) :- infer(Env, Words, effect(In, Out), Constraints, []). infer(_, [], effect(Stack, Stack), Constraints, Constraints). infer(Env, [Word|Words], effect(Stack0, Stack), Constraints0, Constraints) :- infer1(Env, Word, effect(Stack0, Stack1), Constraints0, Constraints1), infer(Env, Words, effect(Stack1, Stack), Constraints1, Constraints). infer1(Env, push(Value), effect(Stack, [Type|Stack]), Constraints, Constraints) :- !, lit(Env, Value, Type). infer1(_Env, call, effect([quote(Scheme)|Stack0], Stack), Constraints0, Constraints) :- !, copy_term(Scheme, scheme(NewConstraints, effect(Stack0, Stack))), append(NewConstraints, Constraints, Constraints0). infer1(Env, Word, effect(Stack0, Stack), Constraints0, Constraints) :- find(Env, Word, InPattern -- OutPattern, NewConstraints, _Goal), types(InPattern, Stack0), types(OutPattern, Stack), append(NewConstraints, Constraints, Constraints0). unpack(int, int(Int), Int) :- integer(Int), !. unpack(bool, bool(Bool), Bool) :- ( Bool == true ; Bool == false ), !. pack(int, Payload, int(Payload)) :- integer(Payload), !. pack(bool, Payload, bool(Payload)) :- ( Payload == true ; Payload == false ), !. lit(Env, quote(Words), quote(Scheme)) :- infer(Env, Words, Scheme). supports(int, numeric). supports(int, equatable). supports(bool, equatable). holds([]). holds([requires(Name, Type)|Constraints]) :- nonvar(Type), supports(Type, Name), holds(Constraints). ``` [[11_lesson|Prev]] | [[13_lesson|Next]]