kind-apply 0.2.0.0 → 0.3.0.0

raw patch · 3 files changed

+59/−25 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• kind-apply.cabal +1/−1
• src/Data/PolyKinded.hs +4/−1
• src/Data/PolyKinded/Atom.hs +54/−23

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-apply-version:             0.2.0.0+version:             0.3.0.0 synopsis:            Utilities to work with lists of types description:         This packages reifies the concept of list of types, and application of those to list constructors. -- bug-reports:

@@ -13,7 +13,7 @@ {-# language ConstraintKinds        #-} module Data.PolyKinded (   -- * Lists of types and application-  LoT(..), (:@@:)+  LoT(..), (:@@:), LoT1, LoT2   -- * Splitting types , SplitF, Nat(..), TyEnv(..), SplitN ) where@@ -26,6 +26,9 @@   LoT0    ::                LoT (*)   -- | Cons a type with a list of types.   (:&&:)  :: k -> LoT ks -> LoT (k -> ks)++type LoT1 a = a ':&&: 'LoT0+type LoT2 a b = a ':&&: b ':&&: LoT0  -- | Apply a list of types to a type constructor. --

@@ -4,43 +4,74 @@ {-# language DataKinds       #-} {-# language PolyKinds       #-} {-# language ConstraintKinds #-}+{-# language RankNTypes      #-}+{-# language AllowAmbiguousTypes  #-}+{-# language UndecidableInstances #-} module Data.PolyKinded.Atom where  import Data.Kind import Data.PolyKinded+import Data.Type.Equality+import GHC.Exts -data TyVar d k where+data TyVar (d :: *) (k :: TYPE r) where   VZ :: TyVar (x -> xs) x   VS :: TyVar xs k -> TyVar (x -> xs) k -type V0 = 'Var 'VZ-type V1 = 'Var ('VS 'VZ)-type V2 = 'Var ('VS ('VS 'VZ))-type V3 = 'Var ('VS ('VS ('VS 'VZ)))-type V4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))-type V5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))-type V6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))-type V7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))-type V8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))-type V9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))+type Var0 = 'Var 'VZ+type Var1 = 'Var ('VS 'VZ)+type Var2 = 'Var ('VS ('VS 'VZ))+type Var3 = 'Var ('VS ('VS ('VS 'VZ)))+type Var4 = 'Var ('VS ('VS ('VS ('VS 'VZ))))+type Var5 = 'Var ('VS ('VS ('VS ('VS ('VS 'VZ)))))+type Var6 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))+type Var7 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))+type Var8 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ))))))))+type Var9 = 'Var ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS ('VS 'VZ)))))))))  infixr 5 :&:-data Atom d k where-  Var   :: TyVar d k -> Atom d k-  Kon   :: k         -> Atom d k+infixr 5 :=>>:+data Atom (d :: *) (k :: TYPE r) where+  Var :: TyVar d k -> Atom d k+  Kon :: k         -> Atom d k   (:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2   (:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint+  ForAll  :: Atom (d1 -> d) (*) -> Atom d (*)+  (:=>>:) :: Atom d Constraint -> Atom d (*) -> Atom d (*) -type f :$: x = 'Kon f ':@: x-type a :~: b = 'Kon (~) ':@: a ':@: b+type f :$:  x = 'Kon f ':@: x+type a :~:  b = 'Kon (~) ':@: a ':@: b+type a :~~: b = 'Kon (~~) ':@: a ':@: b -type family Ty (t :: Atom d k) (tys :: LoT d) :: k where-  Ty ('Var 'VZ)     (t ':&&: ts) = t-  Ty ('Var ('VS v)) (t ':&&: ts) = Ty ('Var v) ts-  Ty ('Kon t)       tys          = t-  Ty (f ':@: x)     tys          = (Ty f tys) (Ty x tys)-  Ty (c ':&: d)     tys          = (Ty c tys, Ty d tys)+type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where+  Interpret ('Var 'VZ)     (t ':&&: ts) = t+  Interpret ('Var ('VS v)) (t ':&&: ts) = Interpret ('Var v) ts+  Interpret ('Kon t)       tys = t+  Interpret (f ':@: x)     tys = (Interpret f tys) (Interpret x tys)+  Interpret (c ':&: d)     tys = (Interpret c tys, Interpret d tys)+  Interpret (ForAll f)     tys = ForAllI f tys+  Interpret (c ':=>>: f)   tys = SuchThatI c f tys +newtype ForAllI (f :: Atom (d1 -> d) (*)) (tys :: LoT d) where+  ForAllI :: (forall t. Interpret f (t ':&&: tys)) -> ForAllI f tys++newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d (*)) (tys :: LoT d) where+  SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys+ type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where   Satisfies '[]       tys = ()-  Satisfies (c ': cs) tys = (Ty c tys, Satisfies cs tys)+  Satisfies (c ': cs) tys = (Interpret c tys, Satisfies cs tys)++type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where+  ContainsTyVar v (Var v)     = 'True+  ContainsTyVar v (Var w)     = 'False+  ContainsTyVar v (Kon t)     = 'False+  ContainsTyVar v (f :@: x)   = Or (ContainsTyVar v f) (ContainsTyVar v x)+  ContainsTyVar v (x :&: y)   = Or (ContainsTyVar v x) (ContainsTyVar v y)+  ContainsTyVar v (c :=>>: f) = Or (ContainsTyVar v c) (ContainsTyVar v f)+  ContainsTyVar v (ForAll f)  = ContainsTyVar (VS v) f++type family Or (x :: Bool) (y :: Bool) :: Bool where+  Or True  thing = True+  Or thing True  = True+  Or False False = False