[Haskell-cafe] Constraint-folding

[Carter Schonwald]

Have you looked at The singleton lib on hackage by Richard Eisenberg? Seems
like it may be related. Or at least touches on related matters.

On Sunday, December 1, 2013, Andras Slemmer <0slemi0 at gmail.com> wrote:

> 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/eaac350d/attachment.html>