packages feed

kind-apply 0.3.1.0 → 0.3.2.0

raw patch · 3 files changed

+34/−7 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- 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: instance (l Data.Type.Equality.~ 'Data.PolyKinded.LoT0) => Data.PolyKinded.SForLoT l
+ Data.PolyKinded: instance forall k k' (l :: Data.PolyKinded.LoT (k -> k')) (t :: k) (ts :: Data.PolyKinded.LoT k'). (l Data.Type.Equality.~ (t 'Data.PolyKinded.:&&: ts), Data.PolyKinded.SForLoT ts) => Data.PolyKinded.SForLoT l

Files

kind-apply.cabal view
@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-apply-version:             0.3.1.0+version:             0.3.2.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
@@ -7,6 +7,7 @@ {-# language PatternSynonyms #-} {-# language UndecidableInstances   #-} {-# language FlexibleContexts       #-}+{-# language FlexibleInstances      #-} {-# language ScopedTypeVariables    #-} {-# language MultiParamTypeClasses  #-} {-# language FunctionalDependencies #-}@@ -14,6 +15,7 @@ module Data.PolyKinded (   -- * Lists of types and application   LoT(..), (:@@:), LoT1, LoT2+, HeadLoT, TailLoT, SpineLoT   -- ** Singleton for list of types , SLoT(..), SForLoT(..), Proxy(..)   -- * Splitting types@@ -39,18 +41,43 @@ -- >>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0) -- Either Int Bool :: * type family (f :: k) :@@: (tys :: LoT k) :: * where-  f :@@: 'LoT0        = f-  f :@@: (a ':&&: as) = f a :@@: as+  f :@@: _  = f+  f :@@: as = f (HeadLoT as) :@@: (TailLoT as) +-- | Head of a non-empty list of types.+--+-- >>> :kind! HeadLoT (Int :&&: LoT0)+-- Int :: *+type family HeadLoT (tys :: LoT (k -> k')) :: k where+  HeadLoT (a :&&: _) = a++-- | Tail of a non-empty list of types.+--+-- >>> :kind! TailLoT (Int :&&: Bool :&&: LoT0)+-- Bool :&&: LoT0 :: LoT (Type -> Type)+type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where+  TailLoT (_ :&&: as) = as++-- | Construct the spine of a list of types whose length is known.+--+-- It can be useful to introduce unification variables for lists of types which+-- will be fully instantiated during constraint resolution.+-- A constraint @p ~ SpineLoT p@ will thus instantiate the spine of @p@.+--+-- On concrete lists, this is the identity function.+type family SpineLoT (ts :: LoT k) :: LoT k where+  SpineLoT (ts :: LoT (k -> k')) = HeadLoT ts :&&: SpineLoT (TailLoT ts)+  SpineLoT (ts :: LoT (*)) = LoT0+ 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+instance (l ~ LoT0) => SForLoT (l :: LoT (*)) where   slot = SLoT0-instance SForLoT ts => SForLoT (t :&&: ts) where+instance (l ~ (t :&&: ts), SForLoT ts) => SForLoT (l :: LoT (k -> k')) where   slot = SLoTA Proxy slot  -- | Split a type @t@ until the constructor @f@ is found.
src/Data/PolyKinded/Atom.hs view
@@ -47,8 +47,8 @@ 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+  InterpretVar 'VZ     tys = HeadLoT tys+  InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)  type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where   Interpret ('Var v)     tys = InterpretVar v tys