kind-apply 0.3.2.1 → 0.4.0.0

raw patch · 3 files changed

+60/−16 lines, 3 filesdep +first-class-familiesPVP ok

version bump matches the API change (PVP)

Dependencies added: first-class-families

API changes (from Hackage documentation)

Files

• kind-apply.cabal +2/−1
• src/Data/PolyKinded.hs +13/−13
• src/Data/PolyKinded/Atom.hs +45/−2

@@ -1,6 +1,6 @@ cabal-version:       >=1.10 name:                kind-apply-version:             0.3.2.1+version:             0.4.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:@@ -24,6 +24,7 @@   -- other-modules:   -- other-extensions:   build-depends:       base >=4.12 && <5+                     , first-class-families >= 0.8 && < 0.9   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall

@@ -1,13 +1,13 @@-{-# language ConstraintKinds       #-}-{-# language FlexibleContexts      #-}-{-# language FlexibleInstances     #-}-{-# language GADTs                 #-}-{-# language MultiParamTypeClasses #-}-{-# language ScopedTypeVariables   #-}-{-# language TypeFamilies          #-}-{-# language TypeInType            #-}-{-# language TypeOperators         #-}-{-# language UndecidableInstances  #-}+{-# language ConstraintKinds        #-}+{-# language FlexibleContexts       #-}+{-# language FlexibleInstances      #-}+{-# language GADTs                  #-}+{-# language MultiParamTypeClasses  #-}+{-# language ScopedTypeVariables    #-}+{-# language TypeFamilyDependencies #-}+{-# language TypeInType             #-}+{-# language TypeOperators          #-}+{-# language UndecidableInstances   #-} -- | Representation of types as constructor + list of types. module Data.PolyKinded (   -- * Lists of types and application@@ -65,9 +65,9 @@ -- 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 Type)      = 'LoT0+type family SpineLoT (tys :: LoT k) = (tys' :: LoT k) | tys' -> tys where+  SpineLoT (a ':&&: as) = a ':&&: SpineLoT as+  SpineLoT 'LoT0        = 'LoT0  data SLoT (l :: LoT k) where   SLoT0 :: SLoT 'LoT0

@@ -29,6 +29,7 @@ import           Data.Kind import           Data.PolyKinded import           GHC.Exts+import           Fcf.Core (Exp, Eval)  -- | Well-scoped de Bruijn representation of type variables. -- @TyVar d@ represents all the possible type variables which@@ -59,6 +60,45 @@ -- -- >>> :kind Kon [] :@: Var0 -- the type [a] for unknown a -- Kon [] :@: Var0 :: Atom (* -> xs) *+--+-- === __Representation of type families__+--+-- Type families are represented using+-- <https://hackage.haskell.org/package/first-class-families first-class-families>.+--+-- For example, the type-level @n + m :: 'GHC.TypeNats.Nat'@-- may expand to the following--+--+-- @+-- n + m         -- using @('GHC.TypeNats.+')@ from "GHC.TypeNats"+-- ~+-- 'Fcf.Core.Eval' (n 'Fcf.Data.Nat.+' m)  -- using 'Fcf.Core.Eval' from "Fcf.Core" and @('Fcf.Data.Nat.+')@ from "Fcf.Data.Nat"+-- @+--+-- which may be encoded as the following 'Atom' (using 'Var0' for @n@ and 'Var1' for @m@):+--+-- @+-- 'Data.PolyKinded.Atom.Eval' (('Kon' ('Fcf.Data.Nat.+') ':@:' 'Var0') ':@:' 'Var1')  -- 'Data.PolyKinded.Atom.Eval' as 'Atom'\'s constructor+--   :: 'Atom' (Nat -> Nat -> Type) Nat+-- @+--+-- <https://hackage.haskell.org/package/kind-generics kind-generics>+-- uses a different, more systematic encoding of type families for @GenericK@ instances;+-- see <https://hackage.haskell.org/package/fcf-family fcf-family> for more details.+-- For example, @n + m@ is instead expanded to the following:+--+-- @+-- n + m+-- ~+-- 'Fcf.Core.Eval' ('Fcf.Family.NDFamily' ('Fcf.Family.MkName' "base" \"GHC.TypeNats\" \"+\") 'Fcf.Family.P0' \'(n, \'(m, \'())))+-- @+--+-- which gets encoded as the following 'Atom':+--+-- @+-- 'Data.PolyKinded.Atom.Eval' ('Kon' ('Fcf.Family.NDFamily' ('Fcf.Family.MkName' "base" \"GHC.TypeNats\" \"+\") 'Fcf.Family.P0')+--         ':@:' (('Kon' \'(,) ':@:' 'Var0') ':@:' (('Kon' \'(,) ':@:' 'Var1') ':@:' 'Kon' \'())))+--   :: 'Atom' (Nat -> Nat -> Type) Nat+-- @ data Atom (d :: Type) (k :: TYPE r) where   -- | Represents a type variable.   Var :: TyVar d k -> Atom d k@@ -72,6 +112,8 @@   ForAll  :: Atom (d1 -> d) Type -> Atom d Type   -- | Represents constraint requirement, the "thick arrow" @=>@.   (:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type+  -- | Represents a type family application.+  Eval :: Atom d (Exp k) -> Atom d k  -- | Represents an applied constructor. -- Instead of @Kon [] :@: Var0$ you can write @[] :$: Var0$.@@ -108,6 +150,7 @@   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 ('Eval f)    tys = Eval (Interpret f tys)  -- | Auxiliary type for interpretation of the 'ForAll' atom. -- Required because a type family like 'Interpret' cannot return@@ -132,9 +175,9 @@ -- Required because a type family like 'Interpret' cannot return -- a type with constraints. newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d Type) (tys :: LoT d) where-  SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys+  SuchThatI :: { unSuchThatI :: Interpret c tys => Interpret f tys } -> SuchThatI c f tys --- | Interprets a list of 'Atoms' representing constraints+-- | Interprets a list of 'Atom' representing constraints -- into the actual constraints. This is a specialization of -- 'Interpret' for the case of constraints. --