Why can't an ImplicitParam be bound by a lambda?

#1

I don’t understand whether an ImplictParam can be bound by a lambda (I can’t make it work) and if not, why not. Here’s an attempt, and the failure message. The User’s Guide suggests (by omission) that it’s not possible, but I don’t understand why it’s not possible. Is there some technical restriction?

{-# LANGUAGE ImplicitParams #-}

implicitDouble :: (?imp :: Int) => Int
implicitDouble = 2 * ?imp

double :: Int -> Int
double exp = let ?imp = exp in implicitDouble
-- ghci> double 5
-- 10

doubleLambda :: Int -> Int
doubleLambda (?imp) = implicitDouble
-- test26.hs:12:15: error: Expression syntax in pattern: ?imp
--    |
-- 12 | doubleLambda (?imp) = implicitDouble
--    |               ^^^^

A group of implicit-parameter bindings may occur anywhere a normal group of Haskell bindings can occur, except at top level. That is, they can occur in a let (including in a list comprehension, or do-notation, or pattern guards), or a where clause. Note the following points:

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/implicit_parameters.html

#2

The docs are saying implicit parameter bindings are a form of bindings with the shape ?<var> = <expr> and that these can occur at any place where normal binding groups occur, except for the top level. And it elaborates that such binding groups are then either let or where blocks.

You seem to be suggesting that ?<var> should be a pattern, which is not quite the same thing. For example you can write patterns nested inside other patterns:

foo (x, y, ?z) = ...

So I don’t think the user guide merely “suggests (by ommision)”; it really does define precisely where you can bind implicit variables.

That said, I don’t know if there is a technical reason that ?<var> = <expr> as a binding was chosen over ?<var> as a pattern. It may just be that the former was easier to implement.

2 Likes
#3

I see, I think I understand. It’s as though there is a new form for binding implicit parameters. It could have been let? x = ..., but it’s more convenient to steal syntax and write it as let ?x = ... (plus it plays well with where sugar).

Yes, I think that’s the right way of putting it. Why is this not so?

Yes, absolutely, but if I wrote a document precisely defining an operation 1 %^ 2 to be 2 + 1 people might wonder if meant to extend the operation to a wider variety of cases, and it would help if I explained further in the docs. Binding explicit parameters as patterns seems such a natural thing to want that it would be helpful if the docs explicitly mentioned whether or not it’s possible (and if not then explained why not).

#4

If implicit params could be used as patterns then you could define a function like this:

f :: (?x :: Int) => Int -> Int
f (?x) = ?x

What would be the result of calling it with the implicit param bound?

let ?x = 3
in f 4
-- 3 or 4?
1 Like
#5

I’d expect it to behave the same as:

f :: (?x :: Int) => Int -> Int
f y = let ?x = y in ?x

So let ?x = 3 in f 4 should evaluate to 4.

Even if some people disagree, I don’t think this is a fundamental problem. This is just a choice that has to be made by someone.

1 Like
#6

Yes, agreed. I think it’s “just” shadowing.

#7

Ah I see, so you’re trying to use identifiers that look like implicit params without having the semantics of them. Reminds me of the MagicHash extension.

#8

I do also want the semantics of them, I just expect any locally-bound implicit parameter to shadow the one bound by the type signature.

#9

Wouldn’t it always be shadowed though? Using my example from earlier:

f :: (?x :: Int) => Int -> Int
f (?x) = ?x

How would you get the value of ?x from the constraint (rather than the argument)?

#10

Yes, in that case it would always be shadowed. But I don’t want to do that. I want to do this:

1 Like
#11

I agree with @jaror that there doesn’t seem to be a fundamental reason one couldn’t do this, it simply isn’t part of the design or implementation. I don’t know for certain why not, but one possible technical reason is that it would lead to patterns introducing constraints that may be needed to typecheck subsequent patterns (e.g. consider f (?x) (blah -> True) = ... where blah :: (?x :: Int) => ...). With our current understanding of constraints and GADTs this isn’t particularly worrisome, but implicit parameters were introduced in the early 2000s, prior to the OutsideIn(X) paper which (mostly) nailed down how GHC does this kind of type inference only in about 2010.

2 Likes