diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,12 @@ +Changelog +========= + +Version 0.1.0.0 +--------------- + +*Sep 1, 2017* + + + +* Initial release. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. 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/Type/Combinator/Singletons.hs b/src/Data/Type/Combinator/Singletons.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Combinator/Singletons.hs @@ -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 diff --git a/type-combinators-singletons.cabal b/type-combinators-singletons.cabal new file mode 100644 --- /dev/null +++ b/type-combinators-singletons.cabal @@ -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