0

Consider the Arrows, Domains and CoDomain type-families defined in the agda codebase.

Obvious to the programmer, it holds that Arrows (Domains func) (CoDomain func) ~ func. But I can't get curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined :: func through GHC's type-checker. That's because GHC isn't smart enough to infer that the combination of Domains and CoDomain is injective. Is there a way to teach GHC nonetheless? I'd imagine some case split over the IsBase predicate.

Sebastian Graf
  • 3,602
  • 3
  • 27
  • 38

1 Answers1

1

Would it be better for you to change Currying to be indexed by func?

class Currying func where
  curries :: (Products (Domains func) -> CoDomain func) -> func
  uncurries :: func -> Products (Domains func) -> CoDomain func

instance Currying b => Currying (a -> b) where
  curries f a = curries (f . (,) a)
  uncurries f (a, as) = uncurries (f a) as

instance {-# OVERLAPPABLE #-} (IsBase b ~ 'True) => Currying b where
  curries f = f ()
  uncurries b _ = b

We can also assert axioms in this way, though I'm not even sure this one is safe:

arrowAxiom :: forall func. func :~: Arrows (Domains func) (CoDomain func)
arrowAxiom = unsafeCoerce Refl

The equality can be put in scope by pattern matching on the axiom.

Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • How would I match on the structure of `func` that way? – Sebastian Graf Feb 14 '18 at 17:49
  • I added instances to my answer. – Li-yao Xia Feb 14 '18 at 18:01
  • Ah, thanks. Actually, there's [one more case](https://github.com/sgraf812/datafix/blob/66a5236791c81249c0e5dd8c682d9a3013d2163b/src/Datafix/Utils/TypeLevel.hs#L136) I'd like to optimize for. Is that still possible that way? I imagine that leads to three tiers of overlaps. Anyway, the axiom approach works just fine, too. – Sebastian Graf Feb 14 '18 at 18:04
  • Hmm.. come to think of it, I'm not sure if can really use `Currying func` in my code, because I do stuff like [this](https://github.com/sgraf812/datafix/blob/66a5236791c81249c0e5dd8c682d9a3013d2163b/src/Datafix/Description.hs#L83), where I return non-`Base` types and the selected `Currying` would not [do the right thing here](https://github.com/sgraf812/datafix/blob/66a5236791c81249c0e5dd8c682d9a3013d2163b/src/Datafix/Description.hs#L234) – Sebastian Graf Feb 14 '18 at 18:11
  • For the three-case situation, you can define three instances `(IsBase b ~ 'True) => Currying b`, `(IsBase b ~ 'True) => Currying (a -> b)`, `Currying (a2 -> b) => Currying (a1 -> a2 -> b)`. – Li-yao Xia Feb 14 '18 at 18:25
  • Exactly, but I'm not sure which instance should overlap which. – Sebastian Graf Feb 14 '18 at 18:27
  • 1
    The first two should be `OVERLAPPABLE`. [This chapter of the GHC manual](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#instance-overlap) explains how these pragmas affect the selection algorithm. There are different combinations that also work, but `OVERLAPPABLE` is almost always sufficient in my experience. – Li-yao Xia Feb 14 '18 at 18:32
  • Great. Thank you! – Sebastian Graf Feb 14 '18 at 18:33
  • As for the more general problem, I don't see a good way to extend my approach (having considered 1) indexing `Currying` by the number of arguments to take, 2) matching on the desired result type). I guess it depends on what information is more readily available. The simplest solution with the original class may be to just let the type equality float into the toplevel constraints. – Li-yao Xia Feb 14 '18 at 18:41