On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald <carter.schonw...@gmail.com> wrote: > Peripherally, this also brings up the notion of type equality, and I'm a bit > fuzzy about how big a chasm there is between what that means in Haskell 2010 > vs more bleeding edge styles, or am I pointing at a shadows?
Generally speaking, notions of "equality" are a major source of complication in any dependently typed theory. The issue isn't coming up with a story that works, but rather choosing between a number of different stories each of which works in slightly different ways. This problem of "equality" is the bulk of why I think it'd be good to postpone the GADT (and TypeFamily) debate. One Haskell-specific example of why defining equality is hard is when we try to handle both the "equalities" induced by dependent case-analysis as well as the "equalities" induced by newtype definitions. Though we use the same word for them, they're two entirely different notions of "equality". However, since they both exist, we must have some story for how these two notions interact with one another (including possibly "not at all"). The new role-typing stuff is one approach to handling this, but many people feel it's overly complicated or otherwise not quite the right way forward. If we add GADTs to the report, then we also need to define how to type check dependent case-analysis, which seems to require introducing type equality, which in turn requires specifying how the semantic notion of type equality interacts with the operational notion of representation equality introduced by newtypes, which is still imo an open area of research. If we can come up with some story that lets us make progress towards eventually including GADTs (and TypeFamilies) while avoiding the equality tarpit, I'm all for it. I'd just really rather avoid the tarpit until we have other easier things squared away. ... One possible way forward may be to introduce the syntax for (~) constraints and defining them merely as "delayed unification constraints". This would require including unification in the report, but may be doable in a way that allows non-unification-based implementations as well. The reason I bring this possibility up now is that it helps handle some other situations where we don't even have GADTs or TypeFamilies. In particular, when FlexibleInstances is enabled it allows for non-linear use of type variables in the instance head. However, this is often not what we mean since "instance Foo (Bar i i)" means that the two parameters to Bar must be unified *prior* to selecting that instance; which often leads to type inference issues since we can't resolve the instance eagerly enough. Whereas, often times what is actually desired is "instance (i ~ j) => Foo (Bar i j)" which causes us to select the instance immediately if the type constructor is Bar, and then *after* committing to the instance we then try to unify the two parameters. Thus, adding delayed unification constraints would be helpful for adding (something like) FlexibleInstances to the report. Of course, "delayed unification constraints" don't have any sort of evidence associated with them like the dependent case-analysis equalities do; so, again, we'd want to make sure to phrase things in such a way that we don't prematurely commit to more than we intend. -- Live well, ~wren _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime