diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,1 @@ +# type-set diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Data/OneOfThem.hs b/src/Data/OneOfThem.hs new file mode 100644 --- /dev/null +++ b/src/Data/OneOfThem.hs @@ -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_ diff --git a/src/Data/OneOrMore.hs b/src/Data/OneOrMore.hs new file mode 100644 --- /dev/null +++ b/src/Data/OneOrMore.hs @@ -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 diff --git a/src/Data/OneOrMore/Internal.hs b/src/Data/OneOrMore/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/OneOrMore/Internal.hs @@ -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_' diff --git a/src/Data/OneOrMoreApp.hs b/src/Data/OneOrMoreApp.hs new file mode 100644 --- /dev/null +++ b/src/Data/OneOrMoreApp.hs @@ -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) diff --git a/src/Data/Type/Set.hs b/src/Data/Type/Set.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Set.hs @@ -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, (:-), (:+:) ) diff --git a/src/Data/Type/Set/Internal.hs b/src/Data/Type/Set/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Set/Internal.hs @@ -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 $ '() diff --git a/src/Data/Type/SetApp.hs b/src/Data/Type/SetApp.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/SetApp.hs @@ -0,0 +1,3 @@ +module Data.Type.SetApp (SetApp, (:$:)) where + +import Data.Type.SetApp.Internal diff --git a/src/Data/Type/SetApp/Internal.hs b/src/Data/Type/SetApp/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/SetApp/Internal.hs @@ -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) diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,2 @@ +main :: IO () +main = putStrLn "Test suite not yet implemented" diff --git a/type-set.cabal b/type-set.cabal new file mode 100644 --- /dev/null +++ b/type-set.cabal @@ -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 +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