packages feed

kind-apply 0.3.0.0 → 0.3.1.0

raw patch · 3 files changed

+38/−8 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Data.PolyKinded: Proxy :: Proxy
+ Data.PolyKinded: [SLoT0] :: SLoT LoT0
+ Data.PolyKinded: [SLoTA] :: Proxy t -> SLoT ts -> SLoT (t :&&: ts)
+ Data.PolyKinded: class SForLoT (l :: LoT k)
+ Data.PolyKinded: data SLoT (l :: LoT k)
+ Data.PolyKinded: data Proxy (t :: k) :: forall k. () => k -> Type
+ Data.PolyKinded: instance Data.PolyKinded.SForLoT 'Data.PolyKinded.LoT0
+ Data.PolyKinded: instance forall k ks (ts :: Data.PolyKinded.LoT ks) (t :: k). Data.PolyKinded.SForLoT ts => Data.PolyKinded.SForLoT (t 'Data.PolyKinded.:&&: ts)
+ Data.PolyKinded: slot :: SForLoT l => SLoT l
+ Data.PolyKinded.Atom: WrapI :: Interpret f tys -> WrappedI
+ Data.PolyKinded.Atom: [unwrapI] :: WrappedI -> Interpret f tys
+ Data.PolyKinded.Atom: fromWrappedI :: forall f tys. (forall t. WrappedI f (t :&&: tys)) -> ForAllI f tys
+ Data.PolyKinded.Atom: newtype WrappedI (f :: Atom d (*)) (tys :: LoT d)
+ Data.PolyKinded.Atom: toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t :&&: tys)

Files

kind-apply.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-apply-version:             0.3.0.0+version:             0.3.1.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:
src/Data/PolyKinded.hs view
@@ -14,10 +14,14 @@ module Data.PolyKinded (   -- * Lists of types and application   LoT(..), (:@@:), LoT1, LoT2+  -- ** Singleton for list of types+, SLoT(..), SForLoT(..), Proxy(..)   -- * Splitting types , SplitF, Nat(..), TyEnv(..), SplitN ) where +import Data.Proxy+ infixr 5 :&&: -- | @LoT k@ represents a list of types which can be applied -- to a data type of kind @k@.@@ -37,6 +41,17 @@ type family (f :: k) :@@: (tys :: LoT k) :: * where   f :@@: 'LoT0        = f   f :@@: (a ':&&: as) = f a :@@: as++data SLoT (l :: LoT k) where+  SLoT0 :: SLoT LoT0+  SLoTA :: Proxy t -> SLoT ts -> SLoT (t :&&: ts)++class SForLoT (l :: LoT k) where+  slot :: SLoT l+instance SForLoT LoT0 where+  slot = SLoT0+instance SForLoT ts => SForLoT (t :&&: ts) where+  slot = SLoTA Proxy slot  -- | Split a type @t@ until the constructor @f@ is found. --
src/Data/PolyKinded/Atom.hs view
@@ -7,6 +7,9 @@ {-# language RankNTypes      #-} {-# language AllowAmbiguousTypes  #-} {-# language UndecidableInstances #-}+{-# language ScopedTypeVariables  #-}+{-# language TypeApplications     #-}+{-# language ImpredicativeTypes   #-} module Data.PolyKinded.Atom where  import Data.Kind@@ -43,17 +46,29 @@ type a :~:  b = 'Kon (~) ':@: a ':@: b type a :~~: b = 'Kon (~~) ':@: a ':@: b +type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where+  InterpretVar 'VZ     (t ':&&: ts) = t+  InterpretVar ('VS v) (t ':&&: ts) = InterpretVar v ts+ 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+  Interpret ('Var v)     tys = InterpretVar v tys+  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 WrappedI (f :: Atom d (*)) (tys :: LoT d) =+  WrapI { unwrapI :: Interpret f tys }++toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t ':&&: tys)+toWrappedI (ForAllI x) = WrapI (x @t)++fromWrappedI :: forall f tys. (forall t. WrappedI f (t ':&&: tys)) -> ForAllI f tys+fromWrappedI = coerce @(forall t. WrappedI f (t ':&&: 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