[Haskell-cafe] lifting restrictions on defining instances
wren ng thornton
wren at freegeek.org
Fri Jul 24 16:47:09 EDT 2009
David Menendez wrote:
> wren ng thornton wrote:
>> John Lask wrote:
>>> Can anyone explain the theoretical reason for this limitation, ie other
>>> than it is a syntactical restriction, what would it take to lift this
>>> restriction ?
>> There are a couple of theoretical concerns, mainly that full type-level
>> lambdas can lead down a rocky path (though simple combinators like `flip`
>> and `const` are fine, and that's all we'd need for most cases). But by and
>> large it's just a syntactic restriction.
> I wouldn't say it's "just" a syntactic restriction. I'm pretty sure
> unrestricted type lambdas are incompatible with Haskell's class
> system. Otherwise, you might end up with Functor instances for /\b.
> (a,b) and /\a. (a,b), at which point fmap (+1) (1,2) is ambiguous.
This is essentially the same problem as arises with overlapping
instances. It is a new version of that problem since it introduces new
places for overlapping (by highlighting the fact that instances on a
*->* kind are actually instances on type-level lambdas), but the problem
isn't exactly a new one. A tweak of the overlap detector should be able
to catch these too; eta expand and check for overlap of the type-level
terms. The definition of "overlap" is somewhat different since it must
respect abstraction, but it's not too much different than the current
It is still possible to use type signatures to clear things up, albeit
much uglier than usual. If we were to head down the road of type-level
lambdas then we would want some mechanism for making it easier to deal
with bifunctors like (,) and similar issues. The easiest thing, perhaps,
would be to expose some of the explicit type passing that happens in the
System F core, though we'd want to massage the dictionary-passing so
that we could say things like (fmap @A) to mean the fmap of the instance
So yes, implementing type-level lambdas is more than just changing the
parser (so more than "just" syntax), but provided the right restrictions
on what type-level lambdas are acceptable I don't think there are any
substantial theoretical issues (so I'd say it's just syntax, rather than
theoretical concerns). And these restrictions are the obvious ones,
mainly blocking recursion to prevent the compiler from hanging or
generating infinite types.
 In System F the capital-lambda binder is used for the term-level
abstraction of passing type representations. So for example we have,
id :: forall a. a -> a
id = /\a. \(x::a). x
Thus, the forall keyword is serving as the type-level abstraction.
Perhaps this is suboptimal syntax, but it is the standard. We could, of
course, have both a term-level /\ and a type-level /\ where the latter
is the type of the former (since the namespaces are separate) though
that's also dubious. Capital-pi is the canonical type-level abstraction,
though that evokes the idea of dependent types which are much more complex.
More information about the Haskell-Cafe