tag:blogger.com,1999:blog-10770855.post8007269235891659481..comments2024-03-28T03:20:57.393-04:00Comments on The Little Calculist: Unordered multi-arity bindersDave Hermanhttp://www.blogger.com/profile/00405190527081772997noreply@blogger.comBlogger9125tag:blogger.com,1999:blog-10770855.post-47202649488289443732009-06-23T00:49:34.214-04:002009-06-23T00:49:34.214-04:00I was going to say exactly what Steck did. Is ther...I was going to say exactly what Steck did. Is there a reason that can't work?Douglas McCleanhttps://www.blogger.com/profile/06662331850663558712noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-60102394775677100842008-10-22T12:46:00.000-04:002008-10-22T12:46:00.000-04:00I haven't read the references mentioned in other c...I haven't read the references mentioned in other comments, but <BR/>normalization sounds right to me.<BR/><BR/>One way to do this is to sort the binders according to the order of their first appearance in the type being quantified. Then you just check the two types for alpha-equivalence.Paul Stecklerhttps://www.blogger.com/profile/13416750891822431224noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-71640506806677920512008-10-16T11:38:00.000-04:002008-10-16T11:38:00.000-04:00SPJ and a bunch of coauthors have a JFP paper abou...SPJ and a bunch of coauthors have a JFP paper about type inference (including higher-rank types) in GHC as of 2006, <A HREF="http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm" REL="nofollow">over here</A>. <BR/><BR/>I dunno if they still do the same thing, since GHC's typechecker changes pretty often. :-)Neel Krishnaswamihttps://www.blogger.com/profile/06853898957395028131noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-44244570569762749482008-10-16T11:15:00.000-04:002008-10-16T11:15:00.000-04:00If I understand you correctly, this check is part ...If I understand you correctly, this check is part of checking whether one type (scheme) is an instance of another. In your example, the type checker should try (successfully) to unify the ground term to(a,to(b,b)) with the non-ground term to(A,to(B,B)). In the more general setting of "Putting type annotations to work" (Section 5), Odersky and Läufer relate the problem of instantiation checking to unification under a mixed prefix.單中杰https://www.blogger.com/profile/14754929367418830739noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-74087232328545399642008-10-16T10:51:00.000-04:002008-10-16T10:51:00.000-04:00It's easy. You just normalise the universal types ...It's easy. You just normalise the universal types as described in Daan Leijen's ICFP paper on HMF (ICFP 2008).Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-10770855.post-23004132394808999692008-10-15T21:11:00.000-04:002008-10-15T21:11:00.000-04:00One place to start might be (I don't know if it co...One place to start might be (I don't know if it contains the answer, it has been a while since I read this paper...)<BR/><BR/>http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.8924<BR/><BR/>and maybe some of the citations.<BR/><BR/>Also, scanning section 12 of<BR/>http://www.haskell.org/haskellwiki/Research_papers/Type_systems<BR/><BR/>some of the papers look promising.Anonymoushttps://www.blogger.com/profile/02471658774243780902noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-42700563279519211892008-10-15T16:48:00.000-04:002008-10-15T16:48:00.000-04:00Using de Bruijn indexes as type variables wouldn't...<I>Using de Bruijn indexes as type variables wouldn't solve this?</I><BR/><BR/>Nope-- try it! What do you pick for the index of each variable?Dave Hermanhttps://www.blogger.com/profile/00405190527081772997noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-37870849012638103702008-10-15T16:42:00.001-04:002008-10-15T16:42:00.001-04:00Using de Bruijn indexes as type variables wouldn't...Using de Bruijn indexes as type variables wouldn't solve this?Daniel Yokomizohttps://www.blogger.com/profile/12528969103424062002noreply@blogger.comtag:blogger.com,1999:blog-10770855.post-55338953979710377302008-10-15T16:42:00.000-04:002008-10-15T16:42:00.000-04:00This comment has been removed by the author.Daniel Yokomizohttps://www.blogger.com/profile/12528969103424062002noreply@blogger.com