kind-apply 0.4.0.0 → 0.4.0.1

raw patch · 4 files changed

+60/−20 lines, 4 filesnew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +22/−0
• kind-apply.cabal +4/−3
• src/Data/PolyKinded.hs +23/−12
• src/Data/PolyKinded/Atom.hs +11/−5

@@ -0,0 +1,22 @@+# Revision history for `kind-apply`
+
+## 0.4.0.1 - 2025-07-29
+
+Tidying:
+
+* Replace deprecated `TypeInType` with `PolyKinds` and `DataKinds`
+* Fix doctests
+
+## 0.4.0.0
+
+## 0.3.2.1
+
+## 0.3.2.0
+
+## 0.3.1.0
+
+## 0.3.0.0
+
+## 0.2.0.0
+
+## 0.1.0.0

@@ -1,16 +1,17 @@ cabal-version:       >=1.10 name:                kind-apply-version:             0.4.0.0+version:             0.4.0.1 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:+bug-reports:         https://gitlab.com/trupill/kind-generics/issues license:             BSD3 license-file:        LICENSE author:              Alejandro Serrano-maintainer:          trupill@gmail.com+maintainer:          lysxia@gmail.com -- copyright: category:            Data build-type:          Simple+extra-source-files:  CHANGELOG.md  source-repository head   type:     git

@@ -1,11 +1,12 @@ {-# language ConstraintKinds        #-} {-# language FlexibleContexts       #-} {-# language FlexibleInstances      #-}+{-# language DataKinds              #-} {-# language GADTs                  #-} {-# language MultiParamTypeClasses  #-}+{-# language PolyKinds              #-} {-# language ScopedTypeVariables    #-} {-# language TypeFamilyDependencies #-}-{-# language TypeInType             #-} {-# language TypeOperators          #-} {-# language UndecidableInstances   #-} -- | Representation of types as constructor + list of types.@@ -22,6 +23,9 @@ import           Data.Kind import           Data.Proxy +-- $setup+-- >>> :set -XTypeOperators -XDataKinds -XNoStarIsType+ infixr 5 :&&: -- | @LoT k@ represents a list of types which can be applied -- to a data type of kind @k@.@@ -39,7 +43,8 @@ -- | Apply a list of types to a type constructor. -- -- >>> :kind! Either :@@: (Int :&&: Bool :&&: LoT0)--- Either Int Bool :: Type+-- Either :@@: (Int :&&: Bool :&&: LoT0) :: Type+-- = Either Int Bool type family (f :: k) :@@: (tys :: LoT k) :: Type where   f :@@: _  = f   f :@@: as = f (HeadLoT as) :@@: TailLoT as@@ -47,14 +52,16 @@ -- | Head of a non-empty list of types. -- -- >>> :kind! HeadLoT (Int :&&: LoT0)--- Int :: Type+-- HeadLoT (Int :&&: LoT0) :: Type+-- = 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)+-- TailLoT (Int :&&: Bool :&&: LoT0) :: LoT (Type -> Type)+-- = Bool :&&: LoT0 type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where   TailLoT (_ ':&&: as) = as @@ -83,9 +90,11 @@ -- | Split a type @t@ until the constructor @f@ is found. -- -- >>> :kind! SplitF (Either Int Bool) Either--- Int :&&: Bool :&&: LoT0 :: LoT (Type -> Type -> Type)+-- SplitF (Either Int Bool) Either :: LoT (Type -> Type -> Type)+-- = Int :&&: (Bool :&&: LoT0) -- >>> :kind! SplitF (Either Int Bool) (Either Int)--- Bool :&&: LoT0 :: LoT (Type -> Type)+-- SplitF (Either Int Bool) (Either Int) :: LoT (Type -> Type)+-- = Bool :&&: LoT0 type SplitF (t :: d) (f :: k) = SplitF' t f 'LoT0 type family SplitF' (t :: d) (f :: k) (p :: LoT l) :: LoT k where   SplitF' f     f acc = acc@@ -100,12 +109,14 @@  -- | Split a type @t@ until its list of types has length @n@. ----- >>> :kind! SplitN (Either Int Bool) (S (S Z))--- TyEnv Either (Int :&&: Bool :&&: LoT0) :: TyEnv--- >>> :kind! SplitF (Either Int Bool) (S Z)--- TyEnv (Either Int) (Bool :&&: LoT0) :: TyEnv+-- >>> :kind! SplitN (S (S Z)) (Either Int Bool)+-- SplitN (S (S Z)) (Either Int Bool) :: TyEnv+-- = 'TyEnv Either (Int :&&: (Bool :&&: LoT0))+-- >>> :kind! SplitN (S Z) (Either Int Bool)+-- SplitN (S Z) (Either Int Bool) :: TyEnv+-- = 'TyEnv (Either Int) (Bool :&&: LoT0) type family SplitN (n :: Nat) t :: TyEnv where   SplitN n t = SplitN' n t 'LoT0 type family SplitN' (n :: Nat) (t :: d) (p :: LoT d) :: TyEnv where-  SplitN' 'Z     t            acc = 'TyEnv t acc-  SplitN' ('S n) (t (a :: l)) acc = SplitN' n t (a ':&&: acc)+  SplitN' 'Z     t     acc = 'TyEnv t acc+  SplitN' ('S n) (t a) acc = SplitN' n t (a ':&&: acc)

@@ -31,6 +31,10 @@ import           GHC.Exts import           Fcf.Core (Exp, Eval) +-- $setup+-- >>> :set -XTypeOperators -XDataKinds -XNoStarIsType+-- >>> import Data.PolyKinded+ -- | Well-scoped de Bruijn representation of type variables. -- @TyVar d@ represents all the possible type variables which -- can refer to the holes in kind @d@.@@ -58,8 +62,9 @@ infixr 5 :=>>: -- | Shape of a type, possibly with type variables. ----- >>> :kind Kon [] :@: Var0 -- the type [a] for unknown a--- Kon [] :@: Var0 :: Atom (* -> xs) *+-- >>> -- the type [a] for unknown a+-- >>> :kind Kon [] :@: Var0+-- Kon [] :@: Var0 :: Atom (Type -> xs) Type -- -- === __Representation of type families__ --@@ -127,10 +132,10 @@ -- by the type variable @t@. -- -- >>> :kind! Interpret Var0 (LoT2 Int Bool)--- Interpret Var0 (LoT2 Int Bool) :: *+-- Interpret Var0 (LoT2 Int Bool) :: Type -- = Int -- >>> :kind! Interpret Var1 (LoT2 Int Bool)--- Interpret Var1 (LoT2 Int Bool) :: *+-- Interpret Var1 (LoT2 Int Bool) :: Type -- = Bool type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where   InterpretVar 'VZ     tys = HeadLoT tys@@ -141,7 +146,7 @@ -- must match statically those required by the 'Atom'. -- -- >>> :kind! Interpret ([] :$: Var0) (LoT1 Int)--- Interpret ([] :$: Var0) (LoT1 Int) :: *+-- Interpret ([] :$: Var0) (LoT1 Int) :: Type -- = [Int] type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where   Interpret ('Var v)     tys = InterpretVar v tys@@ -162,6 +167,7 @@ -- -- >>> :t WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int) -- WrapI [1] :: WrappedI ([] :$: Var0) (LoT1 Int)+--   :: WrappedI ([] :$: Var0) (LoT1 Int) newtype WrappedI (f :: Atom d Type) (tys :: LoT d) =   WrapI { unwrapI :: Interpret f tys }