kongware/scriptum

Allow nested functions to share types

ivenmarquardt opened this issue · 2 comments

#356 only partly causes the problem with incorporating ADTs/TCs into the type validator. The major problem is inherent to the current design of the validator: There is no type inference whatsoever and hence the types of nested functions are disconnected from one another:

Yoneda.map = fun(
  f => tx => Yoneda(fun(
    g => tx.run(fun(
      x => g(f(x)),
      "a => b")),
    "(a => b) => f<b>")),
  "(a => b) => Yoneda<f, a> => Yoneda<f, b>");

There are three a => b types in the above annotations but neither a nor b are the same. There is no connection between them at all but they are all distinct. The desired Yoneda.map function looks like this, of course:

Yoneda.map = fun(
  f => tx => Yoneda(
    g => tx.run(
      x => g(f(x)))),
  "(a => b) => Yoneda<f, a> => Yoneda<f, b>");

But how get we from (a => b) => Yoneda<f, a> of the outer function to (a => b) => f<b> of the inner one without an explicit annotation? The answer lies in the Yoneda type itself:

const Yoneda = type1("(^b. (a => b) => f<b>) => Yoneda<f, a>");

There is the higher-rank type we need so desparately: (^b. (a => b) => f<b>). Whenever the validator runs across a Yoneda type annotation it looks up the corresponding type in the global adtDict type directory and there we go.

That is pretty much it. I cannot find an excuse why this hasn't occurd to me much earlier. Once again it is so obvious in hindsight. I appologize for my rambling and all the confusion.

The revised implementation passed the Yoneda.map test, a.k.a. dynamic loop fusion.

The next pending test is the same functor based loop fusion but this time with Coyonda, which is even harder to type, because it relies on higher-kinded and higher-rank types. If you wonder: No, scriptum doesn't support existential quantification, unfortunately. It is not possible with a type validator but you need a proper type checker with inference.

Done.