The GADT debate

[wren romano]

On Sun, May 8, 2016 at 1:38 AM, Carter Schonwald
<carter.schonwald at 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