Initial commit

.github/workflows/ci.yaml

@@ -0,0 +1,72 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - "*"
+  pull_request:
+    branches:
+      - "*"
+  release:
+    types:
+      - prereleased
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        platform:
+          - ubuntu-latest
+        ghc_version:
+          #- "8.6.5"
+          #- "8.8.4"
+          #- "8.10.7"
+          #- "9.0.2"
+          #- "9.2.8"
+          #- "9.4.8"
+          - "9.6.3"
+          #- "9.8.1"
+      fail-fast: false
+    name: Build on Linux, GHC ${{ matrix.ghc_version }}
+    runs-on: ${{ matrix.platform }}
+    steps:
+      - uses: actions/checkout@v3
+      - uses: haskell/actions/setup@v2
+        with:
+          ghc-version: ${{ matrix.ghc_version }}
+          cabal-version: "3.10.1.0"
+      - name: cabal configure
+        run: cabal configure --with-ghc=ghc-${{ matrix.ghc_version }}
+      - name: Install dependencies
+        run: cabal build --dependencies-only --enable-tests --haddock-all
+      - name: cabal build
+        run: cabal build --ghc-options=-Werror
+      - run: cabal check
+      - run: cabal haddock
+
+  dist:
+    needs: build
+    runs-on: ubuntu-latest
+    name: Build source tarball
+    if: github.event_name == 'release'
+    steps:
+      - uses: actions/checkout@v3
+      - uses: haskell/actions/setup@v2
+        with:
+          cabal-version: "3.10.1.0"
+      - name: cabal sdist
+        run: |
+          cabal sdist --output-dir "$GITHUB_WORKSPACE/sdist"
+          echo "dist=$(find "$GITHUB_WORKSPACE/sdist" -maxdepth 1 -type f -name '*.tar.gz')" >> "$GITHUB_ENV"
+      - uses: actions/upload-artifact@v2
+        with:
+          name: Source tarball
+          path: ${{ env.dist }}
+      - uses: svenstaro/[email protected]
+        with:
+          repo_token: ${{ secrets.GITHUB_TOKEN }}
+          file: ${{ env.dist }}
+          tag: ${{ github.ref }}
+      - name: Upload tarball to hackage
+        run: |
+          curl -X POST 'https://hackage.haskell.org/packages/candidates/' -H "Authorization: X-ApiKey ${{ secrets.HACKAGE_KEY }}" -F "package=@$dist" -w '%{url_effective}\n'

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2023 Typeable
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

refined-containers.cabal

@@ -0,0 +1,99 @@
+cabal-version: 3.0
+name: refined-containers
+category: Data
+synopsis:
+    Type-checked proof that a key exists in a container and can be safely
+    indexed.
+description:
+    This package defines ways to prove that a key exists in an associative
+    container such as a 'Map', 'IntMap', or 'HashMap'; so that the key can be
+    used to index into the map without a 'Maybe' or manually handling the
+    \"impossible\" case with 'error' or other partial functions.
+
+    To do this, the containers are tagged with a type parameter that identifies
+    their set of keys, so that if you have another container with the same
+    parameter, you know it has the same keys.
+
+    There is also a type of keys that have been proven to exist in such
+    containers -- a refinement type. They are also tagged with a type parameter.
+    If the type parameter of the key matches that of the container, indexing is
+    guaranteed to proceed without failure.
+
+license: MIT
+license-file: LICENSE
+author: [email protected]
+maintainer: [email protected]
+version: 0.1.0.0
+build-type: Simple
+
+tested-with:
+    , GHC == 9.8.1
+    , GHC == 9.6.3
+    , GHC == 9.4.8
+    , GHC == 9.2.8
+    , GHC == 9.0.2
+    , GHC == 8.10.7
+    , GHC == 8.6.5
+
+source-repository head
+    type: git
+    location: https://github.com/typeable/refined-containers/
+
+library
+    build-depends:
+        , base >= 4.12 && < 4.19
+        , adjunctions >= 4.4 && < 4.5
+        , constraints >= 0.11 && < 0.15
+        , containers >= 0.5.7 && < 0.8
+        , deepseq >= 1.4 && < 1.6
+        , distributive >= 0.5.3 && < 0.7
+        , hashable >= 1.2.7 && < 1.5
+        , indexed-traversable >= 0.1 && < 0.2
+        , mtl >= 2.2.2 && < 2.4
+        , refined >= 0.5 && < 0.9
+        , reflection >= 2 && < 2.2
+        , unordered-containers >= 0.2.11 && < 0.3
+    exposed-modules:
+        Data.HashMap.Refined
+        Data.HashMap.Strict.Refined
+        Data.HashSet.Refined
+        Data.IntMap.Refined
+        Data.IntMap.Strict.Refined
+        Data.IntSet.Refined
+        Data.Map.Refined
+        Data.Map.Strict.Refined
+        Data.Set.Refined
+    other-modules:
+        Data.Container.Refined.Conversion
+        Data.Container.Refined.Hashable
+        Data.Container.Refined.Proofs
+        Data.Container.Refined.Unsafe
+        Data.HashMap.Common.Refined
+        Data.IntMap.Common.Refined
+        Data.Map.Common.Refined
+    hs-source-dirs: src
+    default-language: Haskell2010
+    default-extensions:
+        BangPatterns
+        BlockArguments
+        ConstraintKinds
+        DataKinds
+        DeriveTraversable
+        DerivingStrategies
+        FlexibleContexts
+        FlexibleInstances
+        GADTs
+        GeneralizedNewtypeDeriving
+        MagicHash
+        MultiParamTypeClasses
+        MultiWayIf
+        OverloadedStrings
+        RankNTypes
+        PatternSynonyms
+        RoleAnnotations
+        ScopedTypeVariables
+        TupleSections
+        TypeApplications
+        TypeFamilies
+        TypeOperators
+    ghc-options: -Wall -Wredundant-constraints

src/Data/Container/Refined/Conversion.hs

@@ -0,0 +1,79 @@
+module Data.Container.Refined.Conversion where
+
+import           Data.Constraint (Dict(..))
+import           Data.Container.Refined.Hashable
+import           Data.Container.Refined.Proofs
+import qualified Data.HashMap.Lazy as HashMap
+import           Data.HashMap.Common.Refined
+import qualified Data.HashSet as HashSet
+import qualified Data.IntMap as IntMap
+import           Data.IntMap.Common.Refined
+import qualified Data.IntSet as IntSet
+import qualified Data.Map as Map
+import           Data.Map.Common.Refined
+import           Data.Proxy
+import           Data.Reflection
+import qualified Data.Set as Set
+import           Data.Type.Equality ((:~:)(..))
+import           Unsafe.Coerce
+
+
+unsafeWrapSet :: forall r r' a. KnownSet r' a => Proxy r' -> Set r a
+unsafeWrapSet _ = case unsafeCoerce Refl :: r :~: r' of Refl -> Dict
+{-# INLINE unsafeWrapSet #-}
+
+unsafeWrapIntSet :: forall r r'. KnownIntSet r' => Proxy r' -> IntSet r
+unsafeWrapIntSet _ = case unsafeCoerce Refl :: r :~: r' of Refl -> Dict
+{-# INLINE unsafeWrapIntSet #-}
+
+unsafeWrapHashSet :: forall r r' a. KnownHashSet r' a => Proxy r' -> HashSet r a
+unsafeWrapHashSet _ = case unsafeCoerce Refl :: r :~: r' of Refl -> Dict
+{-# INLINE unsafeWrapHashSet #-}
+
+set2IntSet :: forall s. KnownSet s Int => IntSet s
+set2IntSet = reify
+  (IntSet.fromDistinctAscList $ Set.toAscList $ reflect $ Proxy @s)
+  unsafeWrapIntSet
+
+map2IntMap :: forall s a. Map s Int a -> IntMap s a
+map2IntMap (Map m) = IntMap $ IntMap.fromDistinctAscList $ Map.toAscList m
+
+set2HashSet :: forall s a. (Hashable a, KnownSet s a) => HashSet s a
+set2HashSet = reify
+  (HashSet.fromList $ Set.toList $ reflect $ Proxy @s)
+  unsafeWrapHashSet
+
+map2HashMap :: forall s k a. Hashable k => Map s k a -> HashMap s k a
+map2HashMap (Map m) = HashMap $ HashMap.fromList $ Map.toList m
+
+intSet2Set :: forall s. KnownIntSet s => Set s Int
+intSet2Set = reify
+  (Set.fromDistinctAscList $ IntSet.toAscList $ reflect $ Proxy @s)
+  unsafeWrapSet
+
+intMap2Map :: forall s a. IntMap s a -> Map s Int a
+intMap2Map (IntMap m) = Map $ Map.fromDistinctAscList $ IntMap.toAscList m
+
+intSet2HashSet :: forall s. KnownIntSet s => HashSet s Int
+intSet2HashSet = reify
+  (HashSet.fromList $ IntSet.toList $ reflect $ Proxy @s)
+  unsafeWrapHashSet
+
+intMap2HashMap :: forall s a. IntMap s a -> HashMap s Int a
+intMap2HashMap (IntMap m) = HashMap $ HashMap.fromList $ IntMap.toList m
+
+hashSet2Set :: forall s a. (Ord a, KnownHashSet s a) => Set s a
+hashSet2Set = reify
+  (Set.fromList $ HashSet.toList $ reflect $ Proxy @s)
+  unsafeWrapSet
+
+hashMap2Map :: forall s k a. Ord k => HashMap s k a -> Map s k a
+hashMap2Map (HashMap m) = Map $ Map.fromList $ HashMap.toList m
+
+hashSet2IntSet :: forall s. KnownHashSet s Int => IntSet s
+hashSet2IntSet = reify
+  (IntSet.fromList $ HashSet.toList $ reflect $ Proxy @s)
+  unsafeWrapIntSet
+
+hashMap2IntMap :: forall s a. HashMap s Int a -> IntMap s a
+hashMap2IntMap (HashMap m) = IntMap $ IntMap.fromList $ HashMap.toList m

src/Data/Container/Refined/Hashable.hs

@@ -0,0 +1,13 @@
+{-# LANGUAGE CPP #-}
+module Data.Container.Refined.Hashable
+  ( Hashable
+  ) where
+
+#if MIN_VERSION_hashable(1, 4, 0)
+import           Data.Hashable (Hashable)
+#else
+import qualified Data.Hashable as Hashable
+
+
+type Hashable a = (Eq a, Hashable.Hashable a)
+#endif