Higher-rank types seem to be not always type safe
ivenmarquardt opened this issue · 1 comments
ivenmarquardt commented
Given is
const Coyoneda = type1(
"(^r. (^b. (b => a) => f<b> => r) => r) => Coyoneda<f, a>");
const coyoneda = fun(
f => tx => Coyoneda(k => k(f) (tx)),
"(b => a) => f<b> => Coyoneda<f, a>");
which is fine. However, the following implementation also type validates, although it violates the higher-rank types:
export const coyoneda = fun(
f => tx => Coyoneda(k => k(f) (tx)),
"(Number => Number) => f<Number> => Coyoneda<f, Number>");
and even this type validates:
export const coyoneda = fun(
f => tx => Coyoneda(fun(k => k(f) (tx), "((b => a) => f<b>) => f<a>")),
"(Number => Number) => f<Number> => Coyoneda<f, Number>");
Further investigation is required.
ivenmarquardt commented
The only version raising a higher-rank type error is the following:
export const coyoneda = fun(
f => tx => Coyoneda(fun(k => k(f) (tx), "((Number => Number) => f<Number>) => f<Number>")),
"(Number => Number) => f<Number> => Coyoneda<f, Number>");
As far as I understand it the outer function's type annotation just serves as a type refinement, i.e. it deliberately narrows the type, but it doesn't pose a threat for unsound types.