Perhaps this is a stupid question. Here's a quote from the Hasochism paper:
One approach to resolving this issue is to encode lemmas, given by parameterised equations, as Haskell functions. In general, such lemmas may be encoded as functions of type:
∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t
I thought I understood RankNTypes, but I can't make sense of the last part of this proposition. I'm reading it informally as "given a term which requires l ~ r, return that term". I'm sure this interpretation is wrong because it seems to lead to a circularity: we don't know l ~ r until the conclusion of the proof itself, so how can I be expected to provide as an assumption of the proof a term which requires that?
I would have expected an equality proof to have a type more like this:
Natty x1 → ... → Natty xn → l :~: r
Informally, "given a bunch of Nattys, return a proof of the proposition that l and r are equal" (using GHC's Data.Type.Equality). This makes far more sense to me, and seems to align with what you'd say in other dependently typed systems. I'm guessing it's equivalent to the version in the paper, but I'm struggling to mentally square away the two versions.
In short, I'm confused. I feel like I'm missing a key insight. How should I read the type ((l ~ r) => t) -> t?
I'm reading it as "given a term which requires
l ~ r, return that term"
It's "given a term whose type contains l, return that term with all ls being substituted by rs in the type" (or in the other direction r -> l). It's a very neat trick, that allows you to delegate all cong, trans, subst and similar stuff to GHC.
Here is an example:
{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-}
data Nat = Z | S Nat
data Natty n where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
data Vec a n where
Nil :: Vec a Z
Cons :: a -> Vec a n -> Vec a (S n)
type family (n :: Nat) :+ (m :: Nat) :: Nat where
Z :+ m = m
(S n) :+ m = S (n :+ m)
assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t
assoc Zy my py t = t
assoc (Sy ny) my py t = assoc ny my py t
coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce ny my py xs = assoc ny my py xs
UPDATE
It's instructive to specialize assoc:
assoc' :: Natty n -> Natty m -> Natty p ->
(((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)))
-> Vec a (n :+ (m :+ p))
assoc' Zy my py t = t
assoc' (Sy ny) my py t = assoc ny my py t
coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p))
coerce' ny my py xs = assoc' ny my py xs
Daniel Wagner explained what's going on in comments:
Or, to say it another way, you can read ((l ~ r) => t) -> t as, "given a term that is well typed assuming that l ~ r, return that same term from a context where we have proven l ~ r and discharged that assumption".
Let's elaborate the proving part.
In the assoc' Zy my py t = t case n is equal to Zy and hence we have
((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p))
which reduces to
(m :+ p) ~ (m :+ p)
This is clearly identity and hence we can discharge that assumption and return t.
At each recursive step we maintain the
((n :+ m) :+ p) ~ (n :+ (m :+ p))
equation. So when assoc' (Sy ny) my py t = assoc ny my py t the equation becomes
((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p))
which reduces to
Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p))
due to the definition of (:+). And since constructors are injective
constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m
constructors_are_injective xs = xs
the equation becomes
((n :+ m) :+ p) ~ (n :+ (m :+ p))
and we can call assoc' recursively.
Finally in the call of coerce' these two terms are unified:
1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))
2. Vec a ((n :+ m) :+ p)
Clearly Vec a ((n :+ m) :+ p) is Vec a (n :+ (m :+ p)) under the assumption that ((n :+ m) :+ p) ~ (n :+ (m :+ p)).