This blog gives a good example showing the restriction to expressiveness of using row polymorphism for the effect system.
In Links, the same problem happens with some slightly modification.
Consider the following recursive function iter which works well in Links.
links> @set show_quantifiers true;
links> @set show_kinds hide;
links> fun iter(n)(f)(x) {if (n==0) {x} else {iter(n-1)(f)(f(x))}};
iter = fun : forall a::Row,b::Type,c::Row,d::Row.(Int) -a-> ((b) ~c~> b) -d-> (b) ~c~> b
links> iter(2);
fun : ((a) ~b~> a) -> (a) ~b~> a
The iter allows its arrows to have different row variables. Thus, iter(2) can take any impure function. This is because Links uses a trick to enable a restricted form of row polymorphic recursion for curried multi-parameters recursive functions. Approximately, Links forces the iter to be bound with a row polymorphic type forall a:Row,d::Row. (...) -a-> (...) -d-> (...) in the context.
However, if we slightly change the definition of iter to nested function literals, the trick fails.
links> fun myiter() {fun(n) {fun(f) {fun(x) {if (n==0) {x} else {myiter()(n-1)(f)(f(x))}}}}};
myiter = fun : forall a::Row,b::Type.() ~a~> (Int) ~a~> ((b) ~a~> b) ~a~> (b) ~a~> b
links> myiter()(2);
fun : ((a) {}~> a) {}~> (a) {}~> a
Now, iter requires its arrows to use the same row variable! As a result, iter(2) can only take pure functions, which is too restrictive.
Of course, we can fix this problem by writing out the signature of myiter to enable polymorphic recursion.
links> sig myiter : () -> (Int) -> ((b) ~c~> b) -> (b) ~c~> b
...... fun myiter() {fun(n) {fun(f) {fun(x) {if (n==0) {x} else {myiter()(n-1)(f)(f(x))}}}}};
myiter = fun : forall a::Row,b::Row,c::Type,d::Row,e::Row.() -a-> (Int) -b-> ((c) ~d~> c) -e-> (c) ~d~> c
links> myiter()(2);
fun : ((a) ~b~> a) -> (a) ~b~> a
To solve it fundamentally, we could probably either develop better approaches to row polymorphic recursion or add row subtyping, as what are suggested in the blog.
This blog gives a good example showing the restriction to expressiveness of using row polymorphism for the effect system. In Links, the same problem happens with some slightly modification.
Consider the following recursive function
iterwhich works well in Links.The
iterallows its arrows to have different row variables. Thus,iter(2)can take any impure function. This is because Links uses a trick to enable a restricted form of row polymorphic recursion for curried multi-parameters recursive functions. Approximately, Links forces theiterto be bound with a row polymorphic typeforall a:Row,d::Row. (...) -a-> (...) -d-> (...)in the context.However, if we slightly change the definition of
iterto nested function literals, the trick fails.Now,
iterrequires its arrows to use the same row variable! As a result,iter(2)can only take pure functions, which is too restrictive.Of course, we can fix this problem by writing out the signature of
myiterto enable polymorphic recursion.To solve it fundamentally, we could probably either develop better approaches to row polymorphic recursion or add row subtyping, as what are suggested in the blog.