packages feed

type-sets (empty) → 0.1.0.0

raw patch · 8 files changed

+439/−0 lines, 8 filesdep +basedep +cmptypedep +type-setssetup-changed

Dependencies added: base, cmptype, type-sets

Files

+ ChangeLog.md view
@@ -0,0 +1,7 @@+# Changelog for type-sets++## 0.1.0.0 --- 2019-08-07++Initial release!++## Unreleased changes
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2019++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 Sandy Maguire 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.
+ README.md view
@@ -0,0 +1,53 @@+# type-sets++[![Build Status](https://api.travis-ci.org/isovector/type-sets.svg?branch=master)](https://travis-ci.org/isovector/type-sets)+[![Hackage](https://img.shields.io/hackage/v/cmptype.svg?logo=haskell&label=cmptype)](https://hackage.haskell.org/package/cmptype)+++## Dedication++> Obstacles don't have to stop you. If you run into a wall, don't turn around+> and give up. Figure out how to climb it, go through it, or work around it.++> -- Michael Jordan, on complexity analysis in Haskell+++## Overview++How much do you hate programming at the type level, but only being able to use+lists? A million? *Two* million? Some mathematicians suspect that there may be+even larger degrees of hate.++Enter `type-sets`. They're sets... at the type-level! Check this:++```haskell+{-# OPTIONS_GHC -fplugin=Type.Compare.Plugin #-}++import Type.Set++type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))++test1 :: Proxy (Member Bool MySet) -> Proxy 'True+test1 = id  -- Bool is a member :)++test2 :: Proxy (Member Char MySet) -> Proxy 'False+test2 = id  -- False is not a member :(+```++See the `Type.Set` module for more operations.++But wait, there's more! There's also a proof-of-concept `Type.Set.Variant` for+describing open-sums indexed by type-sets. PRs to make it better would be+greatly appreciated!++One love.+++## Acknowledgments++Huge shout-outs to [Boris Rozinov][oofp] for all of his help on this library,+including the original idea, help with the implementation, infinite amounts of+coffee, and a couch to sleep on while it was being made.++[oofp]: https://github.com/oofp+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Type/Set.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Set+  ( -- * Core type+    TypeSet (..)++    -- * Set operations+  , Member+  , Insert+  , Remove+  , Merge++    -- * Tree operations+  , Locate+  , Follow+  , Side (..)+  ) where++import Type.Compare+import GHC.TypeLits+++------------------------------------------------------------------------------+-- | A binary search tree. When @-XDataKinds@ is turned on, this becomes the+-- backbone of the type-level set.+--+-- >>> type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))+data TypeSet a+  = Empty+  | Branch a (TypeSet a) (TypeSet a)+++------------------------------------------------------------------------------+-- | Either left or right down a path.+data Side = L | R+  deriving (Eq, Ord, Show)++------------------------------------------------------------------------------+-- | /O(log n)/. Insert an element into the 'TypeSet'.+type family Insert (t :: k) (bst :: TypeSet k)  :: TypeSet k where+  Insert t 'Empty = 'Branch t 'Empty 'Empty+  Insert t ('Branch a lbst rbst) =+    InsertImpl (CmpType t a) t a lbst rbst++type family InsertImpl (ord :: Ordering)+                       (t :: k)+                       (a :: k)+                       (lbst :: TypeSet k)+                       (rbst :: TypeSet k) :: TypeSet k where+  InsertImpl 'EQ t a lbst rbst = 'Branch a lbst rbst+  InsertImpl 'LT t a lbst rbst = 'Branch a (Insert t lbst) rbst+  InsertImpl 'GT t a lbst rbst = 'Branch a lbst (Insert t rbst)+++------------------------------------------------------------------------------+-- | /O(log n)/. Determine membership in the 'TypeSet.'+type family Member (t :: k) (bst :: TypeSet k)  :: Bool where+  Member t 'Empty = 'False+  Member t ('Branch a lbst rbst) = MemberImpl (CmpType t a) t lbst rbst++type family MemberImpl (ord :: Ordering)+                       (t :: k)+                       (lbst :: TypeSet k)+                       (rbst :: TypeSet k) :: Bool where+  MemberImpl 'EQ t lbst rbst = 'True+  MemberImpl 'LT t lbst rbst = Member t lbst+  MemberImpl 'GT t lbst rbst = Member t rbst+++------------------------------------------------------------------------------+-- | /O(m log n)/ for @Merge m n@; put your smaller set on the left side. Merge+-- two 'TypeSet's together.+type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k where+  Merge Empty big   = big+  Merge small Empty = small+  Merge ('Branch a lbst rbst) big = Merge rbst (Merge lbst (Insert a big))+++------------------------------------------------------------------------------+-- | /O(log n)/. Remove an element from the 'TypeSet'.+type family Remove (t :: k) (bst :: TypeSet k) :: TypeSet k where+  Remove t Empty = Empty+  Remove t ('Branch a lbst rbst) = RemoveImpl (CmpType t a) t a lbst rbst++type family RemoveImpl (ord :: Ordering)+                       (t :: k)+                       (a :: k)+                       (lbst :: TypeSet k)+                       (rbst :: TypeSet k) :: TypeSet k where+  RemoveImpl 'LT t a lbst rbst = 'Branch a (Remove t lbst) rbst+  RemoveImpl 'EQ t a Empty rbst = rbst+  RemoveImpl 'EQ t a lbst Empty = lbst+  RemoveImpl 'EQ t a lbst rbst =+    'Branch (RightMost lbst) (Remove (RightMost lbst) lbst) rbst+  RemoveImpl 'GT t a lbst rbst = 'Branch a lbst (Remove t rbst)+++------------------------------------------------------------------------------+-- | /O(log n)/. Get the right-most element in a tree. This function is stuck+-- if the tree is empty.+type family RightMost (bst :: TypeSet k) :: k where+  RightMost ('Branch a lbst 'Empty) = a+  RightMost ('Branch a lbst rbst) = RightMost rbst+++------------------------------------------------------------------------------+-- | /O(log n)/. Compute a @['Side']@ which finds the desired element in the+-- tree. The result of this can be passed to 'Follow' in order to look up the+-- same element again later.+type family Locate (t :: k) (bst :: TypeSet k) :: [Side] where+  Member t ('Branch a lbst rbst) = LocateImpl (CmpType t a) t lbst rbst+  Member t 'Empty = TypeError ('Text "Unable to locate: " ':<>: 'ShowType t)++type family LocateImpl (ord :: Ordering)+                       (t :: k)+                       (lbst :: TypeSet k)+                       (rbst :: TypeSet k) :: [Side] where+  LocateImpl 'EQ t lbst rbst = '[]+  LocateImpl 'LT t lbst rbst = 'L ': Locate t lbst+  LocateImpl 'GT t lbst rbst = 'R ': Locate t rbst+++------------------------------------------------------------------------------+-- | /O(log n)/. Follow the result of a 'Locate' to get a particular element in+-- the tree.+type family Follow (ss :: [Side]) (bst :: TypeSet k) :: k where+  Follow '[] ('Branch t _ _) = t+  Follow ('L ': ss) ('Branch _ l _) = Follow ss l+  Follow ('R ': ss) ('Branch _ _ r) = Follow ss r+  Follow ss 'Empty = TypeError ('Text "Unable to follow: " ':<>: 'ShowType ss)+
+ src/Type/Set/Variant.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE AllowAmbiguousTypes   #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RoleAnnotations       #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# OPTIONS_GHC -Wall              #-}++module Type.Set.Variant+  ( -- * Core types+    Variant (..)+  , Has (..)++    -- * Decomposition proofs+  , decompRoot+  , Split (..)++    -- * Weakening+  , weaken++    -- * Internal stuff+  , proveFollowInsert+  , SSide (..)+  , FromSides (..)+  ) where++import Data.Type.Equality+import Type.Set+import Unsafe.Coerce++------------------------------------------------------------------------------+-- | Singletons for 'Side's.+data SSide (ss :: [Side]) where+  SNil :: SSide '[]+  SL :: SSide ss -> SSide ('L ': ss)+  SR :: SSide ss -> SSide ('R ': ss)++------------------------------------------------------------------------------+-- | Get a singleton for a list of 'Side's.+class FromSides (ss :: [Side]) where+  fromSides :: SSide ss++instance FromSides '[] where+  fromSides = SNil++instance FromSides ss => FromSides ('L ': ss) where+  fromSides = SL fromSides++instance FromSides ss => FromSides ('R ': ss) where+  fromSides = SR fromSides+++------------------------------------------------------------------------------+-- | A 'Variant' is like an 'Either', except that it can store any of the types+-- contained in the 'TypeSet'. You can use 'toVariant' to construct one, and+-- 'fromVariant' to pattern match it out.+data Variant (v :: TypeSet *) where+  Variant :: SSide ss -> Follow ss v -> Variant v+type role Variant nominal+++------------------------------------------------------------------------------+-- | A proof that the set @bst@ contains type @t@.+class Has t bst where+  -- | Inject a @t@ into a 'Variant'.+  toVariant :: t -> Variant bst+  -- | Attempt to project a 'Variant' into @t@. This might fail, because there+  -- is no guarantee that the 'Variant' /actually contains/ @t@.+  --+  -- You can use 'decompRoot' instead of this function if you'd like a proof+  -- that the 'Variant' doesn't contain @t@ in the case of failure.+  fromVariant :: Variant bst -> Maybe t++instance ( Follow (Locate t bst) bst ~ t+         , FromSides (Locate t bst)+         ) => Has t bst where+  toVariant = Variant (fromSides @(Locate t bst))+  fromVariant (Variant tag res) =+    case testEquality tag (fromSides @(Locate t bst)) of+      Just Refl -> Just res+      Nothing -> Nothing+++instance TestEquality SSide where+  testEquality SNil   SNil   = Just Refl+  testEquality (SL a) (SL b) =+    case testEquality a b of+      Just Refl -> Just Refl+      Nothing -> Nothing+  testEquality (SR a) (SR b) =+    case testEquality a b of+      Just Refl -> Just Refl+      Nothing -> Nothing+  testEquality (SL _) SNil   = Nothing+  testEquality SNil   (SL _) = Nothing+  testEquality (SR _) SNil   = Nothing+  testEquality SNil   (SR _) = Nothing+  testEquality (SR _) (SL _) = Nothing+  testEquality (SL _) (SR _) = Nothing+++------------------------------------------------------------------------------+-- | A proof that inserting into a @bst@ doesn't affect the position of+-- anything already in the tree.+proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst+proveFollowInsert = unsafeCoerce Refl+++------------------------------------------------------------------------------+-- | Weaken a 'Variant' so that it can contain something else.+weaken :: forall t bst. Variant bst -> Variant (Insert t bst)+weaken (Variant (tag :: SSide ss) res) = Variant tag $+  case proveFollowInsert @ss @t @bst of+    Refl -> res+++data Split t lbst rbst+  = Root t+  | LSplit (Variant lbst)+  | RSplit (Variant rbst)+++------------------------------------------------------------------------------+-- | Like 'fromVariant', but decomposes the 'Variant' into its left and right+-- branches, depending on where @t@ is.+decompRoot :: Variant ('Branch t lbst rbst) -> Split t lbst rbst+decompRoot (Variant SNil t) = Root t+decompRoot (Variant (SL s) t) = LSplit (Variant s t)+decompRoot (Variant (SR s) t) = RSplit (Variant s t)+
+ test/Spec.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE DataKinds #-}++{-# OPTIONS_GHC -fplugin=Type.Compare.Plugin      #-}+{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}++import Data.Proxy+import Type.Set++type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))++test1 :: Proxy (Member Bool MySet) -> Proxy 'True+test1 = id  -- Bool is a member :)++test2 :: Proxy (Member Char MySet) -> Proxy 'False+test2 = id  -- False is not a member :(++main :: IO ()+main = putStrLn "It compiled!"+
+ type-sets.cabal view
@@ -0,0 +1,55 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 60b368d526cc5cac3b6dd1535ea9d63df46fe48ac16f522464490b53a71a034b++name:           type-sets+version:        0.1.0.0+synopsis:       Type-level sets+description:    Please see the README on GitHub at <https://github.com/isovector/type-sets#readme>+category:       Type+homepage:       https://github.com/isovector/type-sets#readme+bug-reports:    https://github.com/isovector/type-sets/issues+author:         Sandy Maguire+maintainer:     sandy@sandymaguire.me+copyright:      2019 Sandy Maguire+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/isovector/type-sets++library+  exposed-modules:+      Type.Set+      Type.Set.Variant+  other-modules:+      Paths_type_sets+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , cmptype >=0.1.0.0 && <0.2+  default-language: Haskell2010++test-suite type-sets-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Paths_type_sets+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , cmptype >=0.1.0.0 && <0.2+    , type-sets+  default-language: Haskell2010