Typeclass Evidence Scope

So lately I’ve found myself reifying a bunch of typeclasses from variables in my code base. The basic pattern looking a little like the following (using the constraints package from hackage):

example0 x = case evidence x of
  Dict -> ... -- use typeclass evidence stored in Dict

Now I dislike the amount of nesting I get from this. Even for a single pattern match, I don’t actually case split so I don’t need the nesting at all. Some functions require three uses of evidence and thus three pattern matches (or one big one, still ugly) . I’ve found that I can get straight-line code via monadic binds:

example1 x y z = runIdentity do
  Dict <- pure $ evidence x
  Dict <- pure $ evidence y
  Dict <- pure $ evidence z
  pure $ ... -- use typeclass evidence from x, y and z Dict.

This is better, but it has me use the Identity monad which clutters the code a bit. Ideally, I would write something using just some let bindings:

example2 x y z = do
  let !Dict = evidence x
  let !Dict = evidence y
  let !Dict = evidence z
  ... -- doesn't compile... Dict of x, y and z not in scope here :( 

This doesn’t compile though, as the typeclass instances are not in scope at the bottom. :frowning:

What I don’t understand is why it doesn’t work. My understanding was that bang patterns forced the value, so I would expect the resulting expression be a nesting of case expressions that I originally wrote. Perhaps it uses the default pattern internally, thus not scoping it?

Second, I’m interested to know if there is any alternative approach that is close to example2 in spirit.

Thanks in advance! :slight_smile:

This happens to me a lot too (although not with Dict specifically) but I generally work in an effect system’s Eff monad, so I’m generally not introducing a monad just for this purpose.

It seems at least plausible that in do notation

let !pat = exp
...

could desugar to

case exp of pat -> ...

One thing to tackle would be to ensure that the let is not actually part of a recursive group, that is, it really is only binding that one pattern.

So I did some testing, the translation of

let !pat = exp
...

Where pat does not bind any variables (and is irrefutable) is desugared to:

case exp of _ -> ...

That is, the pattern is stored as a DEFAULT in GHC Core and thus does not reveal the typeclass instance. The same happens for type variables (which is another stumbling block of mine). So the following also doesn’t work:

let SNat @n = exp
... -- Type variable 'n' is not in scope

Of course, this one requires the TypeAbstraction language extension. Still, I would have liked this one to work for similar reasons… I wonder if this could be a language extension or something? Do you know if anyone looked into this, or if there is any reason not to want this behaviour?

You can use QualifiedDo to save yourself from using Identity.

Ah yeah, I didn’t consider this. It’s a little bit odd, but you can definitely abuse this to get rid of all the monadic stuff. Here’s an identity bind:

module Id ((>>=)) where
(>>=) :: a -> (a -> b) -> b
(>>=) x f = f x

With this, you can write the following:

import Id qualified

example x y z = Id.do
  Dict <- evidence x
  Dict <- evidence y
  Dict <- evidence z
  ... -- Typeclasses are available here!

Notice how we don’t even need any calls to pure! :slight_smile: I will say that I think that a simple let !pat = exp would still be preferable, but it is a neat trick.

BTW, would it make sense to try and make an RFC for the let-style bindings? Not sure how this process works, but I would be interested to drive this. Of course, I have no clue if I’m not missing some reason why this is not the default behaviour, but I guess this is why it is an RFC first haha :see_no_evil_monkey:

Someone pointed out to me another possibility, which is to use pattern guards:

    example1 x y z                                                                                                                                                                                                                             
       | Dict <- evidence x                                                                                                                                                                                                                    
       , Dict <- evidence y                                                                                                                                                                                                                    
       , Dict <- evidence z                                                                                                                                                                                                                    
       = ...                                                                                                                                                                                                                                   

If you’re not doing a top-level binding I guess you can use MultiWayIf.

I’m not sure if there’s “a reason”. You can always make a GHC proposal and then you might find out. Personally I’m not sure it makes sense to add a special case for single strict let bindings of an irrefutable pattern, but maybe it does.