[Haskell-cafe] Constraint-folding

[Andras Slemmer]

Yes it is very related! In particular it automatically derives the WNat /
WNatClass part. In fact now that I think about it these constraint-folds
can also be automatically generated for every singleton type so I'm
wondering whether there is a place for them in the singletons library.


On 1 December 2013 15:56, Carter Schonwald <carter.schonwald at gmail.com>wrote:

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