kongware / scriptum

Functional Programming Unorthodoxly Adjusted to Client-/Server-side Javascript
MIT License
383 stars 21 forks source link

Unification doesn't work correctly with higher-rank types #348

Closed ivenmarquardt closed 3 years ago

ivenmarquardt commented 3 years ago

The following valid program doesn't type check:

const Coyoneda_ = type1("(^r. (^b. (b => a) => f<b> => r) => r) => Coyoneda<f, a>");

const Coyoneda = fun(f => tx => Coyoneda_(fun(
  k => k(f) (tx),
  "((b => a) => f<b> => r) => r")),
  "(b => a) => f<b> => Coyoneda<f, a>");

Coyoneda.lift = Coyoneda(id);

Coyoneda.lower = fun(
  ({map}) => tx => tx.run(fun(
    f => ty => map(f) (ty),
    "(b => a) => f<b> => f<a>")),
  "Functor<f> => Coyoneda<f, a> => f<b>");

Coyoneda.lower(A.Functor) (Coyoneda.lift([1,2,3])); // type error
ivenmarquardt commented 3 years ago

The problem is caused by an invalid substitution of partially applied type constructors:

((b => a) => f<b> => r) => r

// is substituted to

((b => Number) => [] => r) => r
//                ^^
//          instead of [b]

The type validator restores f's arity in Coyoneda<f, a> correctly with 1, but somewhere along the way this information is lost.

ivenmarquardt commented 3 years ago

see #350