I read the news today, ... http://lambda-the-ultimate.org/node/feed
> Conor McBride wrote: > > Sebastian Hanowski wrote: > > > > You mean like the 'where' for Epigram 2 you introduced when you > > blogged about views for equality? > > > > In fact, there's a generalisation of this which I quite fancy trying > out. For a long time, James McKinna has wanted to experiment something > like Dyckhoff's algorithm jacked up to dependent types. I guess that something now would have to be called Djinns Meta. http://permalink.gmane.org/gmane.comp.lang.haskell.general/12747 But since Djinn doesn't support type classes, i can't check your 'faking it' programs with it. Would be interesting how it decides this: Djinn> f ? ((p -> q) -> p) -> p -- f cannot be realized. http://lambda-the-ultimate.org/node/view/1178 is seeing lively comments. There's already the question been raised, wether this kind of program inference could be used to build isomorphisms between given types ... Best Regards, Sebastian
