[Haskell-cafe] Constraint-folding

[Andras Slemmer]

Hi,

I stumbled upon something pretty neat, and although I'm 95% sure Oleg did
this already 10 years ago in Haskell98 I thought I'd share it because I
find it gorgeous!

The basic issue I was having is that whenever I wrote class instances for a
lifted type (we'll use Nat):

class Class (n :: Nat)
instance Class Zero
instance (Class m) => Class (Succ m)

I always had to litter my code with "(Class n) =>" restrictions even in
places where they just shouldn't belong. However my gut feeling was that
the generic instance "should" be implied, as we covered all cases. A while
ago I proposed a new syntax to do just this (
https://ghc.haskell.org/trac/ghc/ticket/6150) which failed miserably, and
for good reason!

However there is a way to do it anyway:)

What we need is basically a way to "construct" an instance for the fully
polymorpic case: "instance Class n". We cannot do this directly as it would
overlap with our original instances (and we couldn't implement it anyway),
we need another way of representing class instances:

type W p = forall a. (p => a) -> a

W p simply "wraps" the constraint p into a function that eliminates the
constraint on a passed in value. Now we can treat a constraint as a
function.

We will also need a way to "pattern match" on our lifted types, we will do
this with an indexed GADT:

data WNat n where -- W for Witness
    WZero :: WNat Zero
    WSucc :: WNat n -> WNat (Succ n)

And finally the neat part; one can write a general typeclass-polymorphic
induction principle on these wrapped constraints (or a "constraint-fold"):

natFold :: WNat n -> W (p Zero) -> (forall m. W (p m) -> W (p (Succ m))) ->
W (p n)

W (p Zero) in the p ~ Class case corresponds to "instance Class Zero", and
(forall m. W (p m) -> W (p (Succ m))) corresponds to "instance (Class m) =>
Class (Succ m)"
This function is precisely what we need in order to construct the generic
instance!

(Note: the implementation of natFold is NOT trivial as we need to wrestle
with the type checker in the inductive case, but it is a nice excercise.
The solution is here: http://lpaste.net/96429)

Now we can construct the generic instance:

genericClass :: WNat n -> (Class n => a) -> a
genericClass n = natFold n (\x -> x) (\f x -> f x) -- Cannot use id as that
would try to unify away our constraints

Or equivalently:

class WNatClass n where
    witness :: WNat n
instance WNatClass Zero where
    witness = WZero
instance (WNatClass m) => WNatClass (Succ m) where
    witness = WSucc witness

genericClass' :: (WNatClass n) => (Class n => a) -> a
genericClass' = genericClass witness

Now we can decouple all our "(Class n) =>" and similar constraints, all we
need is a WNatClass restriction, which I think is a good enough trade-off
(and it's not really a restriction anyway).

What do you think?

ex
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131201/87457cc4/attachment.html>