Last active
August 29, 2015 14:20
-
-
Save AndrasKovacs/98787f19fce22be025ab to your computer and use it in GitHub Desktop.
Unabiguously injecting functors with an inner type index into open sums.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE | |
DataKinds, PolyKinds, TypeFamilies, MultiParamTypeClasses, | |
RankNTypes, FlexibleInstances, UndecidableInstances, | |
TypeOperators, ConstraintKinds, FlexibleContexts, | |
DeriveFunctor, ScopedTypeVariables #-} | |
import Data.Proxy | |
import Control.Monad.Free | |
data Pos = Here | GoLeft Pos | GoRight Pos | |
data (f :+: g) a = Inl (f a) | Inr (g a) | |
deriving (Eq, Show, Functor) | |
class Subsume e f g where | |
inj' :: Proxy e -> f a -> g a | |
prj' :: Proxy e -> g a -> Maybe (f a) | |
instance Subsume Here f f where | |
inj' _ fa = fa | |
prj' _ fa = Just fa | |
instance Subsume pos f g => Subsume (GoLeft pos) f (g :+: h) where | |
inj' _ fa = Inl (inj' (Proxy :: Proxy pos) fa) | |
prj' _ (Inl ga) = prj' (Proxy :: Proxy pos) ga | |
prj' _ _ = Nothing | |
instance Subsume pos f h => Subsume (GoRight pos) f (g :+: h) where | |
inj' _ fa = Inr (inj' (Proxy :: Proxy pos) fa) | |
prj' _ (Inr ga) = prj' (Proxy :: Proxy pos) ga | |
prj' _ _ = Nothing | |
type family Lookup1_ l r where | |
Lookup1_ (Just '(pos , a)) r = Just '(GoLeft pos, a) | |
Lookup1_ l (Just '(pos , a)) = Just '(GoRight pos, a) | |
Lookup1_ l r = Nothing | |
type family Lookup1 f g :: Maybe (Pos, ix) where | |
Lookup1 f (g :+: h) = Lookup1_ (Lookup1 f g) (Lookup1 f h) | |
Lookup1 f (f a) = Just '(Here, a) | |
Lookup1 f g = Nothing | |
type family FromJust x where | |
FromJust (Just x) = x | |
type family Fst x where | |
Fst '(a, b) = a | |
type family Snd x where | |
Snd '(a, b) = b | |
type IxOf f g = Snd (FromJust (Lookup1 f g)) | |
type PosOf f g = Fst (FromJust (Lookup1 f g)) | |
type Sub1 f g = Subsume (PosOf f g) (f (IxOf f g)) g | |
inj1 :: forall f g a. (Sub1 f g) => f (IxOf f g) a -> g a | |
inj1 fa = inj' (Proxy :: Proxy (PosOf f g)) fa | |
prj1 :: forall f g a. (Sub1 f g) => g a -> Maybe (f (IxOf f g) a) | |
prj1 ga = prj' (Proxy :: Proxy (PosOf f g)) ga | |
-- example | |
type Index = Int | |
data DSL a next = Read Index (a -> next) | |
| Write a (Index -> next) | |
| GetLastIndex (Index -> next) | |
deriving (Functor) | |
getLastIndex :: (Functor f, Sub1 DSL f, MonadFree f m) => m Index | |
getLastIndex = liftF (inj1 (GetLastIndex id)) | |
read :: (Functor f, Sub1 DSL f, MonadFree f m) => Index -> m (IxOf DSL f) | |
read idx = liftF (inj1 (Read idx id)) | |
write :: (Functor f, Sub1 DSL f, MonadFree f m) => IxOf DSL f -> m Index | |
write a = liftF (inj1 (Write a id)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment