infer loops and SFINAE
Geoffrey Irving
-- |Type infer a function call and cache the results
--
-- * TODO: cache currently infers every nonvoid function call at least
thrice, regardless of recursion. Fix this.
--
-- * TODO: we should tweak this so that only intermediate
(non-fixpoint) types are recorded into a separate map, so that
-- they can be easily rolled back in SFINAE cases /without/ rolling
back complete computations that occurred in the process.
I'm wondering if we ever need to do any rollback at all. Specifically,
1. Augment the ptrie so that we can store type errors in addition to
valid return types.
2. Make cache catch type errors that occur during function body
inference and store them in the ptrie.
Hmm. I suppose the problem is mutual recursion. Consider
f i = if i then g (i-1) else []
g i = i : f (i-1)
If we want to infer f Int, we
1. Start by assuming f Int :: Void
2. Infer the body of f, which involves g Int.
3. Assume g Int :: Void.
4. Infer the body of g to get g Int :: Void since f Int :: Void
5. Complete the inference of the body of f to get f Int :: List Void
At this point, cache completely discards the overload table,
forgetting that g Int :: Void. Going through the loop one more time
produces f Int :: List Int, and all is well.
What we'd like to do is know that our g Int :: Void judgement is
provisional since it depends on the provisional f Int :: Void
judgement. That way, the next time we go to infer g Int, we repeat
the inference since it isn't solidified yet. As an advantage,
nonrecursive functions would only need to be traversed once: they'd
get a provisional Void judgement, but would never refer to it, so
their first evaluation would be marked final. The disadvantage is
having to thread the provisionality bool through all inference
functions.
Do you think that's the right way to go, or is there a cleaner way to
express the fixpoint iteration? Does playing with laziness more than
I give you any extra intuition?
Geoffrey
Geoffrey Irving
Actually, I don't think a provisional bool is enough. I'm not sure
about an explicit counterexample, but consider the implications
(f Int :: Void) and (g Int :: Void) implies (f Int :: Void)
(f Int :: Void) and (g Int :: List Void) implies (f Int :: Void)
(f Int :: Void) and (g Int :: List Int) implies (f Int :: Int)
(f Int :: Void) and (g Int :: Void) implies (g Int :: List Void)
(f Int :: Void) and (g Int :: List Void) implies (g Int :: List Int)
where f calls g calls f. After inferring the body of f once, we still
get f Int :: Void, so the fixpoint iteration would cease. One
solution would be to replace the provisional bool with an entire list
of provisional dependencies, and then make cache iterate on all
provisional dependencies until none of them change. It seems like
there may be a more elegant algorithm, though.
Geoffrey
Dylan Simon
> On Sun, May 22, 2011 at 6:06 PM, Geoffrey Irving <irv...@naml.us> wrote:
> > Currently Infer has the following comment:
> >
> > -- |Type infer a function call and cache the results
> > --
> > -- * TODO: cache currently infers every nonvoid function call at least
> > --
> > -- * TODO: we should tweak this so that only intermediate
> > (non-fixpoint) types are recorded into a separate map, so that
> > -- they can be easily rolled back in SFINAE cases /without/ rolling
> > back complete computations that occurred in the process.
> >
> >
> > 1. Augment the ptrie so that we can store type errors in addition to
> > valid return types.
> > 2. Make cache catch type errors that occur during function body
> > inference and store them in the ptrie.
> >
> >
> > ? ?f i = if i then g (i-1) else []
> > ? ?g i = i : f (i-1)
> >
> > If we want to infer f Int, we
> >
> > 1. Start by assuming f Int :: Void
> > 2. Infer the body of f, which involves g Int.
> > 3. Assume g Int :: Void.
> > 4. Infer the body of g to get g Int :: Void since f Int :: Void
> > 5. Complete the inference of the body of f to get f Int :: List Void
> >
> > At this point, cache completely discards the overload table,
> > produces f Int :: List Int, and all is well.
> >
> > What we'd like to do is know that our g Int :: Void judgement is
> > provisional since it depends on the provisional f Int :: Void
> > the inference since it isn't solidified yet. ?As an advantage,
> > nonrecursive functions would only need to be traversed once: they'd
> > get a provisional Void judgement, but would never refer to it, so
> > having to thread the provisionality bool through all inference
> > functions.
> >
> > Do you think that's the right way to go, or is there a cleaner way to
> > I give you any extra intuition?
>
> Actually, I don't think a provisional bool is enough. I'm not sure
> about an explicit counterexample, but consider the implications
>
> (f Int :: Void) and (g Int :: Void) implies (f Int :: Void)
> (f Int :: Void) and (g Int :: List Void) implies (f Int :: Void)
> (f Int :: Void) and (g Int :: List Int) implies (f Int :: Int)
> (f Int :: Void) and (g Int :: Void) implies (g Int :: List Void)
> (f Int :: Void) and (g Int :: List Void) implies (g Int :: List Int)
>
> where f calls g calls f. After inferring the body of f once, we still
> get f Int :: Void, so the fixpoint iteration would cease. One
> solution would be to replace the provisional bool with an entire list
> of provisional dependencies, and then make cache iterate on all
> provisional dependencies until none of them change. It seems like
> there may be a more elegant algorithm, though.
Does it help to think about the call graph? Something like: Our goal is to
mark every node. We can only mark a node once all of its descendants are
marked. We want to recursively follow along the graph until we reach a leaf
and mark it. Whenever we reach a cycle (with no unmarked descendants) we want
to iterate around it (not recurse) until convergence of all nodes.
Aside from that, there are some possible optimizations.
We don't need to throw away all the information in the ptrie. Right now I
cache on edges the list of possible overloads. This information should always
be valid, and in fact leaves could be converted to singleton lists. (This may
not actually be true. The thing that always trips me up is that
TypeSet.subset used by overload resolution calls back into Infer.apply, and
those dependencies are hard to think about.)
Second, how much can we rely on Void? Clearly some functions really return
Void, but what about the other way around? If we infer that a function
returns a void-free type are we done? If this happens on the first inference,
can we keep the results?