wat

Constraints.hs

{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, KindSignatures, PolyKinds, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}
module Constraints where
import Data.Constraint
import Data.Constraint.Unsafe
import Data.Monoid
import Data.Proxy
import Data.Reflection

--------------------------------------------------------------------------------
-- Intro

newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) = Lift { lower :: a }

class ReifiableConstraint p where
  data Def (p :: * -> Constraint) (a :: *) :: *
  reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)

--------------------------------------------------------------------------------
-- Machinery

with :: Def p a -> (forall s. Reifies s (Def p a) => Lift p a s) -> a
with d v = reify d (lower . asProxyOf v)
  where
    asProxyOf :: f s -> Proxy s -> f s
    asProxyOf x _ = x

using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
using d m = reify d $ \(_ :: Proxy s) ->
  let replaceProof :: Reifies s (Def p a) :- p a
      replaceProof = trans proof reifiedIns
        where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
  in m \\ replaceProof

usingT :: forall p f a. ReifiableConstraint p => Def p a -> (p a => f a) -> f a
usingT d m = reify d $ \(_ :: Proxy s) ->
  let replaceProof :: Reifies s (Def p a) :- p a
      replaceProof = trans proof reifiedIns
        where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
  in m \\ replaceProof

--------------------------------------------------------------------------------
-- Instances

instance ReifiableConstraint Eq where
  data Def Eq a = Eq { eq_ :: a -> a -> Bool }
  reifiedIns = Sub Dict

instance Reifies s (Def Eq a) => Eq (Lift Eq a s) where
  a == b = eq_ (reflect a) (lower a) (lower b)

instance ReifiableConstraint Ord where
  data Def Ord a = Ord { compare_ :: a -> a -> Ordering }
  reifiedIns = Sub Dict

instance Reifies s (Def Ord a) => Eq (Lift Ord a s) where
  a == b = (compare a b == EQ)

instance Reifies s (Def Ord a) => Ord (Lift Ord a s) where
  compare a b = compare_ (reflect a) (lower a) (lower b)

instance ReifiableConstraint Monoid where
  data Def Monoid a = Monoid { mappend_ :: a -> a -> a, mempty_ :: a }
  reifiedIns = Sub Dict

instance Reifies s (Def Monoid a) => Monoid (Lift Monoid a s) where
  mappend a b        = Lift $ mappend_ (reflect a) (lower a) (lower b)
  mempty = a where a = Lift $ mempty_ (reflect a)

--------------------------------------------------------------------------------
-- Examples

example1 :: Int
example1 = using (Monoid (+) 0) $ mempty <> 12

example2 :: Int
example2 = using (Ord compare) $ max 1 2
{-# NOINLINE example2 #-}

example3 :: Int
example3 = using (Ord $ flip compare) $ max 1 2
{-# NOINLINE example3 #-}

example5 :: Int
example5 = with (Ord $ flip compare) $ max (Lift 1) (Lift 2)

main :: IO ()
main = do
  print example1
  print example2
  print example3
  let example4 :: Int
      example4 = using (Ord $ flip compare) $ max 1 2
  print example4
  print (using (Ord $ flip compare) $ max 1 (2::Int))
  print example5

output.txt

$ ghc -dcmm-lint -dcore-lint -fforce-recomp -O0 Constraints.hs -main-is Constraints.main; ./Constraints                                                                                              
[1 of 1] Compiling Constraints      ( Constraints.hs, Constraints.o )
Linking Constraints ...
12
2
2
2
1
1
$