instance-control (empty) → 0.1.0.0

raw patch · 6 files changed

+370/−0 lines, 6 filesdep +basedep +mtldep +transformerssetup-changed

Dependencies added: base, mtl, transformers

Files

Control/Instances/Morph.hs +149/−0
Control/Instances/ShortestPath.hs +69/−0
Control/Instances/TypeLevelPrelude.hs +88/−0
LICENSE +30/−0
Setup.hs +2/−0
instance-control.cabal +32/−0

+ Control/Instances/Morph.hs view

@@ -0,0 +1,149 @@+{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, PolyKinds, UndecidableInstances, AllowAmbiguousTypes, RankNTypes, ScopedTypeVariables, FlexibleContexts, OverlappingInstances #-}
+
+module Control.Instances.Morph (GenMorph(..), Morph(..)) where
+
+import Control.Instances.ShortestPath
+
+import Control.Monad.Identity
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.List
+import Control.Monad.State
+import Data.Maybe
+import Data.Proxy
+import GHC.TypeLits
+import Control.Instances.TypeLevelPrelude
+
+-- | States that 'm1' can be represented with 'm2'.
+-- That is because 'm2' contains more infromation than 'm1'.
+--
+-- The 'MMorph' relation defines a natural transformation from 'm1' to 'm2'
+-- that keeps the following laws:
+--
+-- > morph (return x)  =  return x
+-- > morph (m >>= f)   =  morph m >>= morph . f
+-- 
+-- It is a reflexive and transitive relation.
+--
+class Morph (m1 :: * -> *) (m2 :: * -> *) where
+  -- | Lifts the first monad into the second.
+  morph :: m1 a -> m2 a
+  
+instance GenMorph DB m1 m2 => Morph m1 m2 where
+  morph = genMorph db
+  
+-- | A generalized version of 'Morph'. Can work on different
+-- rulesets, so this should be used if the ruleset is to be extended.
+class GenMorph db (m1 :: * -> *) (m2 :: * -> *) where
+  -- | Lifts the first monad into the second.
+  genMorph :: db -> m1 a -> m2 a
+  
+instance ( fl ~ (TransformPath (PathFromList (ShortestPath (ToMorphRepo DB) x y)))
+         , CorrectPath x y fl
+         , GeneratableMorph DB fl
+         , Morph' fl x y
+         ) => GenMorph DB x y where
+  genMorph db = repr (generateMorph db :: fl)
+  
+class Morph' fl x y where
+  repr :: fl -> x a -> y a
+  
+instance Morph' r y z => Morph' (ConnectMorph x y :+: r) x z where
+  repr (ConnectMorph m :+: r) = repr r . m
+ 
+instance (Morph' r m x, Monad m) => Morph' (IdentityMorph m :+: r) Identity x where
+  repr (IdentityMorph :+: r) = (repr r :: forall a . m a -> x a) . return . runIdentity
+  
+instance Morph' (MUMorph m :+: r) m Proxy where
+  repr (MUMorph :+: _) = const Proxy
+ 
+instance Morph' NoMorph x x where
+  repr fl = id
+  
+infixr 6 :+:
+data a :+: r = a :+: r 
+
+data NoMorph = NoMorph
+  
+type family ToMorphRepo db where
+  ToMorphRepo (cm :+: r) = TranslateConn cm ': ToMorphRepo r
+  ToMorphRepo NoMorph = '[]
+   
+type DB = ConnectMorph_2m Maybe MaybeT
+           :+: ConnectMorph_mt MaybeT 
+           :+: ConnectMorph Maybe [] 
+           :+: ConnectMorph_2m [] ListT
+           :+: ConnectMorph (MaybeT IO) (ListT IO)
+           :+: NoMorph
+ 
+db :: DB 
+db = ConnectMorph_2m (MaybeT . return) 
+       :+: ConnectMorph_mt (MaybeT . liftM Just) 
+       :+: ConnectMorph (maybeToList) 
+       :+: ConnectMorph_2m (ListT . return) 
+       :+: ConnectMorph (ListT . liftM maybeToList . runMaybeT) 
+       :+: NoMorph
+  
+-- | This class provides a way to construct the value-level transformations
+-- from the type-level path and a rulebase.
+class GeneratableMorph db ch where
+  generateMorph :: db -> ch
+    
+instance GeneratableMorph db NoMorph where
+  generateMorph _ = NoMorph
+  
+instance GeneratableMorph db r 
+      => GeneratableMorph db ((IdentityMorph m) :+: r) where
+  generateMorph db = IdentityMorph :+: generateMorph db
+  
+instance GeneratableMorph db r 
+      => GeneratableMorph db (MUMorph m :+: r) where
+  generateMorph db = MUMorph :+: generateMorph db
+  
+instance (HasMorph db (ConnectMorph a b), GeneratableMorph db r) 
+      => GeneratableMorph db (ConnectMorph a b :+: r) where
+  generateMorph db = getMorph db :+: generateMorph db
+  
+-- | This class extracts a given morph from the set of rules
+class HasMorph r m where 
+  getMorph :: r -> m
+instance HasMorph (m :+: r) m where
+  getMorph (c :+: r) = c
+instance Monad k => HasMorph (ConnectMorph_2m a b :+: r) (ConnectMorph a (b k)) where
+  getMorph (ConnectMorph_2m f :+: r) = ConnectMorph f
+instance Monad k => HasMorph (ConnectMorph_mt t :+: r) (ConnectMorph k (t k)) where
+  getMorph (ConnectMorph_mt f :+: r) = ConnectMorph f
+instance HasMorph r m => HasMorph (c :+: r) m where
+  getMorph (c :+: r) = getMorph r
+
+-- | Checks if the path is found to provide usable error messages
+class CorrectPath from to path
+
+instance CorrectPath from to (a :+: b)
+instance CorrectPath from to NoMorph
+
+data ConnectMorph m1 m2 = ConnectMorph { fromConnectMorph :: forall a . m1 a -> m2 a }
+data ConnectMorph_2m m1 m2 = ConnectMorph_2m { fromConnectMorph_2m :: forall a k . Monad k => m1 a -> m2 k a }
+data ConnectMorph_mt mt = ConnectMorph_mt { fromConnectMorph_mt :: forall a k . Monad k => k a -> mt k a }
+data IdentityMorph (m :: * -> *) = IdentityMorph
+data MUMorph m = MUMorph
+
+-- | Transforms a path element from the generic format to the specific one
+type family TranslateConn m where
+  TranslateConn (ConnectMorph m1 m2) = Connect m1 m2
+  TranslateConn (ConnectMorph_2m m1 m2) = Connect_2m m1 m2
+  TranslateConn (ConnectMorph_mt mt) = Connect_mt mt
+  
+-- | Transforms the path from the generic format to the specific one
+type family TransformPath m where
+  TransformPath (Connect m1 m2 :+: r) = ConnectMorph m1 m2 :+: TransformPath r
+  TransformPath (Connect_id m :+: r) = IdentityMorph m :+: TransformPath r
+  TransformPath (Connect_MU m :+: r) = MUMorph m :+: TransformPath r
+  TransformPath NoMorph = NoMorph
+  TransformPath NoPathFound = NoPathFound
+  
+type family PathFromList ls where
+  PathFromList '[] = NoMorph
+  PathFromList '[ NoPathFound ] = NoPathFound
+  PathFromList (c ': ls) = c :+: PathFromList ls
+
+

+ Control/Instances/ShortestPath.hs view

@@ -0,0 +1,69 @@+{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, PolyKinds, UndecidableInstances, AllowAmbiguousTypes, RankNTypes, ScopedTypeVariables, FlexibleContexts, OverlappingInstances #-}
+
+module Control.Instances.ShortestPath where
+
+import Control.Monad.Identity
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.List
+import Control.Monad.State
+import Data.Maybe
+import Data.Proxy
+import GHC.TypeLits
+import Control.Instances.TypeLevelPrelude
+
+-- * Generic datatypes to store connections
+  
+data Connect m1 m2
+data Connect_2m m1 m2
+data Connect_mt mt
+data Connect_id m
+data Connect_MU m
+
+-- | Marks that there is no legal path between the two types according
+-- to the rulebase.
+data NoPathFound
+  
+type family ShortestPath (e :: [*]) (s :: * -> *) (t :: * -> *) :: [*] where
+  ShortestPath e t t = '[]
+  ShortestPath e Identity t = '[ Connect_id t ]
+  ShortestPath e s Proxy = '[ Connect_MU s ]
+  ShortestPath e s t = ShortestPath' e s (InitCurrent e t)
+  
+type family ShortestPath' (e :: [*]) (s :: * -> *) (c :: [[*]]) :: [*] where
+  ShortestPath' e s '[] = '[ NoPathFound ]
+  ShortestPath' e s c = FromMaybe (ShortestPath' e s (ApplyEdges e c c))
+                                  (GetFinished s c) 
+                                  
+                                      
+type family GetFinished s c where
+  GetFinished s ((Connect s b ': p) ': lls) 
+    = Just (Connect s b ': p)
+  GetFinished s (p ': lls) = GetFinished s lls
+  GetFinished s '[] = Nothing
+
+type family InitCurrent (e :: [*]) (t :: * -> *) :: [[*]] where
+  InitCurrent '[] t = '[]
+  InitCurrent (e ': es) t = IfJust (ApplyEdge e t)
+                                   ('[ MonomorphEnd e t ] ': InitCurrent es t) 
+                                   (InitCurrent es t)
+  
+type family ApplyEdges (e :: [*]) (co :: [[*]]) (c :: [[*]]) :: [[*]] where
+  ApplyEdges (e ': es) co ((Connect s b ': p) ': cs) 
+    = AppendJust (IfThenJust (IsJust (ApplyEdge e s)) 
+                                (MonomorphEnd e s ': Connect s b ': p)) 
+                 (ApplyEdges (e ': es) co cs)
+  ApplyEdges (e ': es) co '[] = ApplyEdges es co co
+  ApplyEdges '[] co cr = '[]  
+  
+type family ApplyEdge e t :: Maybe (* -> *) where
+  ApplyEdge (Connect ms mr) mr = Just ms
+  ApplyEdge (Connect_2m ms mt) (mt m) = Just ms
+  ApplyEdge (Connect_mt mt) (mt m) = Just m
+  ApplyEdge e t = Nothing
+
+type family MonomorphEnd c v :: * where
+  MonomorphEnd (Connect_2m m m') v = Connect m v
+  MonomorphEnd (Connect_mt t) (t m) = Connect m (t m)
+  MonomorphEnd c v = c
+
+

+ Control/Instances/TypeLevelPrelude.hs view

@@ -0,0 +1,88 @@+{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, PolyKinds, UndecidableInstances, AllowAmbiguousTypes, RankNTypes, ScopedTypeVariables, FlexibleContexts #-}
+
+module Control.Instances.TypeLevelPrelude where
+
+import GHC.TypeLits
+
+type family Const a b where
+  Const a b = a
+  
+type family Seq a b where
+  Seq a b = b
+  
+type family LazyIfThenElse p a b where
+  LazyIfThenElse True a b = a
+  LazyIfThenElse False a b = b
+  
+type family Iterate a where
+  Iterate a = a ': Iterate a
+
+type family l1 :++: l2 where
+  '[] :++: l2       = l2
+  (e ': r1) :++: l2 = e ': (r1 :++: l2)
+  
+type family Elem e ls where
+  Elem e '[] = False
+  Elem e (e ': ls) = True
+  Elem e (x ': ls) = Elem e ls
+  
+type family IfThenElse (b :: Bool) (th :: x) (el :: x) :: x where
+  IfThenElse True  th el = th
+  IfThenElse False th el = el
+         
+type family Length ls :: Nat where
+  Length '[] = 0
+  Length (e ': ls) = 1 + Length ls
+           
+type family Head (ls :: [k]) :: k where
+  Head (e ': ls) = e   
+  
+type family HeadMaybe (ls :: [k]) :: Maybe k where
+  HeadMaybe (e ': ls) = Just e
+  HeadMaybe '[] = Nothing
+  
+type family FromMaybe d m where
+  FromMaybe d (Just x) = x
+  FromMaybe d Nothing = d
+  
+type family Same a b where
+  Same a a = True
+  Same a b = False
+  
+type family Null (ls :: [k]) :: Bool where
+  Null '[] = True
+  Null ls = False
+           
+type family MapAppend e lls where
+  MapAppend e (ls ': lls) = (e ': ls) ': MapAppend e lls
+  MapAppend e '[] = '[]
+  
+type family AppendJust m ls where
+  AppendJust (Just x) ls = x ': ls
+  AppendJust Nothing ls = ls
+  
+type family Revert ls where
+  Revert '[] = '[]
+  Revert (e ': ls) = Revert ls :++: '[ e ]
+  
+type family IfThenJust (p :: Bool) (v :: k) :: Maybe k where
+  IfThenJust True v = Just v
+  IfThenJust False v = Nothing  
+  
+type family IfJust (p :: Maybe k) (t :: kr) (e :: kr) :: kr where
+  IfJust (Just x) t e = t
+  IfJust Nothing t e = e
+  
+type family IsJust (p :: Maybe k) :: Bool where
+  IsJust (Just x) = True
+  IsJust Nothing = False    
+  
+type family FromJust (p :: Maybe k) :: k where
+  FromJust (Just x) = x
+  
+type family Cat (f2 :: k2 -> k3) (f1 :: k1 -> k2) (a :: k1) :: k3 where
+  Cat f2 f1 a = f2 (f1 a)
+  
+
+  
+

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Boldizsar Nemeth
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Boldizsar Nemeth nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

+ instance-control.cabal view

@@ -0,0 +1,32 @@+
+name:                instance-control
+version:             0.1.0.0
+synopsis:            Controls how the compiler searches for instances using type families.
+description:         GHC has no capability to perform graph searches on instance definition. Because of that,
+                     transitive rules for type classes cannot be defined. This package solves the issue with
+                     type functions performing a search on the graph where nodes are types and edges are
+                     rules from a given rule database. After constructing the type-level representation of the
+                     wanted path, the system constructs the needed functions from the value-level representation
+                     of the database.
+homepage:            https://github.com/lazac/instance-control
+license:             BSD3
+license-file:        LICENSE
+author:              Boldizsar Nemeth
+maintainer:          nboldi@caesar.elte.hu
+-- copyright:           
+category:            Control
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+source-repository head
+  type:                git
+  location:            http://github.com/nboldi/instance-control
+
+library
+  exposed-modules:     Control.Instances.Morph
+  other-modules:       Control.Instances.TypeLevelPrelude
+                     , Control.Instances.ShortestPath
+  other-extensions:    TypeFamilies, DataKinds, TypeOperators, MultiParamTypeClasses, FlexibleInstances, PolyKinds, UndecidableInstances, AllowAmbiguousTypes, RankNTypes, ScopedTypeVariables, FlexibleContexts, OverlappingInstances
+  build-depends:       base >=4.7 && <4.9, mtl >=2.2 && <2.3, transformers >=0.4 && <0.5
+  -- hs-source-dirs:      
+  default-language:    Haskell2010