packages feed

haskus-utils-types (empty) → 1.0

raw patch · 6 files changed

+548/−0 lines, 6 filesdep +base

Dependencies added: base

Files

+ CHANGES view
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2013-2017, Haskus organization+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 Sylvain Henry 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 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.
+ haskus-utils-types.cabal view
@@ -0,0 +1,32 @@+name: haskus-utils-types+version: 1.0+cabal-version: >=1.20+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: Sylvain Henry 2018+maintainer: sylvain@haskus.fr+homepage: http://www.haskus.org+synopsis: Haskus utility modules+description:+    Haskus types utility modules+category: System+author: Sylvain Henry+extra-source-files:+    CHANGES++source-repository head+    type: git+    location: git://github.com/haskus/haskus-utils.git++library+    exposed-modules:+        Haskus.Utils.Types+        Haskus.Utils.Types.List+        Haskus.Utils.Types.Generics+    build-depends:+        base >=4.9 && <4.12+    default-language: Haskell2010+    hs-source-dirs: src/lib+    ghc-options: -Wall+
+ src/lib/Haskus/Utils/Types.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE PolyKinds #-}++-- | Common type functions+module Haskus.Utils.Types+   ( Nat+   , Symbol+   , natValue+   , natValue'+   , symbolValue+   , KnownNat+   , KnownSymbol+   , CmpNat+   , CmpSymbol+   , type (<=?)+   , type (<=)+   , type (+)+   , type (-)+   , type (*)+   , type (^)+   , Assert+   , If+   , Modulo+   , Same+   , Proxy (..)+   , TypeError+   , ErrorMessage (..)+   )+where++import GHC.TypeLits+import Data.Proxy++-- | Get a Nat value+natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a+{-# INLINE natValue #-}+natValue = fromIntegral (natVal (Proxy :: Proxy n))++-- | Get a Nat value+natValue' :: forall (n :: Nat). KnownNat n => Word+{-# INLINE natValue' #-}+natValue' = natValue @n++-- | Get a Symbol value+symbolValue :: forall (s :: Symbol). (KnownSymbol s) => String+{-# INLINE symbolValue #-}+symbolValue = symbolVal (Proxy :: Proxy s)++-- | If-then-else+type family If (c :: Bool) (t :: k) (e :: k) where+   If 'True  t e = t+   If 'False t e = e+++-- | Like: If cond t (TypeError msg)+--+-- The difference is that the TypeError doesn't appear in the RHS of the type+-- which lead to better error messages (see GHC #14771).+--+-- For instance:+--    type family F n where+--       F n = If (n <=? 8) Int8 (TypeError (Text "ERROR"))+--+--    type family G n where+--       G n = Assert (n <=? 8) Int8 (Text "ERROR")+--+--    If GHC cannot solve `F n ~ Word`, it shows: ERROR+--    If GHC cannot solve `G n ~ Word`, it shows:+--       can't match `Assert...` with `Word`+--+type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) where+   Assert 'True  val msg = val+   Assert 'False val msg = TypeError msg++-- | Modulo+type family Modulo (a :: Nat) (b :: Nat) where+   Modulo a b = Modulo' (a <=? b) a b++-- | Helper for Modulo+type family Modulo' c a b where+   Modulo' 'True  a b = a+   Modulo' 'False a b = Modulo' ((a-b) <=? b) (a-b) b++-- | Type equality to Nat+type family Same a b :: Nat where+   Same a a = 1+   Same a b = 0
+ src/lib/Haskus/Utils/Types/Generics.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE UndecidableInstances #-}++-- | Generics+module Haskus.Utils.Types.Generics+   ( module GHC.Generics+   -- * Fields+   , Field+   , FieldType+   , LookupField+   , LookupFieldType+   -- * Data type fields+   , ExtractFields+   , ExtractFieldTypes+   )+where++import Haskus.Utils.Types.List+import Haskus.Utils.Types+import GHC.Generics++-- | Named field+data Field (name :: Symbol) (t :: *)++type family FieldType f where+   FieldType (Field name t) = t++type family LookupFieldType fs s where+   LookupFieldType fs s = FieldType (LookupField fs s)++type family LookupField (fs :: [*]) (s :: Symbol) where+   LookupField (Field name t ': fs) name = Field name t+   LookupField (Field name t ': fs) s    = LookupField fs s+   LookupField '[]                  name =+      TypeError ('Text "Cannot find field with name: " ':<>: 'ShowType name)+++-- | Extract fields of a data type:+--    - require selector symbols+--    - only support data type with a single constructor+type family ExtractFields (a :: *)  where+   ExtractFields a = ExtractFields' (Rep a)++type family ExtractFields' a where+   -- extract constructors+   ExtractFields' (D1 _ cs)   = ExtractFields' cs++   -- extract selectors+   ExtractFields' (C1 _ ss)   = ExtractFields' ss+   ExtractFields' (s1 :*: s2) = Concat (ExtractFields' s1) (ExtractFields' s2)++   -- extract field name and type from the selector+   ExtractFields' (S1 ('MetaSel ('Just name) _ _ _) (Rec0 t)) = '[Field name t]++++-- | Extract types of the fields of a data type+--    - only support data type with a single constructor+type family ExtractFieldTypes (a :: *)  where+   ExtractFieldTypes a = ExtractFieldTypes' (Rep a)++type family ExtractFieldTypes' a where+   -- extract constructors+   ExtractFieldTypes' (D1 _ cs)   = ExtractFieldTypes' cs++   -- extract selectors+   ExtractFieldTypes' (C1 _ ss)   = ExtractFieldTypes' ss+   ExtractFieldTypes' (s1 :*: s2) =+      Concat (ExtractFieldTypes' s1) (ExtractFieldTypes' s2)++   -- extract field type from the selector+   ExtractFieldTypes' (S1 _ (Rec0 t)) = '[t]
+ src/lib/Haskus/Utils/Types/List.hs view
@@ -0,0 +1,321 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds #-}++-- | Utils for type lists+module Haskus.Utils.Types.List+   ( Map+   , Max+   , Tail+   , Drop+   , Take+   , Init+   , Head+   , Snoc+   , InsertAt+   , ReplaceAt+   , Replace+   , ReplaceN+   , ReplaceNS+   , Reverse+   , RemoveAt+   , RemoveAt1+   , RemoveAtN+   , Concat+   , Length+   , Replicate+   , Generate+   , IsMember+   , IsSubset+   , Indexes+   , MapTest+   , Zip+   , Filter+   , Nub+   , NubHead+   , IndexOf+   , IndexesOf+   , MaybeIndexOf+   , Index+   , Union+   , Product+   , Member+   , Member'+   , CheckNub+   )+where++import Haskus.Utils.Types++-- | Map a type function+type family Map (f :: a -> k) (xs :: [a]) :: [k] where+   Map f '[]       = '[]+   Map f (x ': xs) = f x ': Map f xs++-- | Get the max of a list of Nats+type family Max (xs :: [Nat]) where+   Max (x ': xs) = Max' x xs++-- | Helper for Max+type family Max' (x :: Nat) (xs :: [Nat]) where+   Max' x '[]       = x+   Max' x (a ': xs) = Max' (If (x <=? a) a x) xs++-- | Tail of a list+type family Tail (xs :: [k]) :: [k] where+   Tail (x ': xs) = xs++-- | Drop elements in a list+type family Drop (n :: Nat) (xs :: [k]) :: [k] where+   Drop 0 xs        = xs+   Drop n (x ': xs) = Drop (n-1) xs++-- | Take elements in a list+type family Take (n :: Nat) (xs :: [k]) :: [k] where+   Take 0 xs        = '[]+   Take n (x ': xs) = x ': (Take (n-1) xs)++-- | Init of a list+type family Init (xs :: [k]) ::  [k] where+   Init '[x]      = '[]+   Init (x ': xs) = x ': (Init xs)++-- | Snoc+type family Snoc (xs :: [k]) (x :: k) :: [k] where+   Snoc '[] x       = '[x]+   Snoc (y ': ys) x = y ': (Snoc ys x)++-- | Head of a list+type family Head (xs :: [k]) :: k where+   Head (x ': xs) = x++-- | Concat two type lists+type family Concat (xs :: [k]) (ys :: [k]) :: [k] where+   Concat '[] '[]      = '[]+   Concat '[] ys       = ys+   Concat (x ': xs) ys = x ': Concat xs ys++-- | Get list length+type family Length (xs :: [k]) :: Nat where+   Length xs = Length' 0 xs++type family Length' n (xs :: [k]) :: Nat where+   Length' n '[]       = n+   Length' n (x ': xs) = Length' (n+1) xs++-- | Replicate+type family Replicate (n :: Nat) (s :: k) :: [k] where+   Replicate n s = Replicate' s n '[]++type family Replicate' (x :: k) (n :: Nat) (xs :: [k]) :: [k] where+   Replicate' x 0 xs = xs+   Replicate' x n xs = Replicate' x (n-1) (x ': xs)++-- | Insert a list at n+type family InsertAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where+   InsertAt 0 xs ys        = Concat ys xs+   InsertAt n (x ': xs) ys = x ': InsertAt (n-1) xs ys++-- | replace l[n] with l2 (folded)+type family ReplaceAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where+   ReplaceAt 0 (x ': xs) ys = Concat ys xs+   ReplaceAt n (x ': xs) ys = x ': ReplaceAt (n-1) xs ys++-- | replace a type by another in l+type family Replace (t1 :: k) (t2 :: k) (l :: [k]) :: [k] where+   Replace t1 t2 '[]        = '[]+   Replace t1 t2 (t1 ': xs) = t2 ': (Replace t1 t2 xs)+   Replace t1 t2 (x ': xs)  = x ': (Replace t1 t2 xs)++-- | replace a type at offset n in l+type family ReplaceN (n :: Nat) (t :: k) (l :: [k]) :: [k] where+   ReplaceN 0 t (x ': xs)  = (t ': xs)+   ReplaceN n t (x ': xs)  = x ': ReplaceN (n-1) t xs++-- | replace types at offsets ns in l+type family ReplaceNS (ns :: [Nat]) (t :: k) (l :: [k]) :: [k] where+   ReplaceNS '[] t l       = l+   ReplaceNS (i ': is) t l = ReplaceNS is t (ReplaceN i t l)++-- | Reverse a list+type family Reverse (l :: [k]) :: [k] where+   Reverse l = Reverse' l '[]++type family Reverse' (l :: [k]) (l2 :: [k]) :: [k]  where+   Reverse' '[] l       = l+   Reverse' (x ': xs) l = Reverse' xs (x ': l)+++-- | Remove a type at index+type family RemoveAt (n :: Nat) (l :: [k]) :: [k] where+   RemoveAt 0 (x ': xs) = xs+   RemoveAt n (x ': xs) = x ': RemoveAt (n-1) xs++-- | Remove a type at index (0 == don't remove)+type family RemoveAt1 (n :: Nat) (l :: [k]) :: [k]  where+   RemoveAt1 0 xs        = xs+   RemoveAt1 1 (x ': xs) = xs+   RemoveAt1 n (x ': xs) = x ': RemoveAt1 (n-1) xs++-- | Remove types at several indexes+type family RemoveAtN (ns :: [Nat]) (l :: [k]) :: [k]  where+   RemoveAtN '[] xs       = xs+   RemoveAtN (i ': is) xs = RemoveAtN is (RemoveAt i xs)++-- | Generate a list of Nat [n..m-1]+type family Generate (n :: Nat) (m :: Nat) :: [Nat] where+   Generate n n = '[]+   Generate n m = n ': Generate (n+1) m++-- | Check that a type is member of a type list+type family IsMember (a :: k) (l :: [k]) :: Bool where+   IsMember a l = IsMember' l a l++-- | Helper for IsMember+type family IsMember' (i :: [k]) (a :: k) (l :: [k]) :: Bool where+   IsMember' i a (a ': l) = 'True+   IsMember' i a (b ': l) = IsMember' i a l+   IsMember' i a '[]      = TypeError ( 'Text "`"+                                   ':<>: 'ShowType a+                                   ':<>: 'Text "'"+                                   ':<>: 'Text " is not a member of "+                                   ':<>: 'ShowType i)+++-- | Check that a list is a subset of another+type family IsSubset (l1 :: [k]) (l2 :: [k]) :: Bool where+   IsSubset l1 l1 = 'True+   IsSubset l1 l2 = IsSubset' l2 l1 l2++-- | Helper for IsSubset+type family IsSubset' (i :: [k]) (l1 :: [k]) (l2 :: [k]) :: Bool where+   IsSubset' i '[] l2 = 'True+   IsSubset' i l1 '[] = TypeError (     'ShowType l1+                                   ':$$: 'Text "is not a subset of"+                                   ':$$: 'ShowType i)+   IsSubset' i (x ': xs) (x ': ys) = IsSubset' i xs i+   IsSubset' i (x ': xs) (y ': ys) = IsSubset' i (x ': xs) ys++-- | Get list indexes+type family Indexes (l :: [k]) :: [Nat] where+   Indexes xs      = IndexesFrom 0 xs++type family IndexesFrom (n :: Nat) (xs :: [k]) :: [Nat] where+   IndexesFrom n '[]       = '[]+   IndexesFrom n (x ': xs) = n ': IndexesFrom (n+1) xs++-- | Map to 1 if type equality, 0 otherwise+type family MapTest (a :: k) (l :: [k]) :: [Nat] where+   MapTest a '[]       = '[]+   MapTest a (a ': xs) = 1 ': MapTest a xs+   MapTest a (x ': xs) = 0 ': MapTest a xs++-- | Zip two lists+type family Zip (l :: [*]) (l2 :: [*]) where+   Zip '[] xs              = '[]+   Zip xs '[]              = '[]+   Zip (x ': xs) (y ': ys) = (x,y) ': Zip xs ys++-- | Remove `a` in `l`+type family Filter (a :: k) (l :: [k]) :: [k] where+   Filter a '[]       = '[]+   Filter a (a ': as) = Filter a as+   Filter a (b ': as) = b ': Filter a as++-- | Keep only a single value of each type+type family Nub (l :: [k]) :: [k] where+   Nub xs = Reverse (Nub' xs '[])++type family Nub' (as :: [k]) (xs :: [k]) :: [k] where+   Nub' '[]       xs = xs+   Nub' (x ': as) xs = Nub' (Filter x as) (x ': xs) ++-- | Keep only a single value of the head type+type family NubHead (l :: [k]) :: [k] where+   NubHead '[]       = '[]+   NubHead (x ': xs) = x ': Filter x xs++-- | Get the first index of a type+type family IndexOf (a :: k) (l :: [k]) :: Nat where+   IndexOf x xs = IndexOf' x xs xs++-- | Get the first index of a type+type family IndexOf' (a :: k) (l :: [k]) (l2 :: [k]) :: Nat where+   IndexOf' x (x ': xs) l2 = 0+   IndexOf' y (x ': xs) l2 = 1 + IndexOf' y xs l2++-- | Get all the indexes of a type+type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where+   IndexesOf x xs = IndexesOf' 0 x xs++-- | Get the first index of a type+type family IndexesOf' n (a :: k) (l :: [k]) :: [Nat] where+   IndexesOf' n x '[]       = '[]+   IndexesOf' n x (x ': xs) = n ': IndexesOf' (n+1) x xs+   IndexesOf' n x (y ': xs) = IndexesOf' (n+1) x xs++-- | Get the first index (starting from 1) of a type or 0 if none+type family MaybeIndexOf (a :: k) (l :: [k]) where+   MaybeIndexOf x xs = MaybeIndexOf' 0 x xs++-- | Helper for MaybeIndexOf+type family MaybeIndexOf' (n :: Nat) (a :: k) (l :: [k]) where+   MaybeIndexOf' n x '[]       = 0+   MaybeIndexOf' n x (x ': xs) = 1 + n+   MaybeIndexOf' n x (y ': xs) = MaybeIndexOf' (n+1) x xs++-- | Indexed access into the list+type family Index (n :: Nat) (l :: [k]) :: k where+   Index 0 (x ': xs) = x+   Index n (x ': xs) = Index (n-1) xs++-- | Union two lists+type family Union (xs :: [k]) (ys :: [k]) :: [k] where+   Union xs ys = Nub (Concat xs ys)++-- | Product of two lists+type family Product (xs :: [*]) (ys :: [*]) :: [*] where+   Product '[] ys    = '[]+   Product xy '[]    = '[]+   Product (x:xs) ys = Concat (Product' x ys) (Product xs ys)++type family Product' (x :: *) (ys :: [*]) :: [*] where+   Product' x '[]       = '[]+   Product' x (y ': ys) = (x,y) ': Product' x ys++--------------------------------------+-- Constraints+--------------------------------------++-- | Constraint: x member of xs+type Member x xs =+   ( IsMember x xs ~ 'True+   , x ~ Index (IndexOf x xs) xs+   , KnownNat (IndexOf x xs)+   )++-- | Constraint: x member of xs (silent)+type Member' x xs =+   ( x ~ Index (IndexOf x xs) xs+   , KnownNat (IndexOf x xs)+   )++-- | Check that a list only contain a value of each type+type CheckNub (l :: [k]) =+   ( CheckNubEx l (Nub l) ~ 'True+   )++type family CheckNubEx (l1 :: [k]) (l2 :: [k]) where+   CheckNubEx l l   = 'True+   CheckNubEx l1 l2 = TypeError+      ( 'Text "Type-list contains unallowed redundant types."+      ':$$: 'Text "Got: "      ':<>: 'ShowType l1+      ':$$: 'Text "Expected: " ':<>: 'ShowType l2+      )+