Compatibility with GHC 8.4

src/Data/Type/Index/Trans.hs

@@ -0,0 +1,73 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Data.Type.Index.Trans
+  ( module Data.Type.Index.Trans
+  , (:~:)(..)
+  ) where
+
+import Type.Class.Witness ((:~:)(..))
+import Type.Family.List
+import Type.Family.Tuple
+
+type IxList' = IxList (:~:)
+type IxEnv   = IxList (IxFirst (:~:))
+
+class IxLift (t :: (k -> m -> *) -> l -> m -> *) (x :: l) where
+  type LiftI t x :: k
+  ixLift :: i (LiftI t x) y
+         -> t i x y
+
+data IxList (i :: k -> l -> *) :: [k] -> l -> * where
+  IxHead :: !(i a b)
+         -> IxList i (a :< as) b
+  IxTail :: !(IxList i as b)
+         -> IxList i (a :< as) b
+
+data IxFirst (i :: k -> l -> *) :: (k,m) -> l -> * where
+  IxFirst :: !(i a b)
+          -> IxFirst i '(a,c) b
+
+instance (p ~ '(Fst p,Snd p)) => IxLift IxFirst p where
+  type LiftI IxFirst p = Fst p
+  ixLift = IxFirst
+
+data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where
+  IxSecond :: !(i a b)
+           -> IxSecond i '(c,a) b
+
+instance (p ~ '(Fst p,Snd p)) => IxLift IxSecond p where
+  type LiftI IxSecond p = Snd p
+  ixLift = IxSecond
+
+data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where
+  IxOrL :: !(i a b)
+        -> IxOr i j (Left a) b
+  IxOrR :: !(j a b)
+        -> IxOr i j (Right a) b
+
+instance IxLift (IxOr i) (Right a) where
+  type LiftI (IxOr i) (Right a) = a
+  ixLift = IxOrR
+
+data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where
+  IxJust :: !(i a b)
+         -> IxJust i (Just a) b
+
+data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> * where
+  IxComp :: !(i a b)
+         -> !(j b c)
+         -> IxComp i j a c
+

src/Data/Type/Product/Env.hs

@@ -0,0 +1,117 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Data.Type.Product.Env where
+
+import Data.Type.Combinator (Comp1(..))
+import Data.Type.Conjunction
+import Data.Type.Boolean
+import Data.Type.Index
+import Data.Type.Index.Trans
+import Data.Type.Option
+import Data.Type.Product
+import Type.Class.Higher
+import Type.Class.Witness
+import Type.Family.Bool
+import Type.Family.List
+
+newtype Env k v ps = Env
+  { getEnv :: Prod (k :*: v) ps
+  }
+
+type family Member (x :: k) (ps :: [(k,v)]) :: Bool where
+  Member x Ø              = False
+  Member x ('(y,a) :< ps) = (x == y) || Member x ps
+
+member' :: BoolEquality k => k x -> Env k v ps -> Boolean (Member x ps)
+member' x = (. getEnv) $ \case
+  Ø               -> False_
+  (y :*: _) :< ps -> (x .== y) .|| member' x (Env ps)
+
+type family Lookup (x :: k) (ps :: [(k,v)]) :: Maybe v where
+  Lookup x Ø              = Nothing
+  Lookup x ('(y,a) :< ps) = If (x == y) (Just a) (Lookup x ps)
+
+lookup' :: BoolEquality k => k x -> Env k v ps -> Option v (Lookup x ps)
+lookup' x = (. getEnv) $ \case
+  Ø              -> Nothing_
+  (y :*: a) :< ps -> if' (x .== y)
+    (Just_ a)
+    (lookup' x $ Env ps)
+
+type family Insert (x :: k) (a :: v) (ps :: [(k,v)]) :: [(k,v)] where
+  Insert x a Ø              = '[ '(x,a) ]
+  Insert x a ('(y,b) :< ps) = If (x == y) ('(x,a) :< ps) ('(y,b) :< Insert x a ps)
+
+insert' :: BoolEquality k => k x -> v a -> Env k v ps -> Env k v (Insert x a ps)
+insert' x a = (. getEnv) $ \case
+  Ø               -> Env $ (x :*: a) :< Ø
+  (y :*: b) :< ps -> if' (x .== y)
+    (Env $ (x :*: a) :< ps)
+    (Env $ (y :*: b) :< getEnv (insert' x a (Env ps)))
+
+type family Delete (x :: k) (ps :: [(k,v)]) :: [(k,v)] where
+  Delete x Ø              = Ø
+  Delete x ('(y,a) :< ps) = If (x == y) ps ('(y,a) :< Delete x ps)
+
+delete' :: BoolEquality k => k x -> Env k v ps -> Env k v (Delete x ps)
+delete' x = (. getEnv) $ \case
+  Ø               -> Env Ø
+  (y :*: a) :< ps -> if' (x .== y)
+    (Env ps)
+    (Env $ (y :*: a) :< getEnv (delete' x (Env ps)))
+
+type family Difference (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where
+  Difference ps Ø              = ps
+  Difference ps ('(x,a) :< qs) = Delete x (Difference ps qs)
+
+difference' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
+difference' ps = (. getEnv) $ \case
+  Ø               -> ps
+  (x :*: _) :< qs -> delete' x $ difference' ps (Env qs)
+
+(.\\) :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Difference ps qs)
+(.\\) = difference'
+
+type family Union (ps :: [(k,v)]) (qs :: [(k,v)]) :: [(k,v)] where
+  Union ps Ø              = ps
+  Union ps ('(x,a) :< qs) = Insert x a (Union ps qs)
+
+union' :: BoolEquality k => Env k v ps -> Env k v qs -> Env k v (Union ps qs)
+union' ps = (. getEnv) $ \case
+  Ø               -> ps
+  (x :*: a) :< qs -> insert' x a $ union' ps (Env qs)
+
+type family Intersection (ps :: [(k,v)]) (qs :: [(k,w)]) :: [(k,v)] where
+  Intersection Ø              qs = Ø
+  Intersection ('(x,a) :< ps) qs = If (Member x qs) ('(x,a) :< Intersection ps qs) (Intersection ps qs)
+
+intersection' :: BoolEquality k => Env k v ps -> Env k w qs -> Env k v (Intersection ps qs)
+intersection' ps qs = case getEnv ps of
+  Ø                -> Env Ø
+  (x :*: a) :< ps' -> if' (member' x qs) (Env $ (x :*: a) :< getEnv rest) rest
+    where
+    rest = intersection' (Env ps') qs
+
+instance Functor1 (Env k) where
+  map1 f = Env . getComp1 . map1 f . Comp1 . getEnv
+
+instance IxFunctor1 (IxList (IxSecond (:~:))) (Env k) where
+  imap1 f = Env . imap1 (\i -> imap1 $ \j -> f $ ixList i j) . getEnv
+
+ixList :: Index as a -> i a b -> IxList i as b
+ixList = \case
+  IZ   -> IxHead
+  IS x -> IxTail . ixList x
+