Andras Slemmer | 1 Dec 13:49 2013
Picon

Constraint-folding

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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Carter Schonwald | 1 Dec 16:56 2013
Picon

Re: Constraint-folding

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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andras Slemmer | 1 Dec 17:06 2013
Picon

Re: Constraint-folding

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
oleg | 3 Dec 10:47 2013

Re: Constraint-folding


Andras Slemmer wrote:
> I stumbled upon something pretty neat, and although I'm 95% sure Oleg did
> this already 10 years ago in Haskell98

You're quite right about this: Chung-chieh Shan and I did this
reification of constraint in December 2003, and almost in Haskell 98
(we needed Rank2 types though). It was described in the following
paper
        http://okmij.org/ftp/Haskell/types.html#Prepose
We called this transformation reflection/reification.

I'm writing though to show a dual formulation to your development of
using singletons. It gets by without GADTs and uses very few extensions:
essentially Haskell98 with Rank2 types.

{-# LANGUAGE RankNTypes #-}

data Zero
data Succ a

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

-- Tagless final    
class Sym repr where
    z :: repr Zero
    s :: repr n -> repr (Succ n)

newtype R x = R{unR:: x}                -- the identity interpreter

instance Sym R where
    z = R undefined
    s _ = R undefined

newtype S x = S Integer                 -- for show

instance Sym S where
    z = S 0
    s (S x) = S (x + 1)

newtype Reify n = Reify (forall a. (Class n => n -> a) -> a)

instance Sym Reify where
  z = Reify (\f -> f (unR z))
  s (Reify f) = Reify (\g -> f (g . unR . s . R))

genericClass :: (forall repr. Sym repr => repr n) -> (Class n => a) -> a
genericClass m f = case m of
                   Reify k -> k (const f)

Gmane