[Haskell-cafe] lifting restrictions on defining instances

[wren ng thornton]

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 
version.

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[1], 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 
for A.

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.



[1] 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.

-- 
Live well,
~wren