Closed ivenmarquardt closed 2 years ago
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.
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:
There are three
a => b
types in the above annotations but neithera
norb
are the same. There is no connection between them at all but they are all distinct. The desiredYoneda.map
function looks like this, of course: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 theYoneda
type itself:There is the higher-rank type we need so desparately:
(^b. (a => b) => f<b>)
. Whenever the validator runs across aYoneda
type annotation it looks up the corresponding type in the globaladtDict
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.