kongware/scriptum

Higher-rank types seem to be not always type safe

ivenmarquardt opened this issue · 1 comments

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.

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.