1 Dec 13:49 2013

## Constraint-folding

Andras Slemmer <0slemi0 <at> gmail.com>

2013-12-01 12:49:04 GMT

2013-12-01 12:49:04 GMT

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?

exI 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?

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe <at> haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe