missing post-facto type inference

GoogleCodeExporter commented 9 years ago

run
<http://svn.berlios.de/viewcvs/al4nin/trunk/found-bugs/issue12-Cat.omg?rev=388&v
iew=markup>
in Omega 1.4.2

on the prompt one can examine:

*** Checking: n
*** expected type: m
***    refinement: (_d,_e), (_f,Prod *0), (_g,{blow (1+_c)t _h}), (_i,Cat), 
                   (_j,_h), (_k,{blow (1+_c)t _h}), (_l,_c), 
***   assumptions: Nat' _c, 
***      theorems: 
check> ZZ
ZZ :: Cat {blow (1+_c)t _h} _h
check> r
r :: Thrist Cat _h _e
check> :q

**** Near line: 313 column: 23
(V) different types
   _c   !=   0t
(luf,0t)

Looks like Omega does not do post-facto type inference. The idea is:
if the case expression

        where compiledRest = case check n of
                     Z -> check (compile r)

enters the first arm, we can retrospectively (post-facto) say that
n is equal 0v, so their types must be the same too:

Equal _c 0t  (in the second check> loop's context).

This type equality should allow to evaluate thus:

Cat {blow (1+_c)t _h} _h --> Cat {blow 1t _h} _h -->
Cat [freshXX; _h]sh _h

(I am not completely sure why this is needed at all)

If this kind of type inference is feasible (algorithmically,
complexity-wise), I do not know. Anyway I have written a text
on it in the context of multi-dispatch languages, and it seems
to be a sound concept.

Original issue reported on code.google.com by ggr...@gmail.com on 22 Jun 2007 at 2:41

GoogleCodeExporter commented 9 years ago

looks like this problem can be worked around by
lifting the pattern match from the "case n of"
into the top-level pattern and duplicating the function for (PopN (S Z))
and (PopN (S (S n)).

It is demonstrated here:

http://svn.berlios.de/viewcvs/al4nin/trunk/purgatory/Cat.omg?rev=389&view=markup

Original comment by ggr...@gmail.com on 23 Jun 2007 at 2:55

GoogleCodeExporter commented 9 years ago

regarding the soundness of this inference, it must be clear that the obtained 
information must be propagated in 
both directions. I think that needs quite a bit of pondering first, and may 
produce different function signatures 
(than e.g. Haskell's algorithm).

Original comment by ggr...@gmail.com on 9 Dec 2007 at 8:48

GoogleCodeExporter commented 9 years ago

seems like Haskell monads already employ a similar concept:

http://reddit.com/r/programming/info/695es/comments/

Original comment by ggr...@gmail.com on 20 Feb 2008 at 11:38

GoogleCodeExporter commented 9 years ago

Maybe this could be added as an extra heuristic to the two existing ones on 
page 57 of cklin's presentation 
<http://865974842905851078-a-1802744773732722657-s-sites.googlegroups.com/site/c
hklin/research/dissertation-slides.pdf?attachauth=ANoY7cp-ezgu89vUrkkwthSS_9Bof8
dAxypK5s_D6TniQNZVeho33aFxtvRRpPjQblOmKnlXwt1S69CAMjqEML-8g4IeMt-eFilpLPqnKUcznB
LrVaubrytH_nFO0HJNFfaxH3HhmqLpbmQDNC9iQrAGwLXGPoKWETiPvUTaUqE6FjwUQEP0bj7a-8sO8R
ajC38ZTajU1eFAS-_bTN6vP5ILlU0LYgLXcw%3D%3D&attredirects=0> ?

Is there any relation at all? Can it improve inference? Do the two existing 
heuristics already cover post-facto?

Original comment by ggr...@gmail.com on 24 Nov 2010 at 4:48

ggreif / omega

missing post-facto type inference #12