packages feed

kind-apply (empty) → 0.1.0.0

raw patch · 7 files changed

+251/−0 lines, 7 filesdep +basesetup-changed

Dependencies added: base

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2018, Alejandro Serrano++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Alejandro Serrano nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ kind-apply.cabal view
@@ -0,0 +1,29 @@+cabal-version:       >=1.10+name:                kind-apply+version:             0.1.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:+license:             BSD3+license-file:        LICENSE+author:              Alejandro Serrano+maintainer:          trupill@gmail.com+-- copyright:+category:            Data+build-type:          Simple++source-repository head+  type:     git+  location: https://gitlab.com/trupill/kind-generics.git++library+  exposed-modules:     Data.PolyKinded,+                       Data.PolyKinded.Atom,+                       Data.PolyKinded.Functor,+                       GHC.Generics.Extra+  -- other-modules:+  -- other-extensions:+  build-depends:       base >=4.12 && <5+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall
+ src/Data/PolyKinded.hs view
@@ -0,0 +1,74 @@+{-# language DataKinds       #-}+{-# language TypeOperators   #-}+{-# language GADTs           #-}+{-# language TypeFamilies    #-}+{-# language KindSignatures  #-}+{-# language TypeInType      #-}+{-# language PatternSynonyms #-}+{-# language UndecidableInstances   #-}+{-# language FlexibleContexts       #-}+{-# language ScopedTypeVariables    #-}+{-# language MultiParamTypeClasses  #-}+{-# language FunctionalDependencies #-}+{-# language ConstraintKinds        #-}+module Data.PolyKinded (+  -- * Lists of types and application+  LoT(..), (:@@:)+  -- * Splitting types+, SplitF, Nat(..), TyEnv(..), SplitN, Split+) where++infixr 5 :&&:+-- | @LoT k@ represents a list of types which can be applied+-- to a data type of kind @k@.+data LoT k where+  -- | Empty list of types.+  LoT0    ::                LoT (*)+  -- | Cons a type with a list of types.+  (:&&:)  :: k -> LoT ks -> LoT (k -> ks)++-- | Apply a list of types to a type constructor.+--+-- >>> :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++-- | Split a type @t@ until the constructor @f@ is found.+--+-- >>> :kind! SplitF (Either Int Bool) Either+-- Int :&&: Bool :&&: LoT0 :: LoT (* -> * -> *)+-- >>> :kind! SplitF (Either Int Bool) (Either Int)+-- Bool :&&: LoT0 :: LoT (* -> *)+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+  SplitF' (t a) f acc = SplitF' t f (a ':&&: acc)++-- | Simple natural numbers.+data Nat = Z | S Nat++-- | A type constructor and a list of types that can be applied to it.+data TyEnv where+  TyEnv :: forall k. k -> LoT k -> TyEnv++-- | 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+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)++-- | @Split t f x@ declares that the default way to split+-- the type @t@ is into a type constructor @f@ and a list+-- of types @x@.+--+-- > instance Split (Either a b) Either (a :&&: b :&&: LoT0)+class (x ~ SplitF t f, t ~ (f :@@: x))+      => Split t (f :: k) (x :: LoT k) | t -> k f x
+ src/Data/PolyKinded/Atom.hs view
@@ -0,0 +1,43 @@+{-# language GADTs           #-}+{-# language TypeOperators   #-}+{-# language TypeFamilies    #-}+{-# language DataKinds       #-}+{-# language PolyKinds       #-}+{-# language ConstraintKinds #-}+module Data.PolyKinded.Atom where++import Data.Kind+import Data.PolyKinded++data TyVar d k 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)))))))))++data Atom d k where+  Var    :: TyVar d k -> Atom d k+  Kon    :: k         -> Atom d k+  (:@:)  :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2++type f :$: x = 'Kon f ':@: x+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)++type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where+  Satisfies '[]       tys = ()+  Satisfies (c ': cs) tys = (Ty c tys, Satisfies cs tys)
+ src/Data/PolyKinded/Functor.hs view
@@ -0,0 +1,51 @@+{-# language DataKinds              #-}+{-# language PolyKinds              #-}+{-# language GADTs                  #-}+{-# language TypeOperators          #-}+{-# language MultiParamTypeClasses  #-}+{-# language ScopedTypeVariables    #-}+{-# language FunctionalDependencies #-}+{-# language TypeApplications       #-}+{-# language AllowAmbiguousTypes    #-}+{-# language TypeFamilies           #-}+-- | Poly-kinded 'Functor' type class.+-- 'KFunctor' generalizes functors, bifunctors, profunctors, ...+-- by declaring a list of 'Variance's for a type constructor.+module Data.PolyKinded.Functor where++import Data.PolyKinded++-- | Declares that the type constructor @f@ is a generalized+-- functor whose variances for each type argument are given by @v@.+class KFunctor (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k) | f -> v where+  -- | The generalized version of 'fmap', 'bimap', 'dimap', and so on.+  kfmap :: Mappings v as bs -> f :@@: as -> f :@@: bs++-- | The generalized version of 'fmap', 'bimap', 'dimap', and so on.+-- This version uses 'Split' to obtain better type inference.+kmapo :: forall t f v as bs. (Split t f as, KFunctor f v as bs)+      => Mappings v as bs -> t -> f :@@: bs+kmapo = kfmap @_ @f++-- ** Mappings of different variance++-- | Possible variances for each argument of a type constructor.+data Variance = Co       -- ^ The functor is covariant in this position.+              | Contra   -- ^ The functor is contravariant in this position.+              | Phantom  -- ^ This position is not used in any constructor.+type Variances = [Variance]++-- | If a 'KFunctor' needs to map an @f ... a ...@ to an @f ... b ...@,+-- a @Mapping v a b@ specifies which function needs to be provided+-- for that position depending on its variance @v@.+type family Mapping (v :: Variance) a b where+  Mapping 'Co      a b = a -> b+  Mapping 'Contra  a b = b -> a+  Mapping 'Phantom a b = ()++infixr 5 :^:+-- | List of mappings for the list of variances @v@.+data Mappings (v :: Variances) (x :: LoT k) (y :: LoT k) where+  M0    :: Mappings '[] 'LoT0 'LoT0+  (:^:) :: Mapping v a b -> Mappings vs as bs+        -> Mappings (v ': vs) (a ':&&: as) (b ':&&: bs)
+ src/GHC/Generics/Extra.hs view
@@ -0,0 +1,22 @@+{-# language KindSignatures  #-}+{-# language ConstraintKinds #-}+{-# language PolyKinds       #-}+{-# language GADTs           #-}+{-# language TypeOperators   #-}+-- | Extensions to the "GHC.Generics" module.+module GHC.Generics.Extra (+  module GHC.Generics+, (:=>:)(..)+) where++import Data.Kind+import GHC.Generics++-- | Constraints: used to represent constraints in a constructor.+--+-- > data Showable a = Show a => a -> X a+-- >+-- > instance Generic (Showable a) where+-- >   type Rep (Showable a) = (Show a) :=>: (K1 R a)+data (:=>:) (c :: Constraint) (f :: k -> *) (a :: k) where+  SuchThat :: c => f a -> (c :=>: f) a