type-combinators-singletons (empty) → 0.1.0.0
raw patch · 6 files changed
+268/−0 lines, 6 filesdep +basedep +singletonsdep +type-combinatorssetup-changed
Dependencies added: base, singletons, type-combinators
Files
- CHANGELOG.md +12/−0
- LICENSE +30/−0
- README.md +15/−0
- Setup.hs +2/−0
- src/Data/Type/Combinator/Singletons.hs +169/−0
- type-combinators-singletons.cabal +40/−0
+ CHANGELOG.md view
@@ -0,0 +1,12 @@+Changelog+=========++Version 0.1.0.0+---------------++*Sep 1, 2017*++<https://github.com/mstksg/type-combinators-singletons/releases/tag/v0.1.0.0>++* Initial release.+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Justin Le (c) 2017++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 Justin Le 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,15 @@+type-combinator-singletons+==========================++Conversions between data-types in *[type-combinators][]* and singletons from+*[singletons][]*.++[type-combinators]: https://hackage.haskell.org/package/type-combinators+[singletons]: https://hackage.haskell.org/package/singletons++There's a lot of overlap in functionality between the two libraries. I often+use both of them together side-by-side to do different things, but there is+some friction the process of converting between the identical data types that+both libraries have, and between similar typeclasses. This library attempts to+ease that friction by providing conversion functions between identical data+types and also many of the appropriate typeclass instances.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Data/Type/Combinator/Singletons.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++-- |+-- Module : Data.Type.Combinator.Singletons+-- Description : Conversions between datatypes in /type-combinators/ and+-- singletons from /singletons/.+-- Copyright : (c) Justin Le 2017+-- License : BSD-3+-- Maintainer : justin@jle.im+-- Stability : unstable+-- Portability : portable+--+-- There's a lot of identical data types between /type-combinators/ and+-- /singetons/, as well as similar typeclasses. This module provides+-- conversion functions between the two, and also many appropriate+-- instances.+--++module Data.Type.Combinator.Singletons (+ prodSing+ , singProd+ , singLength+ , boolSing+ , singBool+ , Sing(SZ, SS), SN, ZSym0, SSym0, SSym1+ , natSing+ , singNat+ , parSing+ , singPar+ , choiceSing+ , singChoice+ , optionSing+ , singOption+ ) where++import Data.Kind+import Data.Singletons+import Data.Singletons.Prelude+import Data.Singletons.TH+import Data.Type.Boolean+import Data.Type.Conjunction+import Data.Type.Disjunction+import Data.Type.Length+import Data.Type.Option+import Data.Type.Product+import Type.Class.Higher+import Type.Class.Known+import Data.Type.Nat+import Type.Class.Witness+import Type.Family.Constraint+import Type.Family.Nat++instance SingI a => Known Sing a where+ type KnownC Sing a = SingI a+ known = sing++instance Witness ØC (SingI a) (Sing a) where+ x \\ s = withSingI s x++instance SEq k => Eq1 (Sing :: k -> Type) where+ eq1 x y = fromSing $ x %:== y+ neq1 x y = fromSing $ x %:/= y++instance SOrd k => Ord1 (Sing :: k -> Type) where+ compare1 x y = fromSing $ sCompare x y+ x <# y = fromSing $ x %:< y+ x ># y = fromSing $ x %:> y+ x <=# y = fromSing $ x %:<= y+ x >=# y = fromSing $ x %:>= y++-- | Convert a 'Prod' of 'Sing's of individual values in @as@ to a 'Sing'+-- for all @as@ together.+prodSing :: Prod Sing as -> Sing as+prodSing = \case+ Ø -> SNil+ x :< xs -> x `SCons` prodSing xs++-- | Convert a 'Sing' for @as@ to a 'Prod' of 'Sing's of each individual+-- value in @as@.+singProd :: Sing as -> Prod Sing as+singProd = \case+ SNil -> Ø+ x `SCons` xs -> x :< singProd xs++-- | Convert a 'Sing' for @as@ into a 'Length' representing the length of+-- @as@.+--+-- @'Length' as@ is equivalent to @'Prod' 'Proxy' as@, so this is basically+--+-- @+-- 'singLength' = 'map1' ('const' 'Proxy') . 'singProd'+-- @+singLength :: Sing as -> Length as+singLength = \case+ SNil -> LZ+ _ `SCons` xs -> LS (singLength xs)++-- | Convert a 'Boolean' singleton for @a@ into the 'Sing' singleton for+-- @a@.+boolSing :: Boolean b -> Sing b+boolSing = \case+ False_ -> SFalse+ True_ -> STrue++-- | Convert a 'Sing' singleton for @b@ to a 'Boolean' singleton for @b@.+singBool :: Sing b -> Boolean b+singBool = \case+ SFalse -> False_+ STrue -> True_++genSingletons [''N]++-- | Convert a 'Nat' singleton for @n@ to a 'Sing' singleton for @n@.+natSing :: Nat n -> Sing n+natSing = \case+ Z_ -> SZ+ S_ n -> SS (natSing n)++-- | Convert a 'Sing' singleton for @n@ to a 'Nat' singleton for @n@.+singNat :: Sing n -> Nat n+singNat = \case+ SZ -> Z_+ SS n -> S_ (singNat n)++-- | Convert a ':*:' tupling of @'Sing' a@ and @'Sing' b@ into a single+-- 'Sing' for @'(a, b)@.+parSing :: (Sing :*: Sing) '(a, b) -> Sing '(a, b)+parSing (x :*: y) = STuple2 x y++-- | Convert a 'Sing' of @'(a, b)@ to a ':*:' tupling of @'Sing' a@ and+-- @'Sing' b@.+singPar :: Sing '(a, b) -> (Sing :*: Sing) '(a, b)+singPar (STuple2 x y) = x :*: y++-- | Convert a ':+:' sum between a @'Sing' a@ and @'Sing' b@ into+-- a 'Sing' of a sum ('Either') of @a@ and @b@.+choiceSing :: (Sing :+: Sing) e -> Sing e+choiceSing = \case+ L' x -> SLeft x+ R' x -> SRight x++-- | Convert a 'Sing' of a sum ('Either') of @a@ and @b@ to a ':+:' sum+-- between @'Sing' a@ and @'Sing' b@.+singChoice :: Sing e -> (Sing :+: Sing) e+singChoice = \case+ SLeft x -> L' x+ SRight x -> R' x++-- | Convert an 'Option' of @'Sing' a@ to a 'Sing' of an optional ('Maybe')+-- @a@.+optionSing :: Option Sing a -> Sing a+optionSing = \case+ Nothing_ -> SNothing+ Just_ x -> SJust x++-- | Convert a 'Sing' of an optional ('Maybe') @a@ to an 'Option' of+-- @'Sing' a@.+singOption :: Sing a -> Option Sing a+singOption = \case+ SNothing -> Nothing_+ SJust x -> Just_ x
+ type-combinators-singletons.cabal view
@@ -0,0 +1,40 @@+name: type-combinators-singletons+version: 0.1.0.0+synopsis: Interop between /type-combinators/ and /singletons/.+description: Conversions between datatypes in /type-combinators/ and+ singletons from /singletons/.+homepage: https://github.com/mstksg/type-combinators-singletons+license: BSD3+license-file: LICENSE+author: Justin Le+maintainer: justin@jle.im+copyright: (c) Justin Le 2017+category: Data+build-type: Simple+extra-source-files: README.md+ CHANGELOG.md+cabal-version: >=1.10+tested-with: GHC == 8.0.2+ , GHC == 8.2.1++library+ hs-source-dirs: src+ exposed-modules: Data.Type.Combinator.Singletons+ build-depends: base >= 4.9 && < 5+ , type-combinators+ , singletons+ default-language: Haskell2010+ ghc-options: -Wall++-- test-suite type-combinators-singletons-test+-- type: exitcode-stdio-1.0+-- hs-source-dirs: test+-- main-is: Spec.hs+-- build-depends: base+-- , type-combinators-singletons+-- ghc-options: -threaded -rtsopts -with-rtsopts=-N+-- default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/mstksg/type-combinators-singletons