type-set (empty) → 0.1.0.0

raw patch · 14 files changed

+681/−0 lines, 14 filesdep +basedep +randomdep +template-haskellsetup-changed

Dependencies added: base, random, template-haskell, type-set

Files

• CHANGELOG.md +11/−0
• LICENSE +30/−0
• README.md +1/−0
• Setup.hs +2/−0
• src/Data/OneOfThem.hs +139/−0
• src/Data/OneOrMore.hs +29/−0
• src/Data/OneOrMore/Internal.hs +190/−0
• src/Data/OneOrMoreApp.hs +63/−0
• src/Data/Type/Set.hs +14/−0
• src/Data/Type/Set/Internal.hs +118/−0
• src/Data/Type/SetApp.hs +3/−0
• src/Data/Type/SetApp/Internal.hs +13/−0
• test/Spec.hs +2/−0
• type-set.cabal +66/−0

@@ -0,0 +1,11 @@+# Changelog for `type-set`++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to the+[Haskell Package Versioning Policy](https://pvp.haskell.org/).++## Unreleased++## 0.1.0.0 - YYYY-MM-DD

@@ -0,0 +1,30 @@+Copyright Yoshikuni Jujo (c) 2023++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 Yoshikuni Jujo 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.

@@ -0,0 +1,1 @@+# type-set

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,139 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs, TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.OneOfThem (+	-- * OneOfThem+	-- ** Type+	OneOfThem,+	-- ** Single+	pattern Singleton, unSingleton,+	-- ** Multiple+	-- *** Project+	Projectable, project,+	-- *** Expand+	Expandable, (>-), expand,+	-- * OneOfThemFun+	-- ** Type and Apply+	OneOfThemFun, apply,+	-- ** Single+	pattern SingletonFun,+	-- ** Insert+	InsertableFun, (>--),+	-- ** Merge+	MergeableFun, mergeFun+	) where++import Data.Kind (Type)+import Data.Type.Set.Internal -- (Set(Nil, (:~)), Singleton)++data OneOfThem :: Set Type -> Type where+	JustIt :: a -> OneOfThem (a ':~ as)+	Wrap :: OneOfThem as -> OneOfThem (a ':~ as)++instance Show (OneOfThem 'Nil) where+	show _ = error "bad"++instance (Show a, Show (OneOfThem as)) => Show (OneOfThem (a :~ as)) where+	show (JustIt x) = "(JustIt " ++ show x ++ ")"+	show (Wrap xs) = show xs++{-# COMPLETE Singleton #-}++pattern Singleton :: a -> OneOfThem (Singleton a)+pattern Singleton x = JustIt x++unSingleton :: OneOfThem (Singleton a) -> a+unSingleton (Singleton x) = x++class Expandable (as :: Set Type) (as' :: Set Type) where+	expand :: OneOfThem as -> OneOfThem as'++instance Expandable 'Nil as where expand _ = error "never occur"++instance Expandable as as' => Expandable (a ':~ as) (a ':~ as') where+	expand (JustIt x) = JustIt x+	expand (Wrap oot) = Wrap $ expand oot++instance {-# OVERLAPPABLE #-} Expandable (a ':~ as) as' =>+	Expandable (a ':~ as) (a' ':~ as') where+	expand x = Wrap $ expand x++class Projectable (as :: Set Type) a where project :: OneOfThem as -> Maybe a++instance Projectable 'Nil a where project _ = Nothing+instance Projectable (a ':~ as) a where+	project (JustIt x) = Just x+	project (Wrap _) = Nothing+instance {-# OVERLAPPABLE #-} Projectable as a =>+	Projectable (a' ':~ as) a where+	project (JustIt _) = Nothing+	project (Wrap xs) = project xs++class Collapsable (as :: Set Type) (as' :: Set Type) where+	collapse :: OneOfThem as -> Maybe (OneOfThem as')++instance Collapsable as 'Nil where collapse _ = Nothing++instance Collapsable as as' => Collapsable (a ':~ as) (a ':~ as') where+	collapse (JustIt x) = Just $ JustIt x+	collapse (Wrap oot) = Wrap <$> collapse oot++instance {-# OVERLAPPABLE #-} Collapsable as (a' ':~ as') =>+	Collapsable (a ':~ as) (a' ':~ as') where+	collapse (JustIt _) = Nothing+	collapse (Wrap oot) = collapse oot++data OneOfThemFun (as :: Set Type) b where+	EmptyFun :: OneOfThemFun 'Nil b+	(:..) :: (a -> b) -> OneOfThemFun as b -> OneOfThemFun (a ':~ as) b++class InsertableFun a (as :: Set Type) (as' :: Set Type) where+	(>--.) :: (a -> b) -> OneOfThemFun as b -> OneOfThemFun as' b++instance InsertableFun a as (a ':~ as) where f >--. fs = f :.. fs++instance {-# OVERLAPPABLE #-} InsertableFun a as as' =>+	InsertableFun a (a' ':~ as) (a' ':~ as') where+	f >--. (g :.. fs) = g :.. (f >--. fs)++infixr 5 >-, >--++(>--) :: InsertableFun a as (a :- as) => (a -> b) -> OneOfThemFun as b -> OneOfThemFun (a :- as) b+(>--) = (>--.)++{-# COMPLETE SingletonFun #-}++pattern SingletonFun :: (a -> b) -> OneOfThemFun (Singleton a) b+pattern SingletonFun f = f :.. EmptyFun++class Applyable as where+	apply :: OneOfThemFun as b -> OneOfThem as -> b++instance Applyable (Singleton a) where+	apply (SingletonFun f) (Singleton x) = f x++instance {-# OVERLAPPABLE #-} Applyable as => Applyable (a ':~ as) where+	apply (f :.. _) (JustIt x) = f x+	apply (_ :.. fs) (Wrap xs) = fs `apply` xs++(>-) :: (Expandable (Singleton a) (a :- as), Expandable as (a :- as)) => a -> [OneOfThem as] -> [OneOfThem (a :- as)]+x >- xs = expand (Singleton x) : (expand <$> xs)++class MergeableFun as as' mrg where+	mergeFun_ :: OneOfThemFun as b -> OneOfThemFun as' b -> OneOfThemFun mrg b++instance MergeableFun 'Nil 'Nil 'Nil where+	mergeFun_ EmptyFun EmptyFun = EmptyFun++instance MergeableFun as as' mrg => MergeableFun as (a' ':~ as') (a' ':~ mrg) where+	mergeFun_ fs (g :.. gs) = g :.. mergeFun_ fs gs++instance MergeableFun as as' mrg => MergeableFun (a ':~ as) as' (a ':~ mrg) where+	mergeFun_ (f :.. fs) gs = f :.. mergeFun_ fs gs++mergeFun :: MergeableFun as as' (as :+: as') =>+	OneOfThemFun as b -> OneOfThemFun as' b -> OneOfThemFun (as :+: as') b+mergeFun = mergeFun_

@@ -0,0 +1,29 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses,+	FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.OneOrMore (+	-- * Type+	OneOrMore,+	-- * Property+	-- ** Basic Property+	Projectable, Insertable,+	-- ** Expandable and Collapsable+	Expandable, Collapsable,+	-- ** Mergeable+	Mergeable, Selectable(..),+	-- * Function+	-- ** Single Type+	pattern Singleton, unSingleton,+	-- ** Multiple Type+	project, (>-),+	-- ** Expand and Collapse+	expand, collapse,+	-- ** Merge+	merge, merge' ) where++import Data.OneOrMore.Internal

@@ -0,0 +1,190 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses,+	FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.OneOrMore.Internal (+	-- * Type+	OneOrMore,+	-- * Property+	-- ** Basic Property+	Projectable, Insertable,+	-- ** Expandable and Collapsable+	Expandable, Collapsable,+	-- ** Mergeable+	Mergeable, Selectable(..),+	-- * Function+	-- ** Single Type+	pattern Singleton, unSingleton,+	-- ** Multiple Type+	project, (>-), (>-.),+	-- ** Expand and Collapse+	expand, collapse,+	-- ** Merge+	merge, merge', merge_, merge_' ) where++import Data.Kind (Type)+import Data.Type.Set.Internal (Set(Nil, (:~)), Singleton, (:-), (:+:))++---------------------------------------------------------------------------++-- * ONE OR MORE TYPE+-- * BASIC PROPERTY+--	+ PROJECTABLE+--	+ INSERTABLE+-- * EXPANDABLE AND COLLAPSABLE+--	+ EXPANDABLE+--	+ COLLAPSABLE+--		- COLLAPSABLE 0+--		- COLLAPSABLE+-- * MERGEABLE++---------------------------------------------------------------------------+-- ONE OR MORE TYPE+---------------------------------------------------------------------------++data OneOrMore :: Set Type -> Type where+	Empty :: OneOrMore 'Nil+	(:.) :: Maybe a -> OneOrMore as -> OneOrMore (a ':~ as)++---------------------------------------------------------------------------+-- BASIC PROPERTY+---------------------------------------------------------------------------++-- PROJECTABLE++class Projectable (as :: Set Type) a where project :: OneOrMore as -> Maybe a+instance Projectable 'Nil a where project _ = Nothing+instance Projectable (a ':~ as) a where project (x :. _) = x+instance {-# OVERLAPPABLE #-} Projectable as a =>+	Projectable (a' ':~ as) a where project (_ :. xs) = project xs++{-# COMPLETE Singleton #-}++pattern Singleton :: a -> OneOrMore (Singleton a)+pattern Singleton x = Just x :. Empty++unSingleton :: OneOrMore (Singleton a) -> a+unSingleton (Singleton x) = x++-- INSERTABLE++infixr 5 >-++class Insertable a (as :: Set Type) (as' :: Set Type) where+	(>-.) :: a -> OneOrMore as -> OneOrMore as'++instance Insertable a as (a ':~ as) where x >-. xs = Just x :. xs++instance {-# OVERLAPPABLE #-} Insertable a as as' =>+	Insertable a (a' ':~ as) (a' ':~ as') where+	x >-. (y :. xs) = y :. (x >-. xs)++(>-) :: Insertable a as (a :- as) => a -> OneOrMore as -> OneOrMore (a :- as)+(>-) = (>-.)++---------------------------------------------------------------------------+-- EXPANDABLE AND COLLAPSABLE+---------------------------------------------------------------------------++-- EXPANDABLE++class Expandable (as :: Set Type) (as' :: Set Type) where+	expand :: OneOrMore as -> OneOrMore as'++instance Nihil as => Expandable (a ':~ 'Nil) (a ':~ as) where+	expand (x :. Empty) = x :. nihil++instance {-# OVERLAPPABLE #-} Expandable as as' =>+	Expandable (a ':~ as) (a ':~ as') where+	expand (x :. xs) = x :. expand xs++instance {-# OVERLAPPABLE #-} Expandable (a ':~ as) as' =>+	Expandable (a ':~ as) (a' ':~ as') where+	expand xs = Nothing :. expand xs++class Nihil as where nihil :: OneOrMore as+instance Nihil 'Nil where nihil = Empty+instance Nihil as => Nihil (a ':~ as) where nihil = Nothing :. nihil++-- COLLAPSABLE++-- COLLAPSABLE 0++class Collapsable0 (as :: Set Type) (as' :: Set Type) where+	collapse0 :: OneOrMore as -> OneOrMore as'++instance Collapsable0 as 'Nil where collapse0 = const Empty++instance {-# OVERLAPPABLE #-} Collapsable0 as as' =>+	Collapsable0 (a ':~ as) (a ':~ as') where+	collapse0 (x :. xs) = x :. collapse0 xs++instance {-# OVERLAPPABLE #-} Collapsable0 as (a' ':~ as') =>+	Collapsable0 (a ':~ as) (a' ':~ as') where+	collapse0 (_ :. xs) = collapse0 xs++-- COLLAPSABLE++class Collapsable (as :: Set Type) (as' :: Set Type) where+	collapse :: OneOrMore as -> Maybe (OneOrMore as')++instance Collapsable 'Nil 'Nil where collapse = const Nothing++instance (Collapsable0 as as', Collapsable as as') =>+	Collapsable (a ':~ as) (a ':~ as') where+	collapse = \case+		Just x :. xs -> Just $ Just x :. collapse0 xs+		Nothing :. xs -> (Nothing :.) <$> collapse xs++instance {-# OVERLAPPABLE #-} Collapsable as as' =>+	Collapsable (a ':~ as) as' where+	collapse (_ :. xs) = collapse xs++---------------------------------------------------------------------------+-- MERGEABLE+---------------------------------------------------------------------------++class Mergeable (as :: Set Type) (as' :: Set Type) (mrg :: Set Type) where+	merge_ :: OneOrMore as -> OneOrMore as' -> OneOrMore mrg++instance Mergeable 'Nil 'Nil 'Nil where merge_ Empty Empty = Empty++instance (Selectable a, Mergeable as as' mrg) =>+	Mergeable (a ':~ as) (a ':~ as') (a ':~ mrg) where+	merge_ (Just x :. xs) (Just x' :. xs') =+		Just (x `select` x') :. merge_ xs xs'+	merge_ (mx :. xs) (Nothing :. xs') = mx :. merge_ xs xs'+	merge_ (Nothing :. xs) (mx' :. xs') = mx' :. merge_ xs xs'++instance {-# OVERLAPPABLE #-} Mergeable as as' mrg =>+	Mergeable (a ':~ as) as'  (a ':~ mrg) where+	merge_ (x :. xs) xs' = x :. merge_ xs xs'++instance {-# OVERLAPPABLE #-} Mergeable as as' mrg =>+	Mergeable as (a ':~ as') (a ':~ mrg) where+	merge_ xs (x :. xs') = x :. merge_ xs xs'++class Selectable a where select :: a -> a -> a+instance {-# OVERLAPPABLE #-} Ord a => Selectable a where select = min++merge_' :: (Mergeable as as' mrg, Expandable as mrg, Expandable as' mrg ) =>+	Maybe (OneOrMore as) -> Maybe (OneOrMore as') -> Maybe (OneOrMore mrg)+ml `merge_'` mr = case (ml, mr) of+	(Just l, Just r) -> Just $ l `merge_` r+	(Just l, Nothing) -> Just $ expand l+	(Nothing, Just r) -> Just $ expand r+	(Nothing, Nothing) -> Nothing++merge :: Mergeable as as' (as :+: as') =>+	OneOrMore as -> OneOrMore as' -> OneOrMore (as :+: as')+merge = merge_++merge' :: (+	Mergeable as as' (as :+: as'),+	Expandable as (as :+: as'), Expandable as' (as :+: as') ) =>+	Maybe (OneOrMore as) -> Maybe (OneOrMore as') -> Maybe (OneOrMore (as :+: as'))+merge' = merge_'

@@ -0,0 +1,63 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ConstraintKinds, FlexibleContexts #-}+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.OneOrMoreApp (+	-- * Type+	OneOrMoreApp,+	-- * Constraint Synonym+	Expandable, Collapsable, Mergeable,+	-- * Function+	-- ** Single Type+	pattern Singleton, unSingleton,+	-- ** Multiple Type+	project, (>-),+	-- ** Expand and Collapse+	expand, collapse,+	-- ** Merge+	merge, merge' ) where++import Data.Kind+import Data.Type.Set.Internal+import Data.Type.SetApp.Internal+import qualified Data.OneOrMore.Internal as Oom++data OneOrMoreApp :: SetApp Type -> Type where+	OneOrMoreApp ::  Oom.OneOrMore as ->  OneOrMoreApp ('SetApp f as)++{-# COMPLETE Singleton #-}++pattern Singleton :: a -> OneOrMoreApp ('SetApp f (Singleton a))+pattern Singleton x = OneOrMoreApp (Oom.Singleton x)++unSingleton :: OneOrMoreApp ('SetApp f (Singleton a)) -> a+unSingleton (Singleton x) = x++expand :: Oom.Expandable as as' => OneOrMoreApp ('SetApp f as) -> OneOrMoreApp ('SetApp f as')+expand (OneOrMoreApp xs) = OneOrMoreApp $ Oom.expand xs++collapse :: Oom.Collapsable as as' => OneOrMoreApp ('SetApp f as) -> Maybe (OneOrMoreApp ('SetApp f as'))+collapse (OneOrMoreApp xs) = OneOrMoreApp <$> Oom.collapse xs++project :: Oom.Projectable as a => OneOrMoreApp ('SetApp f as) -> Maybe a+project (OneOrMoreApp xs) = Oom.project xs++(>-) :: Oom.Insertable a as as' => a -> OneOrMoreApp ('SetApp f as) -> OneOrMoreApp ('SetApp f as')+x >- (OneOrMoreApp xs) = OneOrMoreApp $ x Oom.>-. xs++merge :: Oom.Mergeable as as' mrg => OneOrMoreApp ('SetApp f as) -> OneOrMoreApp ('SetApp f as') -> OneOrMoreApp ('SetApp f mrg)+OneOrMoreApp xs `merge` OneOrMoreApp xs' = OneOrMoreApp $ xs `Oom.merge_` xs'++unOneOrMoreApp :: OneOrMoreApp ('SetApp f as) -> Oom.OneOrMore as+unOneOrMoreApp (OneOrMoreApp xs) = xs++merge' :: (Oom.Mergeable as as' mrg, Oom.Expandable as mrg, Oom.Expandable as' mrg) =>+	Maybe (OneOrMoreApp ('SetApp f as)) -> Maybe (OneOrMoreApp ('SetApp f as')) -> Maybe (OneOrMoreApp ('SetApp f mrg))+xs `merge'` xs' = OneOrMoreApp <$> (unOneOrMoreApp <$> xs) `Oom.merge_'` (unOneOrMoreApp <$> xs')++type Expandable f as as' = Oom.Expandable (f `Map` as) (f `Map` as')+type Collapsable f as as' = Oom.Collapsable (f `Map` as) (f `Map` as')+type Mergeable f as as' mrg = Oom.Mergeable (f `Map` as) (f `Map` as') (f `Map` mrg)

@@ -0,0 +1,14 @@+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Type.Set (+	-- * Set+	Set(Nil),+	-- * Numbered+	Numbered, numbered,+	-- * Function+	Singleton, Insert, Merge,+	-- * Operator+	(:-), (:+:) ) where++import Data.Type.Set.Internal (+	Set(Nil), Numbered, numbered, Singleton, Insert, Merge, (:-), (:+:) )

@@ -0,0 +1,118 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE PolyKinds, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Type.Set.Internal (+	-- * Set+	Set(Nil, (:~)),+	-- * Numbered+	Numbered, numbered,+	-- * Function+	Singleton, Insert, Merge, Map,+	-- * Operator+	(:-), (:+:) ) where++import GHC.TypeLits (Nat, type (<=?))+import Language.Haskell.TH (+	TypeQ, DecsQ, runIO,+	instanceD, cxt, tySynInstD, tySynEqn, conT, appT, litT, numTyLit )+import Data.Kind (Type)+import System.Random (randomRIO)++---------------------------------------------------------------------------++-- * TYPE SET+--	+ DATA DEFINITION+--	+ COMBINATOR+--		- Singleton+--		- Insert+--		- Merge+--		- Map+-- * NUMBERED+-- * BOOL++---------------------------------------------------------------------------+-- TYPE SET+---------------------------------------------------------------------------++-- DATA DEFINITION++infixr 5 :~+data Set a = Nil | a :~ Set a++-- COMBINATOR++-- Singleton++type Singleton t = t ':~ 'Nil++-- Insert++infixr 5 :-+type t :- ts = t `Insert` ts++type family Insert (t :: Type) (ts :: Set Type) :: Set Type where+	Insert t 'Nil = t ':~ 'Nil+	Insert t (t ':~ ts) = t ':~ ts+	Insert t (t' ':~ ts) = BOOL+		(InsertElse t t' ts)+		(InsertThen t t' ts)+			$ (Number t <=? Number t')++data InsertElse t t' ts :: () >-> k+type instance InsertElse  t t' ts $ '() = t' ':~ t :- ts++data InsertThen t t' ts :: () >-> k+type instance InsertThen t t' ts $ '() = t ':~ t' ':~ ts++-- Merge++infixr 5 :+:+type ts :+: ts' = ts `Merge` ts'++type family Merge (ts :: Set Type) (ts' :: Set Type) :: Set Type where+	Merge ts 'Nil = ts+	Merge 'Nil ts' = ts'+	Merge (t ':~ ts) (t ':~ ts') = t ':~ Merge ts ts'+	Merge (t ':~ ts) (t' ':~ ts') = BOOL+		(MergeElse t ts t' ts')+		(MergeThen t ts t' ts')+			$ (Number t <=? Number t')++data MergeElse t ts t' ts' :: () >-> k+type instance MergeElse t ts t' ts' $ '() = t' ':~ (t ':~ ts) :+: ts'++data MergeThen t ts t' ts' :: () >-> k+type instance MergeThen t ts t' ts' $ '() = t ':~ ts :+: (t' ':~ ts')++-- Map++type family Map (f :: Type -> Type) (ts :: Set Type) :: Set Type where+	_ `Map` 'Nil = 'Nil+	f `Map` (t ':~ ts) = f t ':~ (f `Map` ts)++---------------------------------------------------------------------------+-- NUMBERED+---------------------------------------------------------------------------++class Numbered a where type Number (a :: Type) = (r :: Nat) | r -> a++numbered :: TypeQ -> DecsQ+numbered t = ((: []) <$>)+	. instanceD (cxt []) (conT ''Numbered `appT` t) . (: [])+		$ tySynInstD . tySynEqn Nothing (conT ''Number `appT` t)+			. litT . numTyLit =<< runIO (randomRIO (0, 2 ^ s - 1))+	where s = 64 :: Int++---------------------------------------------------------------------------+-- BOOL+---------------------------------------------------------------------------++type a >-> b = (b -> Type) -> a -> Type+type family ($) (f :: a >-> b) (x :: a) :: b++data BOOL :: (() >-> k) -> (() >-> k) -> (Bool >-> k)+type instance (BOOL f _) $ 'False = f $ '()+type instance (BOOL _ t) $ 'True = t $ '()

@@ -0,0 +1,3 @@+module Data.Type.SetApp (SetApp, (:$:)) where++import Data.Type.SetApp.Internal

@@ -0,0 +1,13 @@+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.Type.SetApp.Internal where++import Data.Kind+import Data.Type.Set.Internal++data SetApp a = SetApp (Type -> Type) (Set a)++infixl 4 :$:++type f :$: ts = 'SetApp f (f `Map` ts)

@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"

@@ -0,0 +1,66 @@+cabal-version: 2.2++-- This file has been generated from package.yaml by hpack version 0.35.2.+--+-- see: https://github.com/sol/hpack++name:           type-set+version:        0.1.0.0+synopsis:       Type set+description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/type-set#readme>+category:       Data+homepage:       https://github.com/YoshikuniJujo/type-set#readme+bug-reports:    https://github.com/YoshikuniJujo/type-set/issues+author:         Yoshikuni Jujo+maintainer:     yoshikuni.jujo@gmail.com+copyright:      Copyright (c) 2023 Yoshikuni Jujo+license:        BSD-3-Clause+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/YoshikuniJujo/type-set++library+  exposed-modules:+      Data.Type.Set+      Data.Type.SetApp+      Data.OneOfThem+      Data.OneOrMore+      Data.OneOrMoreApp+  other-modules:+      Data.OneOrMore.Internal+      Data.Type.Set.Internal+      Data.Type.SetApp.Internal+      Paths_type_set+  autogen-modules:+      Paths_type_set+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base >=4.7 && <5+    , random+    , template-haskell+  default-language: Haskell2010++test-suite type-set-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Paths_type_set+  autogen-modules:+      Paths_type_set+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , random+    , template-haskell+    , type-set+  default-language: Haskell2010