Calling a function within a pattern synonym

Question

I'm implementing some functionality on top of a zipper where the hole type is existentially quantified, i.e. I have something like this:

data Zipper (c :: Type -> Constraint) ... =
  forall hole. (c hole, ...) =>
    Zipper hole ...

where dots denote implementation details which I think are unrelated to my question. Consider now some data type:

data Tree = Fork Tree Tree | Leaf Int

What I would like to have is an ability to inspect my position in the tree. In case of simple recursion the standard way to achieve this is pattern matching:

case hole of
  Fork _ _ -> doSomething
  Leaf _   -> doSomethingElse

However, the type of hole is existentially quantified, so simple pattern matching won't do. The idea I had is to use a type class

class WhereAmI p a where
    position :: a -> p a

data Position :: Type -> Type where
    C_Leaf :: Position Tree
    C_Fork :: Position Tree
    -- possibly more constructors if we're traversing
    -- multiple data structures

Then I can do stuff like

f :: Zipper (WhereAmI Position) Tree -> Int
f (Zipper hole _) = case position hole of
  C_Leaf -> let (Leaf x) = hole in x
  otherwise -> ...

What I would like, however, is to replace C_Leaf with something like at @"Leaf" (i.e. use the original constructor names) using some magic like this

class WhereAmI' p (a :: Symbol) where
  position' :: Proxy a -> p

instance WhereAmI' (Position Tree) "Leaf" where
  position' _ = C_Leaf

instance WhereAmI' (Position Tree) "Fork" where
  position' _ = C_Fork

at :: forall a p. WhereAmI' p a => p
at = position (Proxy :: Proxy a)

This even works except that I can't use at as a pattern and I if I try to make it a pattern, GHC complains about a parse error in pattern...

Is there some clever way to achieve what I'm trying to describe here?

You've left an awful lot out. I know you consider some of this irrelevant, but it means (for example) that I can't actually try to compile your code, or add to it, because a bunch of it is missing. I can't even get a good sense of what your Zipper is really supposed to mean. — dfeuer
@dfeuer Good point. Would a link to actual code help? And by zipper I mean a zipper data structure originally described by Huet. — T. Westerhout
A link would help; a self-contained piece of code would be better. I'm familiar with Huet's zippers, but it's not at all obvious how they relate to the zipper structure you're building here. — dfeuer
"... except that I can't use at as a pattern and if I try to make it a pattern, GHC complains about a parse error in pattern..." Did you know that pattern synonyms are supposed to be Capitalized? — luqui
There's library called first-class-patterns which allows to treat patterns as values: hackage.haskell.org/package/first-class-patterns You could try to explore, whether it's possible to achieve your goal with this library. — Shersh

DarthFennec DarthFennec · Accepted Answer · 2018-07-20T20:00:47

As far as I can tell, this isn't really possible. There's no way to return a pattern from a function for use in a match, and because of the way GADTs are refined (I think), it doesn't appear to be possible to do anything more complex than just a direct pattern match. For example, one of my failed attempts:

instance Eq (Position a) where
  C_Leaf == C_Leaf = True
  C_Fork == C_Fork = True
  _ == _ = False

pattern At x = ((\y -> at x == y) -> True)

This should allow you to write case position hole of At @"Leaf" -> ..., but it doesn't typecheck, presumably because of the type refinement process. To clarify:

C_Leaf -> ...                -- This works
((== C_Leaf) -> True) -> ... -- This doesn't work
y | y == C_Leaf -> ...       -- This doesn't work

The error I get for the latter two is Couldn't match expected type ‘Tree’ with actual type ‘hole’. I don't actually know for sure why this happens, but my current theory is that the expression is too complex for the type refinement to "take" properly: as far as the compiler is concerned, there's no reason to expect == to always return False when hole is the wrong type (even though we know that never happens). So it's not allowed.

I have to wonder, why do you believe using at @"Leaf" would be preferable to using C_Leaf? It's not as if you're really "using the original constructor names" in one version any more than in the other: they both use the original names, with some extra characters tacked on. I suppose in the former case you could allow passing in an arbitrary constructor symbol to match against, but that kind of thing appears to be disallowed in general, so you couldn't do that anyway. From what I can tell, you don't actually gain anything with the symbol approach.

Honestly, if your hole type is going to be restricted to the constructors supported by Position anyway, I don't really see the point in making it existential to begin with. It would be much more simple to create a sum type of all the types the zipper might contain, and pass that as a type parameter. But I don't know your use case very well, so I might be wrong.

If you really want to, I suppose you could probably use Template Haskell to do what you're going for. That would allow for something like:

$(at "Leaf") -> ...

Assuming you wrote the appropriate TH function, this would just be converted to C_Leaf -> ... at compile time, which would compile without issue.

Calling a function within a pattern synonym

2 Answers