[Haskell-cafe] Constraint-folding

[oleg at okmij.org]

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)