Skip to content

Instantly share code, notes, and snippets.

@AndrasKovacs
Last active August 29, 2015 14:20
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save AndrasKovacs/98787f19fce22be025ab to your computer and use it in GitHub Desktop.
Save AndrasKovacs/98787f19fce22be025ab to your computer and use it in GitHub Desktop.
Unabiguously injecting functors with an inner type index into open sums.
{-# 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