Build reverse hierarchy

Rev-deps.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
import Control.Category
import Control.Arrow
import Data.Proxy
import Data.Constraint
import Data.Vinyl (Rec(..))
import Prelude hiding ((.), id)


type x ~> y = forall a b. x a b -> y a b

newtype Freer cst eff a b = Freer {  runFreer :: forall x. cst x => (eff ~> x) -> x a b }

-- Instances
instance CInf c Category => Category (Freer c eff) where
  id = Freer $ \(_g :: eff ~> x)-> case cInf @ c @ Category @ x of
     Sub Dict -> id
  Freer f . Freer g = Freer $ \(x :: eff ~> x) -> case cInf @ c @ Category @ x of
     Sub Dict -> f x . g x

instance (CInf a Category, CInf a Arrow) => Arrow (Freer a eff) where
  arr a = Freer $ \(_g :: eff ~> x) ->
            case cInf @ a @ Arrow @ x of
              Sub Dict -> case cInf @ Arrow @ Category @ x of
                Sub Dict -> arr a
  first (Freer a) = Freer $ \(f :: eff ~> x) -> case cInf @ a @ Arrow @ x of
                       Sub Dict -> first (a f)


instance (CInf c Category, CInf c Arrow, CInf c ArrowChoice) => ArrowChoice (Freer c eff) where
  left (Freer a) = Freer $ \(f :: eff ~> x) ->
    case cInf @ c @ ArrowChoice @ x of
      Sub Dict -> left (a f)


-- Tests
test0 :: Freer Category eff a a
test0 = id

test1 :: Freer Arrow eff a a
test1 = id

test2 :: Freer ArrowChoice eff a a
test2 = id

test3 :: (b -> c) -> Freer Arrow eff b c
test3 = arr

test4 :: (b -> c) -> Freer ArrowChoice eff b c
test4 = arr

test5 :: Freer ArrowChoice eff b c -> Freer ArrowChoice eff (Either b d) (Either c d)
test5 = left

--- Dependecy list
-- Encode single level of the class depth.
-- TODO: keep either tf or class

type family DepList (a :: k) :: [k]
type instance DepList Category = '[]
type instance DepList Arrow = '[Category]
type instance DepList ArrowChoice = '[Arrow]

class C0 o is | o -> is where c0 :: forall x . Rec (x :-- o) is
instance C0 Category    '[] where c0 = RNil
instance C0 Arrow       '[Category] where c0 = S (Sub Dict) :& RNil
instance C0 ArrowChoice '[Arrow] where c0    = S (Sub Dict) :& RNil

-- Helper instances
type family If a b c where
  If 'True b c = b
  If 'False b c = c

-- TODO: use any from singletons
type family AnyD s h :: Bool where
  AnyD x (s:ss) = If (DepExists x s) 'True (AnyD x ss)
  AnyD _ _ = 'False

-- TODO: use something from singletons
type family DepExists (search :: k) (hay :: k) :: Bool where
  DepExists a a = 'True
  DepExists a b = AnyD a (DepList b)

-- Type equality over a class
type family EqT a b :: Bool where
  EqT a a = True
  EqT a b = False


-- type wrapper for the proof
newtype (:--) x o i = S (o x :- i x)


-- Infinite search, we look in all deps to find required constraint recursively
class CInf o req where cInf :: o x :- req x
instance (CInfInner t o req, (EqT o req) ~ t) => CInf o req where cInf = cInfInner (Proxy @ t)

-- Helper method in order to allow case split on in the type class as we have to choices
-- a == req, and DEP(a) == req if we would not introduce such search will loop
class CInfInner t a b where cInfInner :: proxy t -> a x :- b x
instance CInfInner 'True o o where cInfInner _ = refl
instance (C0 o cs, CInfSearch cs req) => CInfInner 'False o req where
  cInfInner _ = helper where
                helper :: forall x . o x :- req x
                helper = case c0 @ o @ cs @ x of rec -> cInfSearch rec

-- Search in the dependencies list
class CInfSearch cs req where cInfSearch :: Rec (x :-- o) cs -> (o x :- req x)
instance ((DepExists req c) ~ t, CInfSearchInner t (c:cs) req) => CInfSearch (c:cs) req where cInfSearch rec = cInfSearchInner (Proxy @ t) rec

-- Helper class to allow case split on classes
class CInfSearchInner t cs req where cInfSearchInner :: proxy t -> Rec (x :-- o) cs -> (o x :- req x)
instance CInf c req => CInfSearchInner 'True (c:cs) req where
  cInfSearchInner _ (S proof :& _) = cInf @ c @req `trans` proof
instance CInfSearch cs req => CInfSearchInner 'False (c:cs) req where
  cInfSearchInner _ (_ :& rest) = cInfSearch rest

Reply to the https://codegists.com/snippet/haskell/freerhs_nc6_haskell