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