Skip to content

Instantly share code, notes, and snippets.

@qnikst
Created Nov 3, 2017
Embed
What would you like to do?
Build reverse hierarchy
{-# 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
@qnikst
Copy link
Author

qnikst commented Nov 3, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment