Why not implicit parameters?

[sand-witch]

No, I mean module level for implicit params, my other examples are just more local.

P.S. I will definitely accept partial type signatures for module level private functions, if that’s acceptable by the project’s code style.

[tomjaguarpaw]

OK, so to be clear, I’m specifically interested in examples of things you would use at the same level as you’re suggesting to use implicit params. So, so far we have

• primitives: they exist at module top level but we don’t normally expose them in APIs
• partial type signatures

Do any other examples come to mind?

[Ambrose]

I think there’s a lot of potential in implicit Proxys to guide inference and otherwise do cool things in eDSLs GitHub - ramirez7/icfp-2023-inference-tricks

[lortabac]

@sand-witch

Not quite true. ?symbol :: T is indeed just a Symbol, but you can use IP type class with locally defined dummy data tags

Nice trick! I’ve been experimenting with something similar recently. But that’s not how the ImplicitParams extension is meant to be used. The GHC manual doesn’t talk about this nor I’ve seen it suggested anywhere. In fact until yesterday I thought I was the only one who used this technique.

@sand-witch

Implicit parameters are implemented by piggybacking on type classes, which have been designed for static, global resolution.

Wrong! See the story around withDict and co. There is a lot of work aside implicit params that is done in GHC to resolve type classes with the right scoping

I think I was misunderstood here. I’m not saying that local constraints are not possible in GHC. I’m saying that type classes have been originally designed with global resolution in mind.

Implicit parameters and WithDict introduce different mechanisms but they still look like afterthoughts to me. The implementation of IP relies on ad-hoc checks (see isIPLikePred), the semantics of WithDict are unclear and undocumented.

ghci> class GivenInt where giveInt :: Int
ghci> instance GivenInt where giveInt = 42

ghci> withDict @GivenInt 1 giveInt 
1

ghci> withDict @GivenInt 1 $ withDict @GivenInt 2 giveInt
1

ghci> withDict @(IP "int" Int) 1 $ ip @"int"
1

ghci> withDict @(IP "int" Int) 1 $ withDict @(IP "int" Int) 2 $ ip @"int"
2

In these examples withDict overrides the global GivenInt instance, but the nested withDict call doesn’t override the outer one.
However when applying withDict to IP the innermost instance wins.

This can only be discovered by trial and error. It isn’t documented anywhere, not even in the GHC code base as far as I know (correct me if I’m wrong).

Ideally I would like to see:

• Well-defined and documented semantics.
• A clear difference between global constraints, local constraints (meant to be set with WithDict) and implicit parameters. I don’t know, maybe a kind-level distinction à la TYPE :: RuntimeRep -> Type.

Until then, I agree with you that implicit parameters are not a good idea in a user-facing API. They should only be use internally and only if you know their limitations and quirks.

Edit:
Upon reflection, WithDict's behavior in my example is a bug. The fact that it’s allowed to override a statically-defined instance breaks global coherence. I’ll open a ticket on the GHC bug tracker.