packages feed

type-fun (empty) → 0.0.1

raw patch · 10 files changed

+424/−0 lines, 10 filesdep +basedep +type-funsetup-changed

Dependencies added: base, type-fun

Files

+ CHANGELOG.md view
@@ -0,0 +1,8 @@+# TODO+* Add doctests+* Add TyFun from singletons (or just depend from)?++# CHANGELOG++## 0.0.1+First version
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Aleksey Uimanov++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 Aleksey Uimanov 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
+ example/Main.hs view
@@ -0,0 +1,40 @@+module Main where++import Data.Proxy+import TypeFun.Data.List+import TypeFun.Data.Peano++-- | This function has wider constraint __Int is inside l__+elemConstr :: (Elem Int l) => proxy l -> Int+elemConstr p = 1++-- | This function has narrower constraint than 'elemConstr'+-- __Int and Bool are contained in l__+sublistConstr :: (SubList '[Int, Bool] l) => proxy l -> Int+sublistConstr p = elemConstr p + 1++-- | This function has narrower constraint than 'sublistConstr' (Order+-- of elements matters)+prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int+prefixConstr p = sublistConstr p + 1++-- | This function has narrower constraint+-- __Int is inside of l and it is a first argument__+-- and uses inside more wide function+indexConstr :: (('Just 'Z) ~ (IndexOfMay Int l)) => proxy l -> Int+indexConstr p = elemConstr p + 1++uniqConstr :: (UniqElements l) => proxy l -> Int+uniqConstr _ = 1++main :: IO ()+main = do+  let+    p2 = Proxy :: Proxy '[Int, Bool]+    p3 = Proxy :: Proxy '[Int, Bool, Int]+  print $ indexConstr p2+  print $ sublistConstr p2+  print $ prefixConstr p2+  print $ prefixConstr p3+  print $ uniqConstr p2+  -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]
+ src/TypeFun/Constraint.hs view
@@ -0,0 +1,10 @@+module TypeFun.Constraint+  ( AllSatisfy+  ) where++import GHC.Exts++-- | Apply constraint for each element of list+type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where+  AllSatisfy c '[]       = ()+  AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
+ src/TypeFun/Data/Eq.hs view
@@ -0,0 +1,7 @@+module TypeFun.Data.Eq+  ( Equal+  ) where++type family Equal (a :: k) (b :: k) :: Bool where+  Equal a a = 'True+  Equal a b = 'False
+ src/TypeFun/Data/List.hs view
@@ -0,0 +1,208 @@+-- | Collection of type families on type lists. This module differs+-- from __Data.Singletons.Prelude.List__ because works with __[*]__+-- and relies on GHC's type equality (~). The rest of required+-- operations like 'Reverse' or '(:++:)' you could find in singletons++module TypeFun.Data.List+  ( -- * Primitive operations on lists+    Length+  , Drop+  , Take+  , Delete+  , Remove+  , (:++:)+    -- * Elements lookup+  , IndexOf+  , IndexOfMay+  , IndexOfMay'+  , IndicesOfMay+  , IndicesOf+  , Index+  , IndexMay+  , IndicesMay+  , Indices+  , Elem+  , NotElem+  , Count+    -- * Operations with lists+  , SubList+  , NotSubList+  , IsPrefixOf+  , IsNotPrefixOf+  , IsPrefixOfBool+    -- * Set operations+  , Union+  , UnionList+  , AppendUniq+  , Intersect+    -- * Uniqueness checking+  , ElementIsUniq+  , UniqElements+  , UniqElements'+  ) where++import Data.Type.Bool+import GHC.Exts+import GHC.TypeLits+import TypeFun.Data.Eq+import TypeFun.Data.Maybe+import TypeFun.Data.Peano++------------------------------------------------------------------------+-- NOTE: Errors type classes. These type classes are not in separate  --+-- module because in this case user could import them and instantiate --+-- by mistake. The name of typeclass is an error message in fact. We  --+-- have not any way to fail constraint explicitly, so this hack was   --+-- introduced.                                                        --+------------------------------------------------------------------------++class ElementNotFoundInList a s++class ElementIsInList a s++class ListIsNotPrefixOf a b++class ListIsPrefixOf a b++class ElementIsNotUniqInList a s++class IndexNotFoundInList a s++----------------------+-- main module code --+----------------------+++type family Length (a :: [k]) :: N where+  Length '[] = 'Z+  Length (a ': as) = 'S (Length as)++type family Drop (c :: N) (s :: [k]) :: [k] where+  Drop 'Z     s         = s+  Drop ('S c) '[]       = '[]+  Drop ('S c) (a ': as) = Drop c as++type family Take (c :: N) (s :: [k]) :: [k] where+  Take 'Z     s         = '[]+  Take ('S c) '[]       = '[]+  Take ('S c) (a ': as) = a ': (Take c as)++-- | Remove first argument type from anywhere in a list.+type family Delete (a :: k) (s :: [k]) :: [k] where+  Delete a '[]       = '[]+  Delete a (a ': as) = Delete a as+  Delete a (b ': as) = b ': (Delete a as)++-- | Remove index from the list+type family Remove (i :: N) (a :: [k]) :: [k] where+  Remove i      '[]       = '[]+  Remove 'Z     (a ': as) = as+  Remove ('S i) (a ': as) = a ': (Remove i as)++type family (:++:) (a :: [k]) (b :: [k]) :: [k] where+  '[] :++: b = b+  (a ': as) :++: b = a ': (as :++: b)++type IndexOf a s = FromJust (IndexOfMay a s)++type IndexOfMay a s = IndexOfMay' Z a s++type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where+  IndexOfMay' acc a '[]       = 'Nothing+  IndexOfMay' acc a (a ': as) = 'Just acc+  IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as++type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where+  IndicesOfMay '[] bs = '[]+  IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)++type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where+  IndicesOf '[] bs = '[]+  IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)++type Index idx s = FromJust (IndexMay idx s)++type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where+  IndexMay idx     '[]       = 'Nothing+  IndexMay Z       (a ': as) = 'Just a+  IndexMay (S idx) (a ': as) = IndexMay idx as++type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where+  IndicesMay '[] as = '[]+  IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)++type family Indices (idxs :: [N]) (a :: [k]) :: [k] where+  Indices '[]         as = '[]+  Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)++-- | Generates unresolvable constraint if fists element is not+-- contained inside of second+type Elem a s = NothingToConstr (IndexOfMay a s)+                                (ElementNotFoundInList a s)++-- | Reverse of 'Elem'+type NotElem a s = JustToConstr (IndexOfMay a s)+                                (ElementIsInList a s)++-- | Count elements in a list+type family Count (a :: k) (s :: [k]) :: N where+  Count a '[]       = 'Z+  Count a (a ': as) = 'S (Count a as)+  Count a (b ': as) = Count a as++-- | Constanints that first argument is a sublist of second. Reduces+-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__+type family SubList (a :: [k]) (b :: [k]) :: Constraint where+  SubList '[]       bs = ()+  SubList (a ': as) bs = (Elem a bs, SubList as bs)++type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where+  NotSubList '[]       bs = ()+  NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)++type IsPrefixOf a b = ( If (IsPrefixOfBool a b)+                           (() :: Constraint)+                           (ListIsNotPrefixOf a b)+                      , SubList a b )++type IsNotPrefixOf a b = If (IsPrefixOfBool a b)+                            (ListIsPrefixOf a b)+                            (() :: Constraint)++-- | First argument is prefix of second+type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where+  IsPrefixOfBool '[]       b         = 'True+  IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs+  IsPrefixOfBool as        bs        = 'False++-- | Appends elements from first list to second if they are not+-- presented in.+type family Union (a :: [k]) (b :: [k]) :: [k] where+  Union '[]       bs = bs+  Union (a ': as) bs = Union as (AppendUniq a bs)++type family UnionList (l :: [[k]]) :: [k] where+  UnionList '[]       = '[]+  UnionList (a ': as) = Union a (UnionList as)++-- | Append element to list if element is not already presented in+type family AppendUniq (a :: k) (s :: [k]) :: [k] where+  AppendUniq a (a ': bs) = a ': bs+  AppendUniq a (b ': bs) = b ': (AppendUniq a bs)+  AppendUniq a '[]       = '[a]++-- | Calculates intersection between two lists. Order of elements is+-- taken from first list+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)++-- | Checks that element 'a' occurs in a list just once+type ElementIsUniq a s = If (Equal (S Z) (Count a s))+                            (() :: Constraint)+                            (ElementIsNotUniqInList a s)++-- | Checks that all elements in list are unique+type UniqElements a = UniqElements' a a++type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where+  UniqElements' '[]       self = ()+  UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
+ src/TypeFun/Data/Maybe.hs view
@@ -0,0 +1,32 @@+module TypeFun.Data.Maybe+  ( MaybeCase+  , NothingToConstr+  , JustToConstr+  , CatMaybes+  , FromJust+  ) where++import GHC.Exts++type family MaybeCase (a :: Maybe k)+                      (nothing :: r)+                      (just :: k -> r) :: r where+  MaybeCase 'Nothing nothing just  = nothing+  MaybeCase ('Just k) nothing just = just k++type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where+  NothingToConstr 'Nothing  c = c+  NothingToConstr ('Just a) c = ()++type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where+  JustToConstr 'Nothing  c = ()+  JustToConstr ('Just a) c = c++-- | Like 'catMaybes' for type lists+type family CatMaybes (l :: [Maybe k]) :: [k] where+  CatMaybes '[]               = '[]+  CatMaybes (('Just a) ': as) = a ': (CatMaybes as)+  CatMaybes ('Nothing ': as)  = CatMaybes as++type family FromJust (a :: Maybe k) :: k where+  FromJust ('Just a) = a
+ src/TypeFun/Data/Peano.hs view
@@ -0,0 +1,37 @@+module TypeFun.Data.Peano+  ( N(..)+  , ToNat+  , FromNat+  , (:+:)+  , (:-:)+  , (:*:)+  ) where++import Data.Typeable+import GHC.Generics (Generic)+import GHC.TypeLits++data N = Z | S N+         deriving ( Eq, Ord, Read, Show+                  , Generic, Typeable )++type family ToNat (a :: N) :: Nat where+  ToNat Z = 0+  ToNat (S a) = 1 + (ToNat a)++type family FromNat (a :: Nat) :: N where+  FromNat 0 = Z+  FromNat a = S (FromNat (a - 1))++type family (:+:) (a :: N) (b :: N) :: N where+  Z :+: b = b+  (S a) :+: b = a :+: (S b)++type family (:-:) (a :: N) (b :: N) :: N where+  a :-: Z = a+  (S a) :-: (S b) = a :-: b++type family (:*:) (a :: N) (b :: N) :: N where+  Z :*: b = Z+  a :*: Z = Z+  (S a) :*: b = b :+: (a :*: b)
+ type-fun.cabal view
@@ -0,0 +1,50 @@+name:                type-fun+version:             0.0.1+synopsis:            Collection of widely reimplemented type families+license:             BSD3+license-file:        LICENSE+author:              Aleksey Uimanov+maintainer:          s9gf4ult@gmail.com+category:            Dependent Types+build-type:          Simple+extra-source-files:  CHANGELOG.md+cabal-version:       >=1.10+homepage:            https://github.com/s9gf4ult/type-fun+source-repository head+  type:     git+  location: git@github.com:s9gf4ult/type-fun.git++library+  default-language:    Haskell2010+  hs-source-dirs:      src+  default-extensions:  ConstraintKinds+                     , DataKinds+                     , DeriveGeneric+                     , FlexibleInstances+                     , MultiParamTypeClasses+                     , PolyKinds+                     , TypeFamilies+                     , TypeOperators+                     , UndecidableInstances++  exposed-modules:     TypeFun.Constraint+                     , TypeFun.Data.Eq+                     , TypeFun.Data.List+                     , TypeFun.Data.Maybe+                     , TypeFun.Data.Peano++  build-depends:       base >=4.7 && <4.9+++test-suite example+  type:               exitcode-stdio-1.0+  default-language:   Haskell2010+  hs-source-dirs:     example+  main-is:            Main.hs+  default-extensions: DataKinds+                    , GADTs+                    , TemplateHaskell+                    , TypeFamilies+                    , UndecidableInstances+  build-depends:  base+                , type-fun