Reified.hs

{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE Rank2Types              #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeInType              #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Reified where

import Data.Kind (Constraint, Type)
import GHC.TypeLits (Nat, type (+), type (-))

--------------------------------------------------------------------------------
-- Reify fundeps
class f a b c => Reified2 f a b c | f a b -> c
class f a b => Reified f a b | f a -> b

instance {-# OVERLAPPABLE #-} (f a b c, Reified2 f a b c) => Reified (f a) b c

--------------------------------------------------------------------------------
-- * Flip

class Reified2 f b a c => Flip f a b c | f a b -> c
instance Reified2 f b a c => Flip f a b c

instance (Flip f b a c, Reified2 f a b c) => Reified2 (Flip f) b a c

--------------------------------------------------------------------------------
-- * Map

class Map (f :: k -> j -> Constraint) (as :: [k]) (bs :: [j]) | as f -> bs where

instance Map f '[] '[]
instance (Reified f a b, Map f as bs) => Map f (a ': as) (b ': bs)

--------------------------------------------------------------------------------
-- * Some functions

class Add (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c
instance c ~ (a + b) => Add a b c

class Sub (a :: Nat) (b :: Nat) (c :: Nat) | a b -> c
instance c ~ (a - b) => Sub a b c

instance Add a b c => Reified2 Add a b c
instance Sub a b c => Reified2 Sub a b c
--------------------------------------------------------------------------------

data Proxy a = Proxy

--------------------------------------------------------------------------------
-- * Examples

map' :: forall f xs ys. Map f xs ys => Proxy ys
map' = Proxy

-- *Reified> :t map' @(Add 10) @'[1,2,3,4,5]
-- map' @(Add 10) @'[1,2,3,4,5] :: Proxy '[11, 12, 13, 14, 15]

-- *Reified> :t map' @(Flip Sub 1) @'[1,2,3,4,5]
-- map' @(Flip Sub 1) @'[1,2,3,4,5] :: Proxy '[0, 1, 2, 3, 4]