[Haskell-cafe] Constraint-folding
oleg at okmij.org
oleg at okmij.org
Tue Dec 3 09:47:13 UTC 2013
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)
More information about the Haskell-Cafe
mailing list