diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Louis Pan (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 Louis Pan 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,11 @@ +[![Hackage](https://img.shields.io/hackage/v/data-diverse.svg)](https://hackage.haskell.org/package/data-diverse) +[![Build Status](https://secure.travis-ci.org/louispan/data-diverse.png?branch=master)](http://travis-ci.org/louispan/data-diverse) + +"Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Int, Map Int Any). + +"Data.Diverse.Which" polymorphic variant of possibilities encoded as (Int, Any). + +Provides getters, setters, projection, injection, fold, and catamorphisms; +accessed by type or index. + +Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages. 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/data-diverse.cabal b/data-diverse.cabal new file mode 100644 --- /dev/null +++ b/data-diverse.cabal @@ -0,0 +1,63 @@ +name: data-diverse +version: 0.1.0.0 +synopsis: Extensible records and polymorphic variants. +description: "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Int, Map Int Any). + "Data.Diverse.Which" polymorphic variant of possibilities encoded as (Int, Any). + Provides getters, setters, projection, injection, fold, and catamorphisms; + accessed by type or index. + Refer to [ManySpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/ManySpec.hs) and [WhichSpec.hs](https://github.com/louispan/data-diverse/blob/master/test/Data/Diverse/WhichSpec.hs) for example usages. +homepage: https://github.com/louispan/data-distinct#readme +license: BSD3 +license-file: LICENSE +author: Louis Pan +maintainer: louis@pan.me +copyright: 2017 Louis Pan +category: Data, Records +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 +tested-with: GHC == 8.0.1 + +library + hs-source-dirs: src + exposed-modules: Data.Diverse.AFoldable + Data.Diverse + Data.Diverse.Case + Data.Diverse.Cases + Data.Diverse.CaseTypeable + Data.Diverse.Collector + Data.Diverse.Emit + Data.Diverse.Many + Data.Diverse.Many.Internal + Data.Diverse.PackageId + Data.Diverse.Reduce + Data.Diverse.Reiterate + Data.Diverse.Type + Data.Diverse.Type.Internal + Data.Diverse.Which + Data.Diverse.Which.Internal + build-depends: base >= 4.7 && < 5 + , containers >= 0.5 && < 0.6 + , ghc-prim >= 0.5 && < 1 + , lens >= 4 && < 5 + , tagged >= 0.8.5 && < 1 + ghc-options: -Wall + default-language: Haskell2010 + +test-suite data-diverse-test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Spec.hs + other-modules: Data.Diverse.ManySpec + Data.Diverse.TypeSpec + Data.Diverse.WhichSpec + build-depends: base + , data-diverse + , hspec >= 2 && < 3 + , lens >= 4 && < 5 + ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall + default-language: Haskell2010 + +source-repository head + type: git + location: https://github.com/louispan/data-diverse diff --git a/src/Data/Diverse.hs b/src/Data/Diverse.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse.hs @@ -0,0 +1,25 @@ +module Data.Diverse + ( module Data.Diverse.AFoldable + , module Data.Diverse.Case + , module Data.Diverse.Cases + , module Data.Diverse.CaseTypeable + , module Data.Diverse.Collector + , module Data.Diverse.Emit + , module Data.Diverse.Many + , module Data.Diverse.Reduce + , module Data.Diverse.Reiterate + , module Data.Diverse.Type + , module Data.Diverse.Which + ) where + +import Data.Diverse.AFoldable +import Data.Diverse.Case +import Data.Diverse.Cases +import Data.Diverse.CaseTypeable +import Data.Diverse.Collector +import Data.Diverse.Emit +import Data.Diverse.Many +import Data.Diverse.Reduce +import Data.Diverse.Reiterate +import Data.Diverse.Type +import Data.Diverse.Which diff --git a/src/Data/Diverse/AFoldable.hs b/src/Data/Diverse/AFoldable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/AFoldable.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE MultiParamTypeClasses #-} + +module Data.Diverse.AFoldable where + +-- | Constrained Foldable for a specified type instead for all types. +class AFoldable t a where + afoldr :: (a -> b -> b) -> b -> t a -> b + +afoldl' :: AFoldable t a => (b -> a -> b) -> b -> t a -> b +afoldl' f z0 xs = afoldr f' id xs z0 + where f' x k z = k $! f z x diff --git a/src/Data/Diverse/Case.hs b/src/Data/Diverse/Case.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Case.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Diverse.Case where + +import Data.Diverse.Type +import Data.Kind + +-- | This class allows defining handlers that can handle the 'Head' type in the @xs@ typelist. +-- In conjunction with 'Data.Diverse.Reiterate.Reiterate', you can define handlers that can handle all +-- the types in the @xs@ typelist. +-- +-- See "Data.Diverse.CaseTypeable" and "Data.Diverse.Cases". +class Case c (xs :: [Type]) r where + -- | Return the handler/continuation when x is observed. + case' :: c xs r -> (Head xs -> r) diff --git a/src/Data/Diverse/CaseTypeable.hs b/src/Data/Diverse/CaseTypeable.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/CaseTypeable.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} + +module Data.Diverse.CaseTypeable where + +import Data.Diverse.Case +import Data.Diverse.Reiterate +import Data.Diverse.Type +import Data.Kind +import Data.Typeable + +-- | This handler stores a polymorphic function for all Typeables. +-- +-- @ +-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] +-- 'Data.Diverse.Which.switch' y ('CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` "Int" +-- @ +-- +-- @ +-- let x = (5 :: Int) 'Data.Diverse.Many../' False 'Data.Diverse.Many../' \'X' 'Data.Diverse.Many../' Just \'O' 'Data.Diverse.Many../' (6 :: Int) 'Data.Diverse.Many../' Just \'A' 'Data.Diverse.Many../' 'Data.Diverse.Many.nul' +-- 'Data.Diverse.AFoldable.afoldr' (:) [] ('Data.Diverse.Many.forMany' ('CaseTypeable' (show . typeRep . (pure @Proxy))) x) \`shouldBe` +-- [\"Int", \"Bool", \"Char", \"Maybe Char", \"Int", \"Maybe Char"] +-- @ +newtype CaseTypeable (xs :: [Type]) r = CaseTypeable (forall x. Typeable x => x -> r) + +instance Reiterate CaseTypeable xs where + reiterate (CaseTypeable f) = CaseTypeable f + +instance Typeable (Head xs) => Case CaseTypeable xs r where + case' (CaseTypeable f) = f diff --git a/src/Data/Diverse/Cases.hs b/src/Data/Diverse/Cases.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Cases.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +module Data.Diverse.Cases + ( Cases(..) + , cases + , CasesN + , casesN + ) where + +import Data.Diverse.Case +import Data.Diverse.Many +import Data.Diverse.Reiterate +import Data.Diverse.Type +import Data.Kind +import Data.Proxy +import GHC.TypeLits + +-- | Contains a 'Many' of handlers/continuations for all the types in the 'xs' typelist. +-- This uses __'fetch'__ to get the unique handler for the type at the 'Head' of @xs@. +-- +-- Use 'cases' to construct this with 'SameLength' constraint to reduce programming confusion. +-- However, the 'Cases' constructor is still exported to allow creating a master-of-all-'Case'. +newtype Cases (fs :: [Type]) (xs :: [Type]) r = Cases (Many fs) + +instance Reiterate (Cases fs) xs where + reiterate (Cases s) = Cases s + +-- | UndecidableInstances because @fs@ appers more often. +instance UniqueMember (Head xs -> r) fs => Case (Cases fs) xs r where + case' (Cases s) = fetch @(Head xs -> r) s + +-- | Create an instance of 'Case' for either handling 'Data.Diverse.Which.switch'ing a 'Which'. +-- +-- @ +-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] +-- 'Data.Diverse.Which.switch' y ( +-- 'cases' (show \@Bool +-- './' show \@Int +-- './' 'nul')) \`shouldBe` "5" +-- @ +-- +-- Or for handling 'collect' from a 'Many'. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Char './' show \@(Maybe Char) './' show \@Bool './' 'nul' +-- 'Data.Diverse.AFoldable.afoldr' (:) [] ('collect' x ('cases' y)) \`shouldBe` +-- [\"5", \"False", \"'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +-- +-- This function imposes additional @SameLength@ constraints than when using the 'Cases' constructor directly. +-- It is better practice to use 'cases' to prevent programming confusion with dead code. +-- However, the 'Cases' constructor is still exported to allow creating a master-of-all-'Case'. +cases :: SameLength fs (Distinct xs) => Many fs -> (Cases fs) xs r +cases = Cases + +----------------------------------------------- + +-- | A variation of 'Cases' which uses __'fetchN'__ to get the handler by index. +-- There may be different handlers for the same type, but the handlers must be in the same order +-- as the input @xs@ typelist. +-- Use 'casesN' to construct this safely ensuring @n@ starts at 0. +newtype CasesN (fs :: [Type]) (n :: Nat) (xs :: [Type]) r = CasesN (Many fs) + +instance ReiterateN (CasesN fs) n xs where + reiterateN (CasesN s) = CasesN s + +-- | UndecidableInstances because @fs@ appears more often. +instance (MemberAt n (Head xs -> r) fs) => Case (CasesN fs n) xs r where + case' (CasesN s) = fetchN (Proxy @n) s + +-- | Safe Constructor for 'CasesN' ensuring that the @n@ Nat starts at 0. +-- It is an instance of 'CaseN' for either handling 'Data.Diverse.Which.switchN'ing a 'Which' in index order. +-- +-- @ +-- let y = 'Data.Diverse.Which.pickN' @0 Proxy (5 :: Int) :: Which '[Int, Bool, Bool, Int] +-- 'Data.Diverse.Which.switchN' y ( +-- 'casesN' (show \@Int +-- './' show \@Bool +-- './' show \@Bool +-- './' show \@Int +-- './' 'nul')) \`shouldBe` "5" +-- @ +-- +-- Or for handling 'collectN' from a 'Many'. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Bool './' show \@Char './' show \@(Maybe Char) './' show \@Int './' show \@(Maybe Char) './' 'nul' +-- 'Data.Diverse.AFoldable.afoldr' (:) [] ('collectN' x ('casesN' y)) \`shouldBe` +-- [\"5", \"False", \"'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +casesN :: SameLength fs xs => Many fs -> CasesN fs 0 xs r +casesN = CasesN diff --git a/src/Data/Diverse/Collector.hs b/src/Data/Diverse/Collector.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Collector.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Diverse.Collector where + +import Data.Diverse.AFoldable +import Data.Diverse.Emit +import Data.Diverse.Reiterate +import Data.Kind +import GHC.TypeLits + +-- | Folds output from an 'Emit'ter of values while __'reiterate'__ing the @xs@ typelist. +-- This guarantees that the @Emit e '[]@ is not instantiated. +-- Undecidable instances! But this is safe since it's a wrapper +newtype Collector e (xs :: [Type]) r = Collector (e xs r) + +-- | null case that doesn't even use 'emit', so that an instance of @Emit e '[]@ is not needed. +instance AFoldable (Collector e '[]) r where + afoldr _ z _ = z + +-- | Folds values by 'reiterate'ing 'Emit'ters through the @xs@ typelist. +instance ( Emit e (x ': xs) r + , Reiterate e (x ': xs) + , AFoldable (Collector e xs) r + ) => + AFoldable (Collector e (x ': xs)) r where + afoldr f z (Collector e) = f (emit e) (afoldr f z (Collector (reiterate e))) + +-- | A variation of 'Collector' which does require the @Emit e '[]@ instance for the empty typelist. +-- Undecidable instances! But this is safe since it's a wrapper +newtype Collector0 e (xs :: [Type]) r = Collector0 (e xs r) + +-- | terminating case that does use @Emit e '[]@ +instance (Emit e '[] r) => + AFoldable (Collector0 e '[]) r where + afoldr f z (Collector0 e) = f (emit e) z + +-- | Folds values by 'reiterate'ing 'Emit'ters through the @xs@ typelist. +instance ( Emit e (x ': xs) r + , Reiterate e (x ': xs) + , AFoldable (Collector0 e xs) r + ) => + AFoldable (Collector0 e (x ': xs)) r where + afoldr f z (Collector0 e) = f (emit e) (afoldr f z (Collector0 (reiterate e))) + +-------------------------------------------- + +-- | A variation of 'Collector' which __'reiterateN'__s the @xs@ typelist. +-- This version guarantees that the @Emit (e n) '[]@ is not instantiated. +-- Undecidable instances! But this is safe since it's a wrapper +newtype CollectorN e (n :: Nat) (xs :: [Type]) r = CollectorN (e n xs r) + +-- | null case that doesn't even use 'emit', so that an instance of @Emit (e n) '[]@ is not needed. +instance AFoldable (CollectorN e n '[]) r where + afoldr _ z _ = z + +-- | Folds values by 'reiterateN'ing 'Emit'ters through the @xs@ typelist. +instance ( Emit (e n) (x ': xs) r + , ReiterateN e n (x ': xs) + , AFoldable (CollectorN e (n + 1) xs) r + ) => + AFoldable (CollectorN e n (x ': xs)) r where + afoldr f z (CollectorN e) = f (emit e) (afoldr f z (CollectorN (reiterateN e))) + +-- | A variation of 'Collector0' which __'reiterateN'__s the @xs@ typelist. +-- Undecidable instances! But this is safe since it's a wrapper +newtype CollectorN0 e (n :: Nat) (xs :: [Type]) r = CollectorN0 (e n xs r) + +-- | terminating case that does use @Emit (e n) '[]@ +instance (Emit (e n) '[] r) => + AFoldable (CollectorN0 e n '[]) r where + afoldr f z (CollectorN0 e) = f (emit e) z + +-- | Folds values by 'reiterateN'ing 'Emit'ters through the @xs@ typelist. +instance ( Emit (e n) (x ': xs) r + , ReiterateN e n (x ': xs) + , AFoldable (CollectorN0 e (n + 1) xs) r + ) => + AFoldable (CollectorN0 e n (x ': xs)) r where + afoldr f z (CollectorN0 e) = f (emit e) (afoldr f z (CollectorN0 (reiterateN e))) diff --git a/src/Data/Diverse/Emit.hs b/src/Data/Diverse/Emit.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Emit.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} + +module Data.Diverse.Emit where + +-- | 'Emit' can generate a value, and is differentiated with an additional @xs@ typelist +class Emit e (xs :: [k]) r where + emit :: e xs r -> r diff --git a/src/Data/Diverse/Many.hs b/src/Data/Diverse/Many.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Many.hs @@ -0,0 +1,72 @@ +-- | Re-export Many without the constructor +module Data.Diverse.Many ( + -- * 'Many' type + Many -- Hiding constructor + + -- * Isomorphism + , IsMany(..) + , fromMany' + , toMany' + , _Many + , _Many' + + -- * Construction + , nul + , single + , prefix + , (./) + , postfix + , (\.) + , append + , (/./) + + -- * Simple queries + , front + , back + , aft + , fore + + -- * Single field + -- ** Getter for single field + , fetch + , (.^.) + , fetchN + -- ** Setter for single field + , replace + , (.~.) + , replaceN + -- ** Lens for a single field + , item + , itemN + + -- * Multiple fields + -- ** Getter for multiple fields + , Narrow + , narrow + , (\^.) + , NarrowN + , narrowN + -- ** Setter for multiple fields + , Amend + , amend + , (\~.) + , AmendN + , amendN + -- ** Lens for multiple fields + , project + , projectN + + -- * Destruction + -- ** By type + , Via -- no constructor + , via -- safe construction + , forMany + , collect + -- ** By Nat index offset + , ViaN -- no constructor + , viaN -- safe construction + , forManyN + , collectN + ) where + +import Data.Diverse.Many.Internal diff --git a/src/Data/Diverse/Many/Internal.hs b/src/Data/Diverse/Many/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Many/Internal.hs @@ -0,0 +1,937 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Diverse.Many.Internal ( + -- * 'Many' type + Many(..) -- Exporting constructor unsafely! + + -- * Isomorphism + , IsMany(..) + , fromMany' + , toMany' + , _Many + , _Many' + + -- * Construction + , nul + , single + , prefix + , (./) + , postfix + , (\.) + , append + , (/./) + + -- * Simple queries + , front + , back + , aft + , fore + + -- * Single field + -- ** Getter for single field + , fetch + , (.^.) + , fetchN + -- ** Setter for single field + , replace + , (.~.) + , replaceN + -- ** Lens for a single field + , item + , itemN + + -- * Multiple fields + -- ** Getter for multiple fields + , Narrow + , narrow + , (\^.) + , NarrowN + , narrowN + -- ** Setter for multiple fields + , Amend + , amend + , (\~.) + , AmendN + , amendN + -- ** Lens for multiple fields + , project + , projectN + + -- * Destruction + -- ** By type + , Via -- no constructor + , via -- safe construction + , forMany + , collect + -- ** By Nat index offset + , ViaN -- no constructor + , viaN -- safe construction + , forManyN + , collectN + ) where + +import Control.Applicative +import Control.Lens +import Data.Bool +import Data.Diverse.AFoldable +import Data.Diverse.Case +import Data.Diverse.Collector +import Data.Diverse.Emit +import Data.Diverse.PackageId +import Data.Diverse.Reiterate +import Data.Diverse.Type +import Data.Kind +import qualified Data.Map.Strict as M +import Data.Proxy +import Data.Tagged +import qualified GHC.Generics as G +import GHC.Prim (Any, coerce) +import GHC.TypeLits +import Text.ParserCombinators.ReadPrec +import Text.Read +import qualified Text.Read.Lex as L +import Unsafe.Coerce + +-- This module uses the partial 'head', 'tail' from Prelude. +-- I like to highlight them as partial by using them in the namespace Partial.head +-- These usages in this module are safe due to size guarantees provided by the typelist. +import Prelude as Partial + +newtype Key = Key Int deriving (Eq, Ord, Show) +newtype LeftOffset = LeftOffset Int +newtype LeftSize = LeftSize Int +newtype RightOffset = RightOffset Int +newtype NewRightOffset = NewRightOffset { unNewRightOffset :: Int } + +-- | A Many is an anonymous product type (also know as polymorphic record), with no limit on the number of fields. +-- +-- The following functions are available can be used to manipulate unique fields +-- +-- * getter/setter for single field: 'fetch' and 'replace' +-- * getter/setter for multiple fields: 'narrow' and 'amend' +-- * folds: 'forMany' or 'collect' +-- +-- These functions are type specified. This means labels are not required because the types themselves can be used to access the 'Many. +-- It is a compile error to use those functions for duplicate fields. +-- +-- For duplicate fields, Nat-indexed versions of the functions are available: +-- +-- * getter/setter for single field: 'fetchN' and 'replaceN' +-- * getter/setter for multiple fields: 'narrowN' and 'amendN' +-- * folds: 'forManyN' or 'collectN' +-- +-- Encoding: The record is encoded as (Offset, Map Int Any). +-- This encoding should reasonabily efficient for any number of fields. +-- +-- The map Key is index + offset of the type in the typelist. +-- The Offset is used to allow efficient cons 'prefix'. +-- +-- @Key = Index of type in typelist + Offset@ +-- +-- The constructor will guarantee the correct number and types of the elements. +-- The constructor is only exported in the "Data.Diverse.Many.Internal" module +data Many (xs :: [Type]) = Many {-# UNPACK #-} !Int (M.Map Key Any) + +-- | Inferred role is phantom which is incorrect +type role Many representational + +----------------------------------------------------------------------- + +-- | A terminating 'G.Generic' instance encoded as a 'nul'. +instance G.Generic (Many '[]) where + type Rep (Many '[]) = G.D1 ('G.MetaData + "Many" + "Data.Diverse.Many.Internal" + PackageId + 'False) G.U1 + from _ = {- G.D1 -} G.M1 {- G.U1 -} G.U1 + to (G.M1 G.U1) = nul + +-- | A 'G.Generic' instance encoded as the 'front' value 'G.:*:' with the 'aft' 'Many'. +-- The 'G.C1' and 'G.S1' metadata are not encoded. +instance G.Generic (Many (x ': xs)) where + type Rep (Many (x ': xs)) = G.D1 ('G.MetaData + "Many" + "Data.Diverse.Many.Internal" + PackageId + 'False) ((G.Rec0 x) G.:*: (G.Rec0 (Many xs))) + from r = {- G.D1 -} G.M1 (({- G.Rec0 -} G.K1 (front r)) G.:*: ({- G.Rec0 -} G.K1 (aft r))) + to ({- G.D1 -} G.M1 (({- G.Rec0 -} G.K1 a) G.:*: ({- G.Rec0 -} G.K1 b))) = a ./ b + +----------------------------------------------------------------------- + +-- | This instance allows converting to and from Many +-- There are instances for converting tuples of up to size 15. +class IsMany t xs a where + toMany :: t xs a -> Many xs + fromMany :: Many xs -> t xs a + +-- | Converts from a value (eg a tuple) to a 'Many', via a 'Tagged' wrapper +toMany' :: IsMany Tagged xs a => a -> Many xs +toMany' a = toMany (Tagged a) + +-- | Converts from a Many to a value (eg a tuple), via a Tagged wrapper +fromMany' :: IsMany Tagged xs a => Many xs -> a +fromMany' = unTagged . fromMany + +-- | @_Many = iso fromMany toMany@ +_Many :: IsMany t xs a => Iso' (Many xs) (t xs a) +_Many = iso fromMany toMany + +-- | @_Many' = iso fromMany' toMany'@ +_Many' :: IsMany Tagged xs a => Iso' (Many xs) a +_Many' = iso fromMany' toMany' + +-- | These instances add about 7 seconds to the compile time! +instance IsMany Tagged '[] () where + toMany _ = nul + fromMany _ = Tagged () + +-- | This single field instance is the reason for 'Tagged' wrapper. +-- Otherwise this instance will overlap. +instance IsMany Tagged '[a] a where + toMany (Tagged a) = single a + fromMany r = Tagged (fetch @a r) + +instance IsMany Tagged '[a,b] (a,b) where + toMany (Tagged (a,b)) = a./b./nul + fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r) + +instance IsMany Tagged '[a,b,c] (a,b,c) where + toMany (Tagged (a,b,c)) = a./b./c./nul + fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r) + +instance IsMany Tagged '[a,b,c,d] (a,b,c,d) where + toMany (Tagged (a,b,c,d)) = a./b./c./d./nul + fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r) + +instance IsMany Tagged '[a,b,c,d,e] (a,b,c,d,e) where + toMany (Tagged (a,b,c,d,e)) = a./b./c./d./e./nul + fromMany r = Tagged (fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r) + +instance IsMany Tagged '[a,b,c,d,e,f] (a,b,c,d,e,f) where + toMany (Tagged (a,b,c,d,e,f)) = a./b./c./d./e./f./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g] (a,b,c,d,e,f,g) where + toMany (Tagged (a,b,c,d,e,f,g)) = a./b./c./d./e./f./g./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h] (a,b,c,d,e,f,g,h) where + toMany (Tagged (a,b,c,d,e,f,g,h)) = a./b./c./d./e./f./g./h./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i] (a,b,c,d,e,f,g,h,i) where + toMany (Tagged (a,b,c,d,e,f,g,h,i)) = a./b./c./d./e./f./g./h./i./ nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j] (a,b,c,d,e,f,g,h,i,j) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j)) = a./b./c./d./e./f./g./h./i./j./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k] (a,b,c,d,e,f,g,h,i,j,k) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k)) = a./b./c./d./e./f./g./h./i./j./k./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r + , fetchN (Proxy @10) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l] (a,b,c,d,e,f,g,h,i,j,k,l) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l)) = a./b./c./d./e./f./g./h./i./j./k./l./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r + , fetchN (Proxy @10) r, fetchN (Proxy @11) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m] (a,b,c,d,e,f,g,h,i,j,k,l,m) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m)) = a./b./c./d./e./f./g./h./i./j./k./l./m./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r + , fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m,n] (a,b,c,d,e,f,g,h,i,j,k,l,m,n) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m,n)) = a./b./c./d./e./f./g./h./i./j./k./l./m./n./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r + , fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r, fetchN (Proxy @13) r) + +instance IsMany Tagged '[a,b,c,d,e,f,g,h,i,j,k,l,m,n,o] (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o) where + toMany (Tagged (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)) = a./b./c./d./e./f./g./h./i./j./k./l./m./n./o./nul + fromMany r = Tagged ( fetchN (Proxy @0) r, fetchN (Proxy @1) r, fetchN (Proxy @2) r, fetchN (Proxy @3) r, fetchN (Proxy @4) r + , fetchN (Proxy @5) r, fetchN (Proxy @6) r, fetchN (Proxy @7) r, fetchN (Proxy @8) r, fetchN (Proxy @9) r + , fetchN (Proxy @10) r, fetchN (Proxy @11) r, fetchN (Proxy @12) r, fetchN (Proxy @13) r, fetchN (Proxy @14) r) + +----------------------------------------------------------------------- + +-- | When appending two maps together, get the function to 'M.mapKeys' the RightMap +-- when adding RightMap into LeftMap. +-- The existing contents of LeftMap will not be changed. +-- LeftMap Offset will also not change. +-- The desired key for element from the RightMap = RightIndex (of the element) + LeftOffset + LeftSize +-- OldRightKey = RightIndex + RightOffset, therefore RightIndex = OldRightKey - RightOffset +-- So we need to adjust the existing index on the RightMap by +-- \OldRightKey -> RightIndex + LeftOffset + LeftSize (as above) +-- \OldRightKey -> OldRightKey - RightOffset + LeftOffset + LeftSize +rightKeyForSnoc :: LeftOffset -> LeftSize -> RightOffset -> Key -> Key +rightKeyForSnoc (LeftOffset lo) (LeftSize ld) (RightOffset ro) (Key rk) = + Key (rk - ro + lo + ld) + +-- | When appending two maps together, get the function to modify the RightMap's offset +-- when adding LeftMap into RightMap. +-- The existing contents of RightMap will not be changed. +-- NewRightOffset = OldRightOffset - LeftSize +rightOffsetForCons :: LeftSize -> RightOffset -> NewRightOffset +rightOffsetForCons (LeftSize ld) (RightOffset ro) = NewRightOffset (ro - ld) + +-- | When appending two maps together, get the function to 'M.mapKeys' the LeftMap +-- when adding LeftMap into RightMap. +-- The existing contents of RightMap will not be changed. +-- The RightMap's offset will be adjusted using 'rightOffsetWithRightMapUnchanged' +-- The desired key for the elements in the the LeftMap = LeftIndex (of the element) + NewRightOffset +-- OldLeftKey = LeftIndex + LeftOffset, therefore LeftIndex = OldLeftKey - LeftOffset +-- So we need to adjust the existing index on the LeftMap by +-- \OldLeftKey -> LeftIndex + NewRightOffset (as above) +-- \OldLeftKey -> OldLeftKey - LeftOffset + NewRightOffset (as above) +leftKeyForCons :: LeftOffset -> NewRightOffset -> Key -> Key +leftKeyForCons (LeftOffset lo) (NewRightOffset ro) (Key lk) = Key (lk - lo + ro) + +-- | Analogous to 'Prelude.null'. Named 'nul' to avoid conflicting with 'Prelude.null'. +nul :: Many '[] +nul = Many 0 M.empty +infixr 5 `nul` -- to be the same as 'prefix' + +-- | Create a Many from a single value. Analogous to 'M.singleton' +single :: x -> Many '[x] +single v = Many 0 (M.singleton (Key 0) (unsafeCoerce v)) + +-- | Add an element to the left of a Many. +-- Not named @cons@ to avoid conflict with 'Control.Lens.cons' +prefix :: x -> Many xs -> Many (x ': xs) +prefix x (Many ro rm) = Many (unNewRightOffset nro) + (M.insert + (leftKeyForCons (LeftOffset 0) nro (Key 0)) + (unsafeCoerce x) + rm) + where + nro = rightOffsetForCons (LeftSize 1) (RightOffset ro) +infixr 5 `prefix` + +-- | Infix version of 'prefix'. +-- +-- Mnemonic: Element on the left is smaller './' than the larger 'Many' to the right. +(./) :: x -> Many xs -> Many (x ': xs) +(./) = prefix +infixr 5 ./ -- like Data.List.(:) + +-- | Add an element to the right of a Many +-- Not named 'snoc' to avoid conflict with 'Control.Lens.snoc' +postfix :: Many xs -> y -> Many (Append xs '[y]) +postfix (Many lo lm) y = Many lo + (M.insert (rightKeyForSnoc (LeftOffset lo) (LeftSize (M.size lm)) (RightOffset 0) (Key 0)) + (unsafeCoerce y) + lm) +infixl 5 `postfix` + +-- | 'snoc' mnemonic: Many is larger '\.' than the smaller element +(\.) :: Many xs -> y -> Many (Append xs '[y]) +(\.) = postfix +infixl 5 \. + +-- | 'append' mnemonic: 'cons' './' with an extra slash (meaning 'Many') in front. +(/./) :: Many xs -> Many ys -> Many (Append xs ys) +(/./) = append +infixr 5 /./ -- like (++) + +-- | Appends two Manys together +append :: Many xs -> Many ys -> Many (Append xs ys) +append (Many lo lm) (Many ro rm) = if ld >= rd + then Many + lo + (lm `M.union` (M.mapKeys (rightKeyForSnoc (LeftOffset lo) (LeftSize ld) (RightOffset ro)) rm)) + else Many + (unNewRightOffset nro) + ((M.mapKeys (leftKeyForCons (LeftOffset lo) nro) lm) `M.union` rm) + where + ld = M.size lm + rd = M.size rm + nro = rightOffsetForCons (LeftSize ld) (RightOffset ro) +infixr 5 `append` -- like Data.List (++) + +----------------------------------------------------------------------- + +-- | Extract the first element of a Many, which guaranteed to be non-empty. +-- Analogous to 'Partial.head' +front :: Many (x ': xs) -> x +front (Many _ m) = unsafeCoerce (snd . Partial.head $ M.toAscList m) + +-- | Extract the 'back' element of a Many, which guaranteed to be non-empty. +-- Analogous to 'Prelude.last' +back :: Many (x ': xs) -> Last (x ': xs) +back (Many _ m) = unsafeCoerce (snd . Partial.head $ M.toDescList m) + +-- | Extract the elements after the front of a Many, which guaranteed to be non-empty. +-- Analogous to 'Partial.tail' +aft :: Many (x ': xs) -> Many xs +aft (Many o m) = Many (o + 1) (M.delete (Key o) m) + +-- | Return all the elements of a Many except the 'back' one, which guaranteed to be non-empty. +-- Analogous to 'Prelude.init' +fore :: Many (x ': xs) -> Many (Init (x ': xs)) +fore (Many o m) = Many o (M.delete (Key (o + M.size m - 1)) m) + +-------------------------------------------------- + +-- | Getter by unique type. Get the field with type @x@. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- 'fetch' \@Int x \`shouldBe` 5 +-- @ +fetch :: forall x xs. UniqueMember x xs => Many xs -> x +fetch (Many o m) = unsafeCoerce (m M.! (Key (o + i))) + where i = fromInteger (natVal @(IndexOf x xs) Proxy) + +-- | infix version of 'fetch', with a extra proxy to carry the destination type. +-- +-- Mnemonic: Like 'Control.Lens.(^.)' but with an extra @.@ in front. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- x '.^.' (Proxy \@Int) \`shouldBe` 5 +-- @ +(.^.) :: forall x xs proxy. UniqueMember x xs => Many xs -> proxy x -> x +(.^.) v _ = fetch v +infixl 8 .^. -- like Control.Lens.(^.) + +-------------------------------------------------- + +-- | Getter by index. Get the value of the field at index type-level Nat @n@ +-- +-- @getchN (Proxy \@2) t@ +fetchN :: forall n x xs proxy. MemberAt n x xs => proxy n -> Many xs -> x +fetchN p (Many o m) = unsafeCoerce (m M.! (Key (o + i))) + where i = fromInteger (natVal p) + +-------------------------------------------------- + +-- | Setter by unique type. Set the field with type @x@. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- 'replace' \@Int x 6 \`shouldBe` (6 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- @ +replace :: forall x xs. UniqueMember x xs => Many xs -> x -> Many xs +replace (Many o m) v = Many o (M.insert (Key (o + i)) (unsafeCoerce v) m) + where i = fromInteger (natVal @(IndexOf x xs) Proxy) + +-- | infix version of 'replace' +-- +-- Mnemonic: Like a back to front 'Control.Lens.(.~)' with an extra @.@ in front. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- (x '.~.' (6 :: Int)) \`shouldBe` (6 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- @ +(.~.) :: forall x xs. UniqueMember x xs => Many xs -> x -> Many xs +(.~.) = replace +infixl 1 .~. -- like Control.Lens.(.~) + +-------------------------------------------------- + +-- | Setter by index. Set the value of the field at index type-level Nat @n@ +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- 'replaceN' \@0 Proxy x 7 `shouldBe` +-- @ +replaceN :: forall n x xs proxy. MemberAt n x xs => proxy n -> Many xs -> x -> Many xs +replaceN p (Many o m) v = Many o (M.insert (Key (o + i)) (unsafeCoerce v) m) + where i = fromInteger (natVal p) + +----------------------------------------------------------------------- + +-- | 'fetch' ('view' 'item') and 'replace' ('set' 'item') in 'Lens'' form. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- x '^.' 'item' \@Int \`shouldBe` 5 +-- (x '&' 'item' \@Int .~ 6) \`shouldBe` (6 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- @ +item :: forall x xs. UniqueMember x xs => Lens' (Many xs) x +item = lens fetch replace +{-# INLINE item #-} + +-- | 'fetchN' ('view' 'item') and 'replaceN' ('set' 'item') in 'Lens'' form. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' ./ nul +-- x '^.' 'itemN' (Proxy \@0) \`shouldBe` 5 +-- (x '&' 'itemN' (Proxy @0) '.~' 6) \`shouldBe` (6 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- @ +itemN :: forall n x xs proxy. MemberAt n x xs => proxy n -> Lens' (Many xs) x +itemN p = lens (fetchN p) (replaceN p) +{-# INLINE itemN #-} + +----------------------------------------------------------------------- + +-- | Internal function for construction - do not expose! +fromList' :: Ord k => [(k, WrappedAny)] -> M.Map k Any +fromList' xs = M.fromList (coerce xs) + +-- | Wraps a 'Case' into an instance of 'Emit', 'reiterate'ing and feeding 'Case' with the value from the 'Many' +-- and 'emit'ting the results. +-- +-- Internally, this holds the left-over [(k, v)] from the original 'Many' for the remaining typelist @xs@. +-- +-- That is the first v in the (k, v) is of type @x@, and the length of the list is equal to the length of @xs@. +newtype Via c (xs :: [Type]) r = Via (c xs r, [Any]) + +-- | Creates an 'Via' safely, so that the invariant of \"typelist to the value list type and size\" holds. +via :: c xs r -> Many xs -> Via c xs r +via c (Many _ m) = Via (c, snd <$> M.toAscList m) + +instance Reiterate c (x ': xs) => Reiterate (Via c) (x ': xs) where + -- use of tail here is safe as we are guaranteed the length from the typelist + reiterate (Via (c, xxs)) = Via (reiterate c, Partial.tail xxs) + +instance (Case c (x ': xs) r) => Emit (Via c) (x ': xs) r where + emit (Via (c, xxs)) = case' c (unsafeCoerce v) + where + -- use of front here is safe as we are guaranteed the length from the typelist + v = Partial.head xxs + +-- | Folds any 'Many', even with indistinct types. +-- Given __distinct__ handlers for the fields in 'Many', create a 'Collector' +-- of the results of running the handlers over the fields in 'Many'. +-- +-- The 'Collector' is 'AFoldable' to combine the results. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Char './' show \@(Maybe Char) './' show \@Bool './' 'nul' +-- 'afoldr' (:) [] ('forMany' ('Data.Diverse.Cases.cases' y) x) \`shouldBe` +-- [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +forMany :: c xs r -> Many xs -> Collector (Via c) xs r +forMany c x = Collector (via c x) + +-- | This is @flip 'forMany'@ +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Char './' show \@(Maybe Char) './' show \@Bool './' 'nul' +-- 'afoldr' (:) [] ('collect' x ('Data.Diverse.Cases.cases' y)) \`shouldBe` +-- [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +collect :: Many xs -> c xs r -> Collector (Via c) xs r +collect = flip forMany + +----------------------------------------------------------------------- + +-- | A variation of 'Via' which __'reiterateN'__ instead. +newtype ViaN c (n :: Nat) (xs :: [Type]) r = ViaN (c n xs r, [Any]) + +-- | Creates an 'ViaN' safely, so that the invariant of \"typelist to the value list type and size\" holds. +viaN :: c n xs r -> Many xs -> ViaN c n xs r +viaN c (Many _ m) = ViaN (c, snd <$> M.toAscList m) + +instance ReiterateN c n (x ': xs) => ReiterateN (ViaN c) n (x ': xs) where + -- use of tail here is safe as we are guaranteed the length from the typelist + reiterateN (ViaN (c, xxs)) = ViaN (reiterateN c, Partial.tail xxs) + +instance (Case (c n) (x ': xs) r) => Emit (ViaN c n) (x ': xs) r where + emit (ViaN (c, xxs)) = case' c (unsafeCoerce v) + where + -- use of front here is safe as we are guaranteed the length from the typelist + v = Partial.head xxs + +-- | Folds any 'Many', even with indistinct types. +-- Given __index__ handlers for the fields in 'Many', create a 'CollectorN' +-- of the results of running the handlers over the fields in 'Many'. +-- +-- The 'CollectorN' is 'AFoldable' to combine the results. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Bool './' show \@Char './' show \@(Maybe Char) './' show \@Int './' show \@(Maybe Char) './' 'nul' +-- 'afoldr' (:) [] ('forManyN' ('Data.Diverse.Cases.casesN' y) x) \`shouldBe` +-- [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +forManyN :: c n xs r -> Many xs -> CollectorN (ViaN c) n xs r +forManyN c x = CollectorN (viaN c x) + +-- | This is @flip 'forManyN'@ +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- y = show \@Int './' show \@Bool './' show \@Char './' show \@(Maybe Char) './' show \@Int './' show \@(Maybe Char) './' 'nul' +-- 'afoldr' (:) [] ('collectN' x ('Data.Diverse.Cases.casesN' y)) \`shouldBe` +-- [\"5", \"False", \"\'X'", \"Just \'O'", \"6", \"Just \'A'"] +-- @ +collectN :: Many xs -> c n xs r -> CollectorN (ViaN c) n xs r +collectN = flip forManyN + +----------------------------------------------------------------------- + +-- | A friendlier type constraint synomyn for 'narrow' +type Narrow (smaller :: [Type]) (larger :: [Type]) = + (AFoldable + ( Collector (Via (CaseNarrow smaller larger)) larger) [(Key, WrappedAny)]) + +-- | Construct a 'Many' with a smaller number of fields than the original. +-- Analogous to 'fetch' getter but for multiple fields. +-- +-- This can also be used to reorder fields in the original 'Many'. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- 'narrow' \@'[Bool, Char] x \`shouldBe` False './' \'X' './' 'nul' +-- @ +narrow :: forall smaller larger. Narrow smaller larger => Many larger -> Many smaller +narrow t = Many 0 (fromList' xs') + where + xs' = afoldr (++) [] (forMany (CaseNarrow @smaller @larger @larger) t) + +-- | infix version of 'narrow', with a extra proxy to carry the @smaller@ type. +-- +-- Mnemonic: Like 'Control.Lens.(^.)' but with an extra '\' (narrow to the right) in front. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- x '\^.' (Proxy @'[Bool, Char]) \`shouldBe` False './' \'X' './' 'nul' +-- @ +(\^.) :: forall smaller larger proxy. Narrow smaller larger => Many larger -> proxy smaller -> Many smaller +(\^.) t _ = narrow t +infixl 8 \^. -- like Control.Lens.(^.) + +-- | For each type x in @larger@, generate the (k, v) in @smaller@ (if it exists) +data CaseNarrow (smaller :: [Type]) (larger :: [Type]) (xs :: [Type]) r = CaseNarrow + +instance Reiterate (CaseNarrow smaller larger) (x ': xs) where + reiterate CaseNarrow = CaseNarrow + +-- | For each type x in larger, find the index in ys, and create an (incrementing key, value) +instance forall smaller larger x xs. (UniqueIfExists smaller x larger, MaybeUniqueMember x smaller) => + Case (CaseNarrow smaller larger) (x ': xs) [(Key, WrappedAny)] where + case' _ v = + case i of + 0 -> [] + i' -> [(Key (i' - 1), WrappedAny (unsafeCoerce v))] + where + i = fromInteger (natVal @(PositionOf x smaller) Proxy) + +----------------------------------------------------------------------- + +-- | A friendlier type constraint synomyn for 'narrowN' +type NarrowN (ns :: [Nat]) (smaller ::[Type]) (larger :: [Type]) = + ( AFoldable (CollectorN (ViaN (CaseNarrowN ns smaller)) 0 larger) [(Key, WrappedAny)] + , smaller ~ KindsAtIndices ns larger + , IsDistinct ns) + +-- | A variation of 'narrow' which uses a Nat list @n@ to specify how to reorder the fields, where +-- +-- @ +-- indices[branch_idx] = tree_idx@ +-- @ +-- +-- This variation allows @smaller@ or @larger@ to contain indistinct since +-- the mapping is specified by @indicies@. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- 'narrowN' (Proxy @'[5, 4, 0]) x \`shouldBe` Just \'A' './' (6 :: Int) './' (5 ::Int) './' 'nul' +-- @ +narrowN + :: forall ns smaller larger proxy. + NarrowN ns smaller larger + => proxy ns -> Many larger -> Many smaller +narrowN _ xs = Many 0 (fromList' xs') + where + xs' = afoldr (++) [] (forManyN (CaseNarrowN @ns @smaller @0 @larger) xs) + +data CaseNarrowN (indices :: [Nat]) (smaller :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseNarrowN + +instance ReiterateN (CaseNarrowN indices smaller) n (x ': xs) where + reiterateN CaseNarrowN = CaseNarrowN + +-- | For each type x in @larger@, find the index in ys, and create an (incrementing key, value) +instance forall indices smaller n x xs. MaybeMemberAt (PositionOf n indices) x smaller => + Case (CaseNarrowN indices smaller n) (x ': xs) [(Key, WrappedAny)] where + case' _ v = + case i of + 0 -> [] + i' -> [(Key (i' - 1), WrappedAny (unsafeCoerce v))] + where + i = fromInteger (natVal @(PositionOf n indices) Proxy) + +----------------------------------------------------------------------- + +-- | A friendlier type constraint synomyn for 'amend' +type Amend smaller larger = (AFoldable (Collector (Via (CaseAmend larger)) smaller) (Key, WrappedAny) + , IsDistinct smaller) + +-- | Sets the subset of 'Many' in the larger 'Many'. +-- Analogous to 'replace' setter but for multiple fields. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- 'amend' \@'[Int, Maybe Char] x ((6 :: Int) './' Just \'P' './' 'nul') \`shouldBe` +-- (6 :: Int) './' False './' \'X' './' Just \'P' './' 'nul' +-- @ +amend :: forall smaller larger. Amend smaller larger => Many larger -> Many smaller -> Many larger +amend (Many lo lm) t = Many lo (fromList' xs' `M.union` lm) + where + xs' = afoldr (:) [] (forMany (CaseAmend @larger @smaller lo) t) + +-- | infix version of 'amend'. Mnemonic: Like 'Control.Lens.(.~)' but with an extra '\' (narrow to the right) in front. +-- +-- Mnemonic: Like backwards 'Control.Lens.(^.)' but with an extra '\' (narrow to the right) in front. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- (x '\~.' (6 :: Int) './' Just \'P' './' 'nul') \`shouldBe` +-- (6 :: Int) './' False './' \'X' './' Just \'P' './' 'nul' +-- @ +(\~.) :: forall smaller larger. Amend smaller larger => Many larger -> Many smaller -> Many larger +(\~.) = amend +infixl 1 \~. -- like Control.Lens.(.~) + +newtype CaseAmend (larger :: [Type]) (xs :: [Type]) r = CaseAmend Int + +instance Reiterate (CaseAmend larger) (x ': xs) where + reiterate (CaseAmend lo) = CaseAmend lo + +-- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @Many larger@ +instance UniqueMember x larger => Case (CaseAmend larger) (x ': xs) (Key, WrappedAny) where + case' (CaseAmend lo) v = (Key (lo + i), WrappedAny (unsafeCoerce v)) + where + i = fromInteger (natVal @(IndexOf x larger) Proxy) + +----------------------------------------------------------------------- + +-- | A friendlier type constraint synomyn for 'amendN' +type AmendN ns smaller larger = + ( AFoldable (CollectorN (ViaN (CaseAmendN ns larger)) 0 smaller) (Key, WrappedAny) + , smaller ~ KindsAtIndices ns larger + , IsDistinct ns) + +-- | A variation of 'amend' which uses a Nat list @n@ to specify how to reorder the fields, where +-- +-- @ +-- indices[branch_idx] = tree_idx@ +-- @ +-- +-- This variation allows @smaller@ or @larger@ to contain indistinct since +-- the mapping is specified by @indicies@. +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- 'amendN' (Proxy \@'[5, 4, 0]) x (Just \'B' './' (8 :: Int) './' (4 ::Int) './' 'nul') \`shouldBe` +-- (4 :: Int) './' False './' \'X' './' Just \'O' './' (8 :: Int) './' Just \'B' './' 'nul' +-- @ +amendN :: forall ns smaller larger proxy. + (AmendN ns smaller larger) + => proxy ns -> Many larger -> Many smaller -> Many larger +amendN _ (Many lo lm) t = Many lo (fromList' xs' `M.union` lm) + where + xs' = afoldr (:) [] (forManyN (CaseAmendN @ns @larger @0 @smaller lo) t) + +newtype CaseAmendN (indices :: [Nat]) (larger :: [Type]) (n :: Nat) (xs :: [Type]) r = CaseAmendN Int + +instance ReiterateN (CaseAmendN indices larger) n (x ': xs) where + reiterateN (CaseAmendN lo) = CaseAmendN lo + +-- | for each x in @smaller@, convert it to a (k, v) to insert into the x in @larger@ +instance (MemberAt (KindAtIndex n indices) x larger) => + Case (CaseAmendN indices larger n) (x ': xs) (Key, WrappedAny) where + case' (CaseAmendN lo) v = (Key (lo + i), WrappedAny (unsafeCoerce v)) + where + i = fromInteger (natVal @(KindAtIndex n indices) Proxy) + +----------------------------------------------------------------------- + +-- | 'narrow' ('view' 'project') and 'amend' ('set' 'project') in 'Lens'' form. +-- +-- @ +-- 'project' = 'lens' 'narrow' 'amend' +-- @ +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul' +-- x '^.' ('project' \@'[Int, Maybe Char]) \`shouldBe` (5 :: Int) './' Just \'O' './' 'nul' +-- (x '&' ('project' \@'[Int, Maybe Char]) '.~' ((6 :: Int) './' Just 'P' './' 'nul')) \`shouldBe` +-- (6 :: Int) './' False './' \'X' './' Just \'P' './' 'nul' +-- @ +project + :: forall smaller larger. + (Narrow smaller larger, Amend smaller larger) + => Lens' (Many larger) (Many smaller) +project = lens narrow amend +{-# INLINE project #-} + +-- | 'narrowN' ('view' 'projectN') and 'amendN' ('set' 'projectN') in 'Lens'' form. +-- +-- @ +-- 'projectN' = 'lens' 'narrowN' 'amendN' +-- @ +-- +-- @ +-- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' (6 :: Int) './' Just \'A' './' 'nul' +-- x '^.' ('projectN' \@'[5, 4, 0] Proxy) \`shouldBe` Just \'A' './' (6 :: Int) './' (5 ::Int) './' 'nul' +-- (x '&' ('projectN' \@'[5, 4, 0] Proxy) '.~' (Just \'B' './' (8 :: Int) './' (4 ::Int) './' nul)) \`shouldBe` +-- (4 :: Int) './' False './' \'X' './' Just \'O' './' (8 :: Int) './' Just \'B' './' 'nul' +-- @ +projectN + :: forall ns smaller larger proxy. + (NarrowN ns smaller larger, AmendN ns smaller larger) + => proxy ns -> Lens' (Many larger) (Many smaller) +projectN p = lens (narrowN p) (amendN p) +{-# INLINE projectN #-} + +----------------------------------------------------------------------- + +-- | Stores the left & right Many and a list of Any which must be the same length and types in xs typelist. +newtype EmitEqMany (xs :: [Type]) r = EmitEqMany ([Any], [Any]) + +instance Reiterate EmitEqMany (x ': xs) where + -- use of tail here is safe as we are guaranteed the length from the typelist + reiterate (EmitEqMany (ls, rs)) = EmitEqMany (Partial.tail ls, Partial.tail rs) + +instance Eq x => Emit EmitEqMany (x ': xs) Bool where + emit (EmitEqMany (ls, rs)) = l == r + where + -- use of front here is safe as we are guaranteed the length from the typelist + l = unsafeCoerce (Partial.head ls) :: x + r = unsafeCoerce (Partial.head rs) :: x + +eqMany + :: forall xs. + AFoldable (Collector EmitEqMany xs) Bool + => Many xs -> Many xs -> [Bool] +eqMany (Many _ lm) (Many _ rm) = afoldr (:) [] + (Collector (EmitEqMany @xs (snd <$> M.toAscList lm, snd <$> M.toAscList rm))) + +-- | Two 'Many's are equal if all their fields equal +instance AFoldable (Collector EmitEqMany xs) Bool => Eq (Many xs) where + lt == rt = foldr (\e z -> bool False z e) True eqs + where + eqs = eqMany lt rt + +----------------------------------------------------------------------- + +-- | Stores the left & right Many and a list of Any which must be the same length and types in xs typelist. +newtype EmitOrdMany (xs :: [Type]) r = EmitOrdMany ([Any], [Any]) + +instance Reiterate EmitOrdMany (x ': xs) where + -- use of tail here is safe as we are guaranteed the length from the typelist + reiterate (EmitOrdMany (ls, rs)) = EmitOrdMany (Partial.tail ls, Partial.tail rs) + +instance Ord x => Emit EmitOrdMany (x ': xs) Ordering where + emit (EmitOrdMany (ls, rs)) = compare l r + where + -- use of front here is safe as we are guaranteed the length from the typelist + l = unsafeCoerce (Partial.head ls) :: x + r = unsafeCoerce (Partial.head rs) :: x + +ordMany + :: forall xs. + AFoldable (Collector EmitOrdMany xs) Ordering + => Many xs -> Many xs -> [Ordering] +ordMany (Many _ lm) (Many _ rm) = afoldr (:) [] + (Collector (EmitOrdMany @xs (snd <$> M.toAscList lm, snd <$> M.toAscList rm))) + +-- | Two 'Many's are ordered by 'compare'ing their fields in index order +instance (Eq (Many xs), AFoldable (Collector EmitOrdMany xs) Ordering) => Ord (Many xs) where + compare lt rt = foldr (\o z -> case o of + EQ -> z + o' -> o') EQ ords + where + ords = ordMany lt rt + +----------------------------------------------------------------------- + +-- | Internally uses [Any] like Via, except also handle the empty type list. +newtype EmitShowMany (xs :: [Type]) r = EmitShowMany [Any] + +instance Reiterate EmitShowMany (x ': xs) where + -- use of tail here is safe as we are guaranteed the length from the typelist + reiterate (EmitShowMany xxs) = EmitShowMany (Partial.tail xxs) + +instance Emit EmitShowMany '[] ShowS where + emit _ = showString "nul" + + +instance Show x => Emit EmitShowMany (x ': xs) ShowS where + emit (EmitShowMany xxs) = showsPrec (cons_prec + 1) v . showString " ./ " + where + -- use of front here is safe as we are guaranteed the length from the typelist + v = unsafeCoerce (Partial.head xxs) :: x + cons_prec = 5 -- infixr 5 cons + +showMany + :: forall xs. + AFoldable (Collector0 EmitShowMany xs) ShowS + => Many xs -> ShowS +showMany (Many _ m) = afoldr (.) id (Collector0 (EmitShowMany @xs (snd <$> M.toAscList m))) + +-- | @read "5 ./ False ./ 'X' ./ Just 'O' ./ nul" == (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul'@ +instance AFoldable (Collector0 EmitShowMany xs) ShowS => Show (Many xs) where + showsPrec d t = showParen (d > cons_prec) $ showMany t + where + cons_prec = 5 -- infixr 5 cons + +----------------------------------------------------------------------- + +newtype EmitReadMany (xs :: [Type]) r = EmitReadMany Key + +instance Reiterate EmitReadMany (x ': xs) where + reiterate (EmitReadMany (Key i)) = EmitReadMany (Key (i + 1)) + +instance Emit EmitReadMany '[] (ReadPrec [(Key, WrappedAny)]) where + emit (EmitReadMany _) = do + lift $ L.expect (Ident "nul") + pure [] + +instance Read x => Emit EmitReadMany (x ': xs) (ReadPrec [(Key, WrappedAny)]) where + emit (EmitReadMany i) = do + a <- readPrec @x + lift $ L.expect (Symbol "./") + pure [(i, WrappedAny (unsafeCoerce a))] + +readMany + :: forall xs. + AFoldable (Collector0 EmitReadMany xs) (ReadPrec [(Key, WrappedAny)]) + => Proxy (xs :: [Type]) -> ReadPrec [(Key, WrappedAny)] +readMany _ = afoldr (liftA2 (++)) (pure []) (Collector0 (EmitReadMany @xs (Key 0))) + +-- | @read "5 ./ False ./ 'X' ./ Just 'O' ./ nul" == (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nul'@ +instance (AFoldable (Collector0 EmitReadMany xs) (ReadPrec [(Key, WrappedAny)])) => + Read (Many xs) where + readPrec = + parens $ + prec 10 $ do + xs <- readMany @xs Proxy + pure (Many 0 (fromList' xs)) + +-- | 'WrappedAny' avoids the following: +-- Illegal type synonym family application in instance: Any +newtype WrappedAny = WrappedAny Any diff --git a/src/Data/Diverse/PackageId.hs b/src/Data/Diverse/PackageId.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/PackageId.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE DataKinds #-} + +module Data.Diverse.PackageId where + +-- | This is used for the Generic D1 metadata. +-- NB. package id is obtained by running `stack exec ghc-pkg describe data-diverse` +type PackageId = "data-diverse-0.1.0.0-15JNBdcTY3F9aOKAG5iNge" diff --git a/src/Data/Diverse/Reduce.hs b/src/Data/Diverse/Reduce.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Reduce.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Data.Diverse.Reduce where + +import Data.Kind + +-- | Reduce a polymorphic variant @v xs@ into @r@ using handlers. +-- This class is required in order to step through all the different types in a variant. +class Reduce v handler (xs :: [Type]) r where + reduce :: handler xs r -> v xs -> r diff --git a/src/Data/Diverse/Reiterate.hs b/src/Data/Diverse/Reiterate.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Reiterate.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Diverse.Reiterate where + +import Data.Diverse.Type +import Data.Kind +import GHC.TypeLits + +-- | Allows iterating over the types in a typelist +class Reiterate c (xs :: [Type]) where + -- | Return the next iteration without the 'Head' type x in (x ': xs) + reiterate :: c xs r -> c (Tail xs) r + +-- | Allows iterating over the types in a typelist, whilst also incrementing an Nat index +class ReiterateN c (n :: Nat) (xs :: [Type]) where + -- | Return the next iteration without the 'Head' type x in (x ': xs) + reiterateN :: c n xs r -> c (n + 1) (Tail xs) r diff --git a/src/Data/Diverse/Type.hs b/src/Data/Diverse/Type.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Type.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE TypeInType #-} + +module Data.Diverse.Type where + +import Data.Diverse.Type.Internal +import Data.Kind +import GHC.TypeLits + +-- | Ensures that @x@ is a unique member of @xs@, and that 'natVal' can be used. +type UniqueMember x xs = (Unique x xs, KnownNat (IndexOf x xs)) + +-- | Ensures that @x@ is a unique member of @xs@ if it exists, and that 'natVal' can be used. +type MaybeUniqueMember x xs = (Unique x xs, KnownNat (PositionOf x xs)) + +-- | Ensures that @x@ is a member of @xs@ at @n@, and that 'natVal' can be used. +type MemberAt n x xs = (KnownNat n, x ~ KindAtIndex n xs) + +-- | Ensures that @x@ is a member of @xs@ at @n@ if it exists, and that 'natVal' can be used. +type MaybeMemberAt n x xs = (KnownNat n, KindAtPositionIs n x xs) + +-- | Ensures x is a unique member in @xs@ iff it exists in @ys@ +type family UniqueIfExists ys x xs :: Constraint where + UniqueIfExists '[] x xs = () + UniqueIfExists (y ': ys) y xs = Unique y xs + UniqueIfExists (y ': ys) x xs = UniqueIfExists ys x xs + +-- | Ensures that the type list contain unique types +type IsDistinct (xs :: [k]) = IsDistinctImpl xs xs + +-- | Return the list of distinct types in a typelist +type family Distinct (xs :: [k]) :: [k] where + Distinct '[] = '[] + Distinct (x ': xs) = DistinctImpl xs x xs + +-- | Ensures that @x@ only ever appears once in @xs@ +type Unique (x :: k) (xs :: [k]) = UniqueImpl xs x xs + +-- | Get the first index of a type (Indexed by 0) +-- Will result in type error if x doesn't exist in xs. +type IndexOf (x :: k) (xs :: [k]) = IndexOfImpl xs x xs + +-- | Get the first index of a type (Indexed by 1) +-- Will return 0 if x doesn't exists in xs. +type PositionOf (x :: k) (xs :: [k]) = PositionOfImpl 0 x xs + +-- | Get the type at an index +type KindAtIndex (n :: Nat) (xs :: [k]) = KindAtIndexImpl n xs n xs + +-- | It's actually ok for the position to be zero, but if it's not zero then the types must match +type family KindAtPositionIs (n :: Nat) (x :: k) (xs :: [k]) :: Constraint where + KindAtPositionIs 0 x xs = () + KindAtPositionIs n x xs = (x ~ KindAtIndexImpl (n - 1) xs (n - 1) xs) + +-- | Get the types at an list of index +type family KindsAtIndices (ns :: [Nat]) (xs :: [k]) :: [k] where + KindsAtIndices '[] xs = '[] + KindsAtIndices (n ': ns) xs = KindAtIndex n xs ': KindsAtIndices ns xs + +-- | The typelist @xs@ without @x@. It is okay for @x@ not to exist in @xs@ +type family Without (x :: k) (xs :: [k]) :: [k] where + Without x '[] = '[] + Without x (x ': xs) = Without x xs + Without x (y ': xs) = y ': Without x xs + +-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@ +type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs + +-- | Gets the ength of a typelist +type family Length (xs :: [k]) :: Nat where + Length '[] = 0 + Length (x ': xs) = 1 + Length xs + +-- | Get the typelist without the 'Head' type +type family Tail (xs :: [k]) :: [k] where + Tail '[] = TypeError ('Text "Cannot Tail an empty type list") + Tail (x ': xs) = xs + +-- | Get the first type in a typelist +type family Head (xs :: [k]) :: k where + Head '[] = TypeError ('Text "Cannot Head an empty type list") + Head (x ': xs) = x + +-- | Get the last type in a typelist +type family Last (xs :: [k]) :: k where + Last '[] = TypeError ('Text "Cannot Last an empty type list") + Last (x ': x' ': xs) = Last (x' ': xs) + Last '[x] = x + +-- | Ensures two typelists are the same length +type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys + +-- | Set complement. Returns the set of things in @xs@ that are not in @ys@. +type family Complement (xs :: [k]) (ys :: [k]) :: [k] where + Complement xs '[] = xs + Complement xs (y ': ys) = Complement (Without y xs) ys + +-- | Returns a @xs@ appended with @ys@ +type family Append (xs :: [k]) (ys :: [k]) :: [k] where + Append '[] ys = ys + Append (x ': xs) ys = x ': Append xs ys + +-- | Returns the typelist without the 'Last' type +type family Init (xs :: [k]) :: [k] where + Init '[] = TypeError ('Text "Cannot Init an empty type list") + Init '[x] = '[] + Init (x ': xs) = x ': Init xs diff --git a/src/Data/Diverse/Type/Internal.hs b/src/Data/Diverse/Type/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Type/Internal.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Diverse.Type.Internal where + +import Data.Kind +import GHC.TypeLits + +-- | Get the first position of a type (indexed by 1) +-- Will return 0 if @x@ doesn't exists in @xs@. +type family PositionOfImpl (i :: Nat) (x :: k) (xs :: [k]) :: Nat where + PositionOfImpl i x (x ': xs) = i + 1 + PositionOfImpl i y (x ': xs) = PositionOfImpl (i + 1) y xs + PositionOfImpl i x '[] = 0 + +-- | Get the first index of a type from a list +type family IndexOfImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Nat where + IndexOfImpl ctx x (x ': xs) = 0 + IndexOfImpl ctx y (x ': xs) = 1 + IndexOfImpl ctx y xs + IndexOfImpl ctx y '[] = TypeError ('Text "‘" + ':<>: 'ShowType y + ':<>: 'Text "’" + ':<>: 'Text " is not a member of " + ':<>: 'Text "‘" + ':<>: 'ShowType ctx + ':<>: 'Text "’") + +-- | Searches for y in ys +-- if not found, than use y, and repeat search with next (y ': ys) in ctx +-- else if found, then don't use y, then repeat search with next (y ': ys) in ctx +type family DistinctImpl (ctx :: [k]) (y :: k) (ys :: [k]) :: [k] where + DistinctImpl '[] y '[] = y ': '[] + DistinctImpl '[] y (y ': xs) = '[] + DistinctImpl (x ': xs) y '[] = y ': DistinctImpl xs x xs + DistinctImpl (x ': xs) y (y ': ys) = DistinctImpl xs x xs + DistinctImpl ctx y (x ': xs) = DistinctImpl ctx y xs + +-- | Errors if a type exists in a typelist +type family MissingImpl (ctx :: [k]) (y :: k) (xs :: [k]) :: Constraint where + MissingImpl ctx y '[] = () + MissingImpl ctx x (x ': xs) = TypeError ('Text "‘" + ':<>: 'ShowType x + ':<>: 'Text "’" + ':<>: 'Text " is a duplicate in " + ':<>: 'Text "‘" + ':<>: 'ShowType ctx + ':<>: 'Text "’") + MissingImpl ctx y (x ': xs) = (MissingImpl ctx y xs) + +-- | Ensures that the type list contain unique types +type family IsDistinctImpl (ctx :: [k]) (xs :: [k]) :: Constraint where + IsDistinctImpl ctx '[] = () + IsDistinctImpl ctx (x ': xs) = (MissingImpl ctx x xs, IsDistinctImpl ctx xs) + +-- | Ensures that @x@ only ever appears once in @xs@ +type family UniqueImpl (ctx :: [k]) (x :: k) (xs :: [k]) :: Constraint where + UniqueImpl ctx x '[] = () + UniqueImpl ctx x (x ': xs) = MissingImpl ctx x xs + UniqueImpl ctx x (y ': xs) = UniqueImpl ctx x xs + +-- | Indexed access into the list +type family KindAtIndexImpl (orig :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: k where + KindAtIndexImpl i ctx 0 '[] = TypeError ('Text "Index ‘" + ':<>: 'ShowType i + ':<>: 'Text "’" + ':<>: 'Text " is out of bounds of " + ':<>: 'Text "‘" + ':<>: 'ShowType ctx + ':<>: 'Text "’") + KindAtIndexImpl i ctx 0 (x ': xs) = x + KindAtIndexImpl i ctx n (x ': xs) = KindAtIndexImpl i ctx (n - 1) xs + +-- | Ensures two typelists are the same length +type family SameLengthImpl (ctx :: [k1]) (cty :: [k2]) (xs :: [k1]) (yx :: [k2]) :: Constraint where + SameLengthImpl as bs '[] '[] = () + SameLengthImpl as bs (x ': xs) (y ': ys) = SameLengthImpl as bs xs ys + SameLengthImpl as bs xs ys = TypeError ('Text "‘" + ':<>: 'ShowType as + ':<>: 'Text "’" + ':<>: 'Text " is not the same length as " + ':<>: 'Text "‘" + ':<>: 'ShowType bs + ':<>: 'Text "’") + +-- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@ +type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where + WithoutIndexImpl i ctx n '[] = TypeError ('Text "Index ‘" + ':<>: 'ShowType i + ':<>: 'Text "’" + ':<>: 'Text " is out of bounds of " + ':<>: 'Text "‘" + ':<>: 'ShowType ctx + ':<>: 'Text "’") + WithoutIndexImpl i ctx 0 (x ': xs) = xs + WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs diff --git a/src/Data/Diverse/Which.hs b/src/Data/Diverse/Which.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Which.hs @@ -0,0 +1,47 @@ +-- | Re-export Which without the constructor +module Data.Diverse.Which ( + -- * 'Which' type + Which -- hiding constructor + + -- * Single type + -- ** Construction + , impossible + , pick + , pick0 + , pickOnly + , pickN + -- ** Destruction + , obvious + , trial + , trial0 + , trialN + -- ** Lens + , facet + , facetN + + -- * Multiple types + -- ** Injection + , Diversify + , diversify + , diversify0 + , DiversifyN + , diversifyN + -- ** Inverse Injection + , Reinterpret + , reinterpret + , ReinterpretN + , reinterpretN + -- ** Lens + , inject + , injectN + + -- * Catamorphism + , Switch(..) + , which + , switch + , SwitchN(..) + , whichN + , switchN + ) where + +import Data.Diverse.Which.Internal diff --git a/src/Data/Diverse/Which/Internal.hs b/src/Data/Diverse/Which/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Diverse/Which/Internal.hs @@ -0,0 +1,666 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Diverse.Which.Internal ( + -- * 'Which' type + Which(..) -- exporting constructor unsafely! + + -- * Single type + -- ** Construction + , impossible + , pick + , pick0 + , pickOnly + , pickN + -- ** Destruction + , obvious + , trial + , trial0 + , trialN + -- ** Lens + , facet + , facetN + + -- * Multiple types + -- ** Injection + , Diversify + , diversify + , diversify0 + , DiversifyN + , diversifyN + -- ** Inverse Injection + , Reinterpret + , reinterpret + , ReinterpretN + , reinterpretN + -- ** Lens + , inject + , injectN + + -- * Catamorphism + , Switch(..) + , which + , switch + , SwitchN(..) + , whichN + , switchN + ) where + +import Control.Applicative +import Control.Lens +import Data.Diverse.AFoldable +import Data.Diverse.Case +import Data.Diverse.Collector +import Data.Diverse.Emit +import Data.Diverse.PackageId +import Data.Diverse.Reduce +import Data.Diverse.Reiterate +import Data.Diverse.Type +import Data.Kind +import Data.Proxy +import qualified GHC.Generics as G +import GHC.Prim (Any) +import GHC.TypeLits +import Text.ParserCombinators.ReadPrec +import Text.Read +import qualified Text.Read.Lex as L +import Unsafe.Coerce + +-- | A 'Which' is an anonymous sum type (also known as a polymorphic variant, or co-record) +-- which can only contain one of the types in the typelist. +-- This is essentially a typed version of 'Data.Dynamic'. +-- +-- The following functions are available can be used to manipulate unique types in the typelist +-- +-- * constructor: 'pick' +-- * destructor: 'trial' +-- * injection: 'diversify' and 'reinterpret' +-- * catamorphism: 'which' or 'switch' +-- +-- These functions are type specified. This means labels are not required because the types themselves can be used to access the 'Which'. +-- It is a compile error to use those functions for duplicate fields. +-- +-- For duplicate types in the list of possible types, Nat-indexed version of the functions are available: +-- +-- * constructor: 'pickN' +-- * destructor: 'trialN' +-- * inejction: 'diversifyN' and 'reinterpretN' +-- * catamorphism: 'whichN' or 'switchN' +-- +-- Encoding: The variant contains a value whose type is at the given position in the type list. +-- This is the same encoding as and . +-- +-- The constructor is only exported in the "Data.Diverse.Which.Internal" module +data Which (xs :: [Type]) = Which {-# UNPACK #-} !Int Any + +-- Just like Haskus and HList versions, inferred type is phantom which is wrong +type role Which representational + +---------------------------------------------- + +-- | A terminating 'G.Generic' instance for no types encoded as a 'impossible'. +-- The 'G.C1' and 'G.S1' metadata are not encoded. +instance G.Generic (Which '[]) where + type Rep (Which '[]) = G.D1 ('G.MetaData + "Which" + "Data.Diverse.Which.Internal" + PackageId + 'False) G.U1 + from _ = {- G.D1 -} G.M1 {- G.U1 -} G.U1 + to (G.M1 G.U1) = impossible + +-- | A terminating 'G.Generic' instance for one type encoded with 'pick''. +-- The 'G.C1' and 'G.S1' metadata are not encoded. +instance G.Generic (Which '[x]) where + type Rep (Which '[x]) = G.D1 ('G.MetaData + "Which" + "Data.Diverse.Which.Internal" + PackageId + 'False) (G.Rec0 x) + from v = {- G.D1 -} G.M1 ({- G.Rec0 -} G.K1 (obvious v)) + to ({- G.D1 -} G.M1 ({- G.Rec0 -} G.K1 a)) = pickOnly a + +-- | A 'G.Generic' instance encoded as either the 'x' value ('G.:+:') or the 'diversify0'ed remaining 'Which xs'. +-- The 'G.C1' and 'G.S1' metadata are not encoded. +instance G.Generic (Which (x ': x' ': xs)) where + type Rep (Which (x ': x' ': xs)) = G.D1 ('G.MetaData + "Which" + "Data.Diverse.Which.Internal" + PackageId + 'False) ((G.Rec0 x) G.:+: (G.Rec0 (Which (x' ': xs)))) + from v = {- G.D1 -} G.M1 $ + case trial0 v of + Right x -> G.L1 ({- G.Rec0 -} G.K1 x) + Left v' -> G.R1 ({- G.Rec0 -} G.K1 v') + to ({- G.D1 -} G.M1 ({- G.Rec0 -} x)) = case x of + G.L1 ({- G.Rec0 -} G.K1 a) -> pick0 a + G.R1 ({- G.Rec0 -} G.K1 v) -> diversify0 Proxy v + +----------------------------------------------------------------------- + +-- | A 'Which' with no alternatives. You can't do anything with 'impossible' +-- except Eq, Read, and Show it. +-- Using functions like 'switch' and 'trial' with 'impossible' is a compile error. +-- 'impossible' is only useful as a 'Left'-over from 'trial'ing a @Which '[x]@ with one type. +impossible :: Which '[] +impossible = Which (-1) (unsafeCoerce ()) + +-- | Lift a value into a 'Which' of possibly other types @xs@. +-- @xs@ can be inferred or specified with TypeApplications. +-- NB. forall is used to specify @xs@ first, so TypeApplications can be used to specify @xs@ first +-- +-- @ +-- 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: Which '[Int, Bool, Char, Maybe String] +-- @ +pick :: forall xs x. UniqueMember x xs => x -> Which xs +pick = Which (fromInteger (natVal @(IndexOf x xs) Proxy)) . unsafeCoerce + +-- | A variation of 'pick' into a 'Which' of a single type. +-- +-- @ +-- 'pickOnly' \'A' :: Which '[Char] +-- @ +pickOnly :: x -> Which '[x] +pickOnly = pick0 + +-- | A variation of 'pick' into a 'Which' where @x@ is the first type. +-- +-- @ +-- 'pick0' \'A' :: Which '[Char, Int, Bool] +-- @ +pick0 :: x -> Which (x ': xs) +pick0 = Which 0 . unsafeCoerce + +-- | Lift a value into a 'Which' of possibly other (possibley indistinct) types, where the value is the @n@-th type. +-- +-- @ +-- 'pickN' (Proxy \@4) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] +-- @ +pickN :: forall n xs x proxy. MemberAt n x xs => proxy n -> x -> Which xs +pickN _ = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce + +-- | It is 'obvious' what value is inside a 'Which' of one type. +-- +-- @ +-- let x = 'pick'' \'A' :: Which '[Char] +-- 'obvious' x \`shouldBe` \'A' +-- @ +obvious :: Which '[a] -> a +obvious (Which _ v) = unsafeCoerce v + +-- | 'trial' a type in a 'Which' and 'Either' get the 'Right' value or the 'Left'-over possibilities. +-- +-- @ +-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] +-- 'trial' \@Char x \`shouldBe` Right \'A' +-- 'trial' \@Int x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String] +-- @ +trial + :: forall x xs. + (UniqueMember x xs) + => Which xs -> Either (Which (Without x xs)) x +trial (Which n v) = let i = fromInteger (natVal @(IndexOf x xs) Proxy) + in if n == i + then Right (unsafeCoerce v) + else if n > i + then Left (Which (n - 1) v) + else Left (Which n v) + +-- | A variation of a 'Which' 'trial' which 'trial's the first type in the type list. +-- +-- @ +-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] +-- 'trial0' x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Bool, Char, Maybe String] +-- @ +trial0 :: Which (x ': xs) -> Either (Which xs) x +trial0 (Which n v) = if n == 0 + then Right (unsafeCoerce v) + else Left (Which (n - 1) v) + + +-- | 'trialN' the n-th type of a 'Which', and get 'Either' the 'Right' value or the 'Left'-over possibilities. +-- +-- @ +-- let x = 'pick' \'A' \@'[Int, Bool, Char, Maybe String] :: 'Which' '[Int, Bool, Char, Maybe String] +-- 'trialN' @1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String] +-- @ +trialN + :: forall n xs x proxy. + (MemberAt n x xs) + => proxy n -> Which xs -> Either (Which (WithoutIndex n xs)) x +trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy) + in if n == i + then Right (unsafeCoerce v) + else if n > i + then Left (Which (n - 1) v) + else Left (Which n v) + +-- | Utility to convert Either to Maybe +hush :: Either a b -> Maybe b +hush = either (const Nothing) Just + +----------------------------------------------------------------- + +-- | 'pick' ('review' 'facet') and 'trial' ('preview' 'facet') in 'Prism'' form. +-- +-- @ +-- 'facet' = 'prism'' 'pick' (either (const Nothing) Just . 'trial') +-- @ +-- +-- @ +-- let y = 'review' ('facet' \@Int) (5 :: Int) :: 'Which' '[Bool, Int, Char, Bool, Char] -- 'pick' +-- x = 'preview' ('facet' \@Int) y -- 'trial' +-- x \`shouldBe` (Just 5) +-- @ +facet :: forall x xs. (UniqueMember x xs) => Prism' (Which xs) x +facet = prism' pick (hush . trial) +{-# INLINE facet #-} + +-- | 'pickN' ('review' 'facetN') and 'trialN' ('preview' 'facetN') in 'Prism'' form. +-- +-- @ +-- 'facetN' p = 'prism'' ('pickN' p) (either (const Nothing) Just . 'trialN' p) +-- @ +-- +-- @ +-- let y = 'review' ('facetN' (Proxy \@4)) (5 :: Int) :: 'Which' '[Bool, Int, Char, Bool, Int, Char] -- 'pickN' +-- x = 'preview' ('facetN' (Proxy \@4)) y -- 'trialN' +-- x \`shouldBe` (Just 5) +-- @ +facetN :: forall n xs x proxy. (MemberAt n x xs) => proxy n -> Prism' (Which xs) x +facetN p = prism' (pickN p) (hush . trialN p) +{-# INLINE facetN #-} + +------------------------------------------------------------------ + +-- | A friendlier constraint synonym for 'diversify'. +type Diversify (tree :: [Type]) (branch :: [Type]) = Reduce Which (Switch (CaseDiversify tree branch)) branch (Which tree) + +-- | Convert a 'Which' to another 'Which' that may include other possibilities. +-- That is, @branch@ is equal or is a subset of @tree@. +-- +-- This can also be used to rearrange the order of the types in the 'Which'. +-- +-- It is a compile error if @tree@ has duplicate types with @branch@. +-- +-- NB. forall is used to @tree@ is ordered first, so TypeApplications can be used to specify @tree@ first. +-- +-- @ +-- let a = 'pick'' (5 :: Int) :: 'Which' '[Int] +-- b = 'diversify' \@[Int, Bool] a :: 'Which' '[Int, Bool] +-- c = 'diversify' \@[Bool, Int] b :: 'Which' '[Bool, Int] +-- @ +diversify :: forall tree branch. Diversify tree branch => Which branch -> Which tree +diversify = which (CaseDiversify @tree @branch @branch) + +data CaseDiversify (tree :: [Type]) (branch :: [Type]) (branch' :: [Type]) r = CaseDiversify + +instance Reiterate (CaseDiversify tree branch) branch' where + reiterate CaseDiversify = CaseDiversify + +-- | The @Unique x branch@ is important to get a compile error if the from @branch@ doesn't have a unique x +instance (UniqueMember x tree, Unique x branch) => + Case (CaseDiversify tree branch) (x ': branch') (Which tree) where + case' CaseDiversify = pick + +-- | A simple version of 'diversify' which add another type to the front of the typelist. +diversify0 :: proxy x -> Which xs -> Which (x ': xs) +diversify0 _ (Which n v) = Which (n + 1) v + +------------------------------------------------------------------ + +-- | A friendlier constraint synonym for 'diversifyN'. +type DiversifyN (indices :: [Nat]) (tree :: [Type]) (branch :: [Type]) = (Reduce Which (SwitchN (CaseDiversifyN indices) 0) (KindsAtIndices indices tree) (Which tree), KindsAtIndices indices tree ~ branch) + +-- | A variation of 'diversify' which uses a Nat list @n@ to specify how to reorder the fields, where +-- +-- @ +-- indices[branch_idx] = tree_idx@ +-- @ +-- +-- This variation allows @tree@ to contain duplicate types with @branch@ since +-- the mapping is specified by @indicies@. +-- +-- @ +-- let a = 'pick'' (5 :: Int) :: 'Which' '[Int] +-- b = 'diversify' \@[Int, Bool] a :: 'Which' '[Int, Bool] +-- c = 'diversify' \@[Bool, Int] b :: 'Which' '[Bool, Int] +-- @ +diversifyN :: forall indices tree branch proxy. (DiversifyN indices tree branch) => proxy indices -> Which branch -> Which tree +diversifyN _ = whichN (CaseDiversifyN @indices @0 @branch) + +data CaseDiversifyN (indices :: [Nat]) (n :: Nat) (branch' :: [Type]) r = CaseDiversifyN + +instance ReiterateN (CaseDiversifyN indices) n branch' where + reiterateN CaseDiversifyN = CaseDiversifyN + +instance MemberAt (KindAtIndex n indices) x tree => + Case (CaseDiversifyN indices n) (x ': branch') (Which tree) where + case' CaseDiversifyN v = pickN (Proxy @(KindAtIndex n indices)) v + +------------------------------------------------------------------ + +-- | A friendlier constraint synonym for 'reinterpret'. +type Reinterpret branch tree = Reduce Which (Switch (CaseReinterpret branch tree)) tree (Either (Which (Complement tree branch)) (Which branch)) + +-- | Convert a 'Which' into possibly another 'Which' with a totally different typelist. +-- Returns either a 'Which' with the 'Right' value, or a 'Which' with the 'Left'over @compliment@ types. +-- +-- It is a compile error if @branch@ or @compliment@ has duplicate types with @tree@. +-- +-- NB. forall used to specify @branch@ first, so TypeApplications can be used to specify @branch@ first. +-- +-- @ +-- let a = 'pick' \@[Int, Char, Bool] (5 :: Int) :: 'Which' '[Int, Char, Bool] +-- let b = 'reinterpret' @[String, Char] y +-- b \`shouldBe` Left ('pick' (5 :: Int)) :: 'Which' '[Int, Bool] +-- let c = 'reinterpret' @[String, Int] a +-- c \`shouldBe` Right ('pick' (5 :: Int)) :: 'Which' '[String, Int] +-- @ +reinterpret :: forall branch tree. Reinterpret branch tree => Which tree -> Either (Which (Complement tree branch)) (Which branch) +reinterpret = which (CaseReinterpret @branch @tree @tree) + +data CaseReinterpret (branch :: [Type]) (tree :: [Type]) (tree' :: [Type]) r = CaseReinterpret + +instance Reiterate (CaseReinterpret branch tree) tree' where + reiterate CaseReinterpret = CaseReinterpret + +instance ( MaybeUniqueMember x branch + , comp ~ Complement tree branch + , MaybeUniqueMember x comp + , Unique x tree -- Compile error to ensure reinterpret only works with unique fields + ) => + Case (CaseReinterpret branch tree) (x ': tree') (Either (Which comp) (Which branch)) where + case' CaseReinterpret a = + case fromInteger (natVal @(PositionOf x branch) Proxy) of + 0 -> let j = fromInteger (natVal @(PositionOf x (Complement tree branch)) Proxy) + -- safe use of partial! j will never be zero due to check above + in Left $ Which (j - 1) (unsafeCoerce a) + i -> Right $ Which (i - 1) (unsafeCoerce a) + +------------------------------------------------------------------ + +-- | A friendlier constraint synonym for 'reinterpretN'. +type ReinterpretN (indices :: [Nat]) (branch :: [Type]) (tree :: [Type]) = (Reduce Which (SwitchN (CaseReinterpretN indices) 0) tree (Maybe (Which (KindsAtIndices indices tree))), KindsAtIndices indices tree ~ branch) + +-- | A limited variation of 'reinterpret' which uses a Nat list @n@ to specify how to reorder the fields, where +-- +-- @ +-- indices[branch_idx] = tree_idx@ +-- @ +-- +-- This variation allows @tree@ to contain duplicate types with @branch@ +-- since the mapping is specified by @indicies@. +-- +-- However, unlike 'reinterpert', in this variation, +-- @branch@ must be a subset of @tree@ instead of any arbitrary Which. +-- Also it returns a Maybe instead of Either. +-- +-- This is so that the same @indices@ can be used in 'narrowN'. +reinterpretN :: forall (indices :: [Nat]) branch tree proxy. (ReinterpretN indices branch tree) => proxy indices -> Which tree -> Maybe (Which branch) +reinterpretN _ = whichN (CaseReinterpretN @indices @0 @tree) + +data CaseReinterpretN (indices :: [Nat]) (n :: Nat) (tree' :: [Type]) r = CaseReinterpretN + +instance ReiterateN (CaseReinterpretN indices) n tree' where + reiterateN CaseReinterpretN = CaseReinterpretN + +instance MaybeMemberAt (PositionOf n indices) x branch => Case (CaseReinterpretN indices n) (x ': tree) (Maybe (Which branch)) where + case' CaseReinterpretN a = + case fromInteger (natVal @(PositionOf n indices) Proxy) of + 0 -> Nothing + i -> Just $ Which (i - 1) (unsafeCoerce a) + +-- ------------------------------------------------------------------ + +-- | 'diversify' ('review' 'inject') and 'reinterpret' ('preview' 'inject') in 'Prism'' form. +-- +-- @ +-- let x = 'pick' (5 :: Int) :: 'Which' '[String, Int] +-- y = 'review' ('inject' \@_ \@[Bool, Int, Char, String]) x -- 'diversify' +-- y \`shouldBe` pick (5 :: Int) :: 'Which' '[Bool, Int, Char, String] +-- let y' = 'preview' ('inject' \@[String, Int]) y -- 'reinterpret' +-- y' \`shouldBe` Just (pick (5 :: Int)) :: Maybe ('Which' '[String, Int]) +inject + :: forall branch tree. + ( Diversify tree branch + , Reinterpret branch tree + ) + => Prism' (Which tree) (Which branch) +inject = prism' diversify (hush . reinterpret) +{-# INLINE inject #-} + +-- | 'diversifyN' ('review' 'injectN') and 'reinterpretN' ('preview' 'injectN') in 'Prism'' form. +-- +-- @ +-- let x = 'pick' (5 :: Int) :: 'Which' '[String, Int] +-- y = 'review' (injectN \@[3, 1] \@_ \@[Bool, Int, Char, String] Proxy) x -- 'diversifyN' +-- y \`shouldBe` pick (5 :: Int) :: 'Which' '[Bool, Int, Char, String] +-- let y' = 'preview' ('injectN' @[3, 1] \@[String, Int] Proxy) y -- 'reinterpertN'' +-- y' \`shouldBe` Just ('pick' (5 :: Int)) :: Maybe ('Which' '[String, Int]) +-- @ +injectN + :: forall indices branch tree proxy. + ( DiversifyN indices tree branch + , ReinterpretN indices branch tree + ) + => proxy indices -> Prism' (Which tree) (Which branch) +injectN p = prism' (diversifyN p) (reinterpretN p) +{-# INLINE injectN #-} + +------------------------------------------------------------------ + +-- | 'Switch' is an instance of 'Reduce' for which __'reiterate'__s through the possibilities in a 'Which', +-- delegating handling to 'Case', ensuring termination when 'Which' only contains one type. +newtype Switch c (xs :: [Type]) r = Switch (c xs r) + +-- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterate'__ +-- trying the next type in the type list. +-- This code will be efficiently compiled into a single case statement in GHC 8.2.1 +-- See http://hsyl20.fr/home/posts/2016-12-12-control-flow-in-haskell-part-2.html +instance (Case c (x ': x' ': xs) r, Reduce Which (Switch c) (x' ': xs) r, Reiterate c (x : x' : xs)) => + Reduce Which (Switch c) (x ': x' ': xs) r where + reduce (Switch c) v = + case trial0 v of + Right a -> case' c a + Left v' -> reduce (Switch (reiterate c)) v' + {-# INLINE reduce #-} + +-- | Terminating case of the loop, ensuring that a instance of @Case '[]@ +-- with an empty typelist is not required. +-- You can't reduce 'impossible' +instance (Case c '[x] r) => Reduce Which (Switch c) '[x] r where + reduce (Switch c) v = case obvious v of + a -> case' c a + +-- | Catamorphism for 'Which'. This is equivalent to @flip 'switch'@. +which :: Reduce Which (Switch case') xs r => case' xs r -> Which xs -> r +which = reduce . Switch + +-- | A switch/case statement for 'Which'. This is equivalent to @flip 'which'@ +-- +-- Use 'Case' instances like 'Data.Diverse.Cases.Cases' to apply a 'Which' of functions to a variant of values. +-- +-- @ +-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] +-- 'Data.Diverse.Which.switch' y ( +-- 'Data.Diverse.Cases.cases' (show \@Bool +-- 'Data.Diverse.Many../' show \@Int +-- 'Data.Diverse.Many../' 'Data.Diverse.Many.nul')) \`shouldBe` "5" +-- @ +-- +-- Or 'Data.Diverse.CaseTypeable.CaseTypeable' to apply a polymorphic function that work on all 'Typeables'. +-- +-- @ +-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool] +-- 'Data.Diverse.Which.switch' y ('CaseTypeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` "Int" +-- @ +-- +-- Or you may use your own custom instance of 'Case'. +switch :: Reduce Which (Switch case') xs r => Which xs -> case' xs r -> r +switch = flip which + +------------------------------------------------------------------ + +-- | 'SwitchN' is a variation of 'Switch' which __'reiterateN'__s through the possibilities in a 'Which', +-- delegating work to 'CaseN', ensuring termination when 'Which' only contains one type. +newtype SwitchN c (n :: Nat) (xs :: [Type]) r = SwitchN (c n xs r) + +-- | 'trial0' each type in a 'Which', and either handle the 'case'' with value discovered, or __'reiterateN'__ +-- trying the next type in the type list. +-- This code will be efficiently compiled into a single case statement in GHC 8.2.1 +-- See http://hsyl20.fr/home/posts/2016-12-12-control-flow-in-haskell-part-2.html +instance (Case (c n) (x ': x' ': xs) r, Reduce Which (SwitchN c (n + 1)) (x' ': xs) r, ReiterateN c n (x : x' : xs)) => + Reduce Which (SwitchN c n) (x ': x' ': xs) r where + reduce (SwitchN c) v = + case trial0 v of + Right a -> case' c a + Left v' -> reduce (SwitchN (reiterateN c)) v' + {-# INLINE reduce #-} + +-- | Terminating case of the loop, ensuring that a instance of @Case '[]@ +-- with an empty typelist is not required. +-- You can't reduce 'impossible' +instance (Case (c n) '[x] r) => Reduce Which (SwitchN c n) '[x] r where + reduce (SwitchN c) v = case obvious v of + a -> case' c a + +-- | Catamorphism for 'Which'. This is equivalent to @flip 'switchN'@. +whichN :: Reduce Which (SwitchN case' n) xs r => case' n xs r -> Which xs -> r +whichN = reduce . SwitchN + +-- | A switch/case statement for 'Which'. This is equivalent to @flip 'whichN'@ +-- +-- Use 'Case' instances like 'Data.Diverse.Cases.CasesN' to apply a 'Which' of functions to a variant of values +-- in index order. +-- +-- @ +-- let y = 'pickN' \@0 Proxy (5 :: Int) :: 'Which' '[Int, Bool, Bool, Int] +-- 'switchN' y ( +-- 'Data.Diverse.Cases.casesN' (show \@Int +-- 'Data.Diverse.Many../' show \@Bool +-- 'Data.Diverse.Many../' show \@Bool +-- 'Data.Diverse.Many../' show \@Int +-- 'Data.Diverse.Many../' 'Data.Diverse.Many.nul')) \`shouldBe` "5" +-- @ +-- +-- Or you may use your own custom instance of 'Case'. +switchN :: Reduce Which (SwitchN case' n) xs r => Which xs -> case' n xs r -> r +switchN = flip whichN + +----------------------------------------------------------------- + +-- | Two 'Which'es are only equal iff they both contain the equivalnet value at the same type index. +instance (Reduce Which (Switch CaseEqWhich) (x ': xs) Bool) => Eq (Which (x ': xs)) where + l@(Which i _) == (Which j u) = + if i /= j + then False + else switch l (CaseEqWhich u) + +-- | @('impossible' == 'impossible') == True@ +instance Eq (Which '[]) where + _ == _ = True + +-- | Do not export constructor +-- Stores the right Any to be compared when the correct type is discovered +newtype CaseEqWhich (xs :: [Type]) r = CaseEqWhich Any + +instance Reiterate CaseEqWhich (x ': xs) where + reiterate (CaseEqWhich r) = CaseEqWhich r + +instance (Eq x) => Case CaseEqWhich (x ': xs) Bool where + case' (CaseEqWhich r) l = l == unsafeCoerce r + +----------------------------------------------------------------- + +-- | A 'Which' with a type at smaller type index is considered smaller. +instance (Reduce Which (Switch CaseEqWhich) (x ': xs) Bool, Reduce Which (Switch CaseOrdWhich) (x ': xs) Ordering) => Ord (Which (x ': xs)) where + compare l@(Which i _) (Which j u) = + if i /= j + then compare i j + else switch l (CaseOrdWhich u) + +-- | @('compare' 'impossible' 'impossible') == EQ@ +instance Ord (Which '[]) where + compare _ _ = EQ + +-- | Do not export constructor +-- Stores the right Any to be compared when the correct type is discovered +newtype CaseOrdWhich (xs :: [Type]) r = CaseOrdWhich Any + +instance Reiterate CaseOrdWhich (x ': xs) where + reiterate (CaseOrdWhich r) = CaseOrdWhich r + +instance (Ord x) => Case CaseOrdWhich (x ': xs) Ordering where + case' (CaseOrdWhich r) l = compare l (unsafeCoerce r) + +------------------------------------------------------------------ + +-- | @show ('pick'' \'A') == "pick \'A'"@ +instance (Reduce Which (Switch CaseShowWhich) (x ': xs) ShowS) => Show (Which (x ': xs)) where + showsPrec d v = showParen (d > app_prec) ((showString "pick ") . (which CaseShowWhich v)) + where app_prec = 10 + +-- | @read "impossible" == 'impossible'@ +instance Show (Which '[]) where + showsPrec d _ = showParen (d > app_prec) (showString "impossible") + where app_prec = 10 + +data CaseShowWhich (xs :: [Type]) r = CaseShowWhich + +instance Reiterate CaseShowWhich (x ': xs) where + reiterate CaseShowWhich = CaseShowWhich + +instance Show x => Case CaseShowWhich (x ': xs) ShowS where + case' _ = showsPrec (app_prec + 1) + where app_prec = 10 + +------------------------------------------------------------------ + +newtype EmitReadWhich (xs :: [Type]) r = EmitReadWhich Int + +instance Reiterate EmitReadWhich (x ': xs) where + reiterate (EmitReadWhich i) = EmitReadWhich (i + 1) + +instance Read x => Emit EmitReadWhich (x ': xs) (ReadPrec (Int, WrappedAny)) where + emit (EmitReadWhich i) = (\a -> (i, WrappedAny (unsafeCoerce a))) <$> readPrec @x + +readWhich + :: forall xs. + AFoldable (Collector EmitReadWhich xs) (ReadPrec (Int, WrappedAny)) + => Proxy (xs :: [Type]) -> ReadPrec (Int, WrappedAny) +readWhich _ = afoldr (<|>) empty (Collector (EmitReadWhich @xs 0)) + +-- | This 'Read' instance tries to read using the each type in the typelist, using the first successful type read. +instance AFoldable (Collector EmitReadWhich (x ': xs)) (ReadPrec (Int, WrappedAny)) => + Read (Which (x ': xs)) where + readPrec = + parens $ + prec 10 $ do + lift $ L.expect (Ident "pick") + (n, WrappedAny v) <- step (readWhich @(x ': xs) Proxy) + pure (Which n v) + +-- | @read "impossible" == 'impossible'@ +instance Read (Which '[]) where + readPrec = + parens $ + prec 10 $ do + lift $ L.expect (Ident "impossible") + pure impossible + +-- | 'WrappedAny' avoids the following: +-- Illegal type synonym family application in instance: Any +newtype WrappedAny = WrappedAny Any diff --git a/test/Data/Diverse/ManySpec.hs b/test/Data/Diverse/ManySpec.hs new file mode 100644 --- /dev/null +++ b/test/Data/Diverse/ManySpec.hs @@ -0,0 +1,277 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Diverse.ManySpec (main, spec) where + +import Control.Lens +import Data.Diverse +import Data.Typeable +import Test.Hspec + +-- `main` is here so that this module can be run from GHCi on its own. It is +-- not needed for automatic spec discovery. +main :: IO () +main = hspec spec + +spec :: Spec +spec = do + describe "Many" $ do + it "is a Typeable" $ do + let x = (5 :: Int) ./ False ./ nul + y = cast x :: Maybe (Many '[Int, String]) + z = cast x :: Maybe (Many '[Int, Bool]) + y `shouldBe` Nothing + z `shouldBe` Just x + (show . typeRep . (pure @Proxy) $ x) `shouldBe` "Many (': * Int (': * Bool '[]))" + + it "is a Read and Show" $ do + let s = "5 ./ False ./ 'X' ./ Just 'O' ./ nul" + x = read s :: Many '[Int, Bool, Char, Maybe Char] + show x `shouldBe` s + + it "is a Eq" $ do + let s = "5 ./ False ./ 'X' ./ Just 'O' ./ nul" + x = read s :: Many '[Int, Bool, Char, Maybe Char] + y = 5 ./ False ./ 'X' ./ Just 'O' ./ nul + x `shouldBe` y + + it "is an Ord" $ do + let s = "5 ./ False ./ 'X' ./ Just 'O' ./ nul" + x = read s :: Many '[Int, Bool, Char, Maybe Char] + y5o = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + y4o = (4 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + y5p = (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + compare x y5o `shouldBe` EQ + compare y4o y5o `shouldBe` LT + compare y5o y4o `shouldBe` GT + compare y5o y5p `shouldBe` LT + compare y5p y5o `shouldBe` GT + + it "can converted to and from a tuple" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + y' = ((5 :: Int), False, 'X', Just 'O') + y = toMany' y' + y2 = review _Many' y' + x' = fromMany' x + x2' = view _Many' x + x `shouldBe` y + x `shouldBe` y2 + x' `shouldBe` y' + x2' `shouldBe` y' + + it "can construct using 'single', 'nul', 'prefix', 'postfix', 'append'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + x' = (5 :: Int) `prefix` False `prefix` 'X' `prefix` Just 'O' `prefix` nul + y = single (5 :: Int) \. False \. 'X' \. Just 'O' + y' = single (5 :: Int) `postfix` False `postfix` 'X' `postfix` Just 'O' + a = single (5 :: Int) `postfix` False + b = single 'X' `postfix` Just 'O' + x `shouldBe` y + x `shouldBe` x' + y `shouldBe` y' + a /./ b `shouldBe` x + a `append` b `shouldBe` x + + it "can contain multiple fields of the same type" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + (x /./ (6 :: Int) ./ Just 'A' ./ nul) `shouldBe` y + + it "can destruct using 'front', 'back', 'aft', 'fore'" $ do + let a = (x ./ y) \. z + x = 5 :: Int + y = single False ./ 'X' ./ nul + z = Just 'O' + front a `shouldBe` x + back a `shouldBe` z + aft a `shouldBe` (y \. z) + fore a `shouldBe` x ./ y + + it "has getter for unique fields using 'fetch'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + fetch @Int x `shouldBe` 5 + x .^. (Proxy @Int) `shouldBe` 5 + fetch @Bool x `shouldBe` False + x .^. (Proxy @Bool) `shouldBe` False + fetch @Char x `shouldBe` 'X' + x .^. (Proxy @Char) `shouldBe` 'X' + fetch @(Maybe Char) x `shouldBe` Just 'O' + x .^. (Proxy @(Maybe Char))`shouldBe` Just 'O' + + it "has getter for for unique fields using 'fetchN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + fetchN @0 Proxy x `shouldBe` 5 + fetchN @1 Proxy x `shouldBe` False + fetchN @2 Proxy x `shouldBe` 'X' + fetchN @3 Proxy x `shouldBe` Just 'O' + + it "has getter for duplicate fields using 'fetchN'" $ do + let y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + fetchN @0 Proxy y `shouldBe` 5 + fetchN @1 Proxy y `shouldBe` False + fetchN @2 Proxy y `shouldBe` 'X' + fetchN @3 Proxy y `shouldBe` Just 'O' + fetchN @4 Proxy y `shouldBe` 6 + fetchN @5 Proxy y `shouldBe` Just 'A' + + it "with duplicate fields can still use 'fetch' for unique fields" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + fetch @Bool x `shouldBe` False + x .^. (Proxy @Bool) `shouldBe` False + fetch @Char x `shouldBe` 'X' + x .^. (Proxy @Char) `shouldBe` 'X' + + it "has setter for unique fields using 'replace'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + replace @Int x 6 `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + (x .~. (6 :: Int)) `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + replace x True `shouldBe` (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ nul + (x .~. True) `shouldBe` (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ nul + replace x 'O' `shouldBe` (5 :: Int) ./ False ./ 'O' ./ Just 'O' ./ nul + (x .~. 'O') `shouldBe` (5 :: Int) ./ False ./ 'O' ./ Just 'O' ./ nul + replace x (Just 'P') `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + (x .~. (Just 'P')) `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + + it "has setter for unique fields using 'replaceN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + replaceN @0 Proxy x 7 `shouldBe` + (7 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + replaceN @1 Proxy x True `shouldBe` + (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ nul + replaceN @2 Proxy x 'Y' `shouldBe` + (5 :: Int) ./ False ./ 'Y' ./ Just 'O' ./ nul + replaceN @3 Proxy x (Just 'P') `shouldBe` + (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + + it "has setter for duplicate fields using 'replaceN'" $ do + let y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replaceN @0 Proxy y 7 `shouldBe` + (7 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replaceN @1 Proxy y True `shouldBe` + (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replaceN @2 Proxy y 'Y' `shouldBe` + (5 :: Int) ./ False ./ 'Y' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replaceN @3 Proxy y (Just 'P') `shouldBe` + (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ (6 :: Int) ./ Just 'A' ./ nul + replaceN @4 Proxy y 8 `shouldBe` + (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (8 :: Int) ./ Just 'A' ./ nul + replaceN @5 Proxy y (Just 'B') `shouldBe` + (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'B' ./ nul + + it "has setter for unique fields using 'replace' (even if there are other duplicate fields)" $ do + let y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replace @Bool y True `shouldBe` + (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + replace @Char y 'Y' `shouldBe` + (5 :: Int) ./ False ./ 'Y' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + + it "has getter/setter lens using 'item'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + x ^. item @Int `shouldBe` 5 + (x & item @Int .~ 6) `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + x ^. item @Bool `shouldBe` False + (x & item @Bool .~ True) `shouldBe` (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ nul + x ^. item @Char `shouldBe` 'X' + (x & item @Char .~ 'O') `shouldBe` (5 :: Int) ./ False ./ 'O' ./ Just 'O' ./ nul + x ^. item @(Maybe Char) `shouldBe` Just 'O' + (x & item @(Maybe Char) .~ Just 'P') `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + + it "has getter/setter lens for duplicate fields using 'itemN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @0) `shouldBe` 5 + (x & itemN (Proxy @0) .~ 6) `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @1) `shouldBe` False + (x & itemN (Proxy @1) .~ True) `shouldBe` (5 :: Int) ./ True ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @2) `shouldBe` 'X' + (x & itemN (Proxy @2) .~ 'O') `shouldBe` (5 :: Int) ./ False ./ 'O' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @3) `shouldBe` Just 'O' + (x & itemN (Proxy @3) .~ Just 'P') `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'P' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @4) `shouldBe` 6 + (x & itemN (Proxy @4) .~ 7) `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (7 :: Int) ./ Just 'A' ./ nul + x ^. itemN (Proxy @5) `shouldBe` Just 'A' + (x & itemN (Proxy @5) .~ Just 'B') `shouldBe` (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'B' ./ nul + + it "has getter for multiple fields using 'narrow'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + narrow @'[Int, Maybe Char] x `shouldBe` (5 :: Int) ./ Just 'O' ./ nul + x \^. (Proxy @'[Int, Maybe Char]) `shouldBe` (5 :: Int) ./ Just 'O' ./ nul + + it "can reorder fields using 'narrow' or 'narrowN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + narrow @'[Bool, Int, Maybe Char] x `shouldBe` False ./ (5 :: Int) ./ Just 'O' ./ nul + let y = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + narrowN (Proxy @'[5, 4, 0, 1, 3, 2]) y `shouldBe` + Just 'A' ./ (6 :: Int) ./ (5 ::Int) ./ False ./ Just 'O' ./ 'X' ./ nul + + it "has getter for multiple fields with duplicates using 'narrowN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + narrowN (Proxy @'[5, 4, 0]) x `shouldBe` Just 'A' ./ (6 :: Int) ./ (5 ::Int) ./ nul + + it "can't narrow into types from indistinct fields" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + -- Compile error: Int is a duplicate + -- narrow @[Bool, Char, Int] x `shouldBe` False ./ 'X' ./ (5 :: Int) ./ nul + x `shouldBe` x + + it "with duplicate fields has getter for multiple unique fields 'narrow'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + narrow @'[Bool, Char] x `shouldBe` False ./ 'X' ./ nul + x \^. (Proxy @'[Bool, Char]) `shouldBe` False ./ 'X' ./ nul + + it "has setter for multiple fields using 'amend'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + amend @'[Int, Maybe Char] x ((6 :: Int) ./ Just 'P' ./ nul) `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + (x \~. (6 :: Int) ./ Just 'P' ./ nul) `shouldBe` (6 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + + it "has setter for multiple fields with duplicates using 'amendN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + amendN (Proxy @'[5, 4, 0]) x (Just 'B' ./ (8 :: Int) ./ (4 ::Int) ./ nul) `shouldBe` + (4 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (8 :: Int) ./ Just 'B' ./ nul + + it "can't amend into types from indistinct fields" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + -- Compile error: Int is a duplicate + -- amend @ '[Bool, Char, Int] x (True ./ 'B' ./ (8 :: Int) ./ nul) `shouldBe` + -- (5 :: Int) ./ True ./ 'B' ./ Just 'O' ./ (8 :: Int) ./ Just 'A' ./ nul + x `shouldBe` x + + it "with duplicate fields has setter for unique fields 'amend'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + amend @ '[Bool, Char] x (True ./ 'B' ./ nul) `shouldBe` + (5 :: Int) ./ True ./ 'B' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + + it "has getter/setter lens for multiple fields using 'project'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ nul + x ^. (project @'[Int, Maybe Char]) `shouldBe` (5 :: Int) ./ Just 'O' ./ nul + (x & (project @'[Int, Maybe Char]) .~ ((6 :: Int) ./ Just 'P' ./ nul)) `shouldBe` + (6 :: Int) ./ False ./ 'X' ./ Just 'P' ./ nul + + it "has getter/setter lens for multiple fields with duplicates using 'projectN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + x ^. (projectN @'[5, 4, 0] Proxy) `shouldBe` Just 'A' ./ (6 :: Int) ./ (5 ::Int) ./ nul + (x & (projectN @'[5, 4, 0] Proxy) .~ (Just 'B' ./ (8 :: Int) ./ (4 ::Int) ./ nul)) `shouldBe` + (4 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (8 :: Int) ./ Just 'B' ./ nul + + it "can be folded with 'Many' handlers using 'forMany' or 'collect'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + y = show @Int ./ show @Char ./ show @(Maybe Char) ./ show @Bool ./ nul + ret = ["5", "False", "'X'", "Just 'O'", "6", "Just 'A'"] + afoldr (:) [] (collect x (cases y)) `shouldBe` ret + afoldr (:) [] (forMany (cases y) x) `shouldBe` ret + afoldr (:) [] (forMany (cases y) x) `shouldBe` ret + + it "can be folded with single 'CaseTypeable' handlers using 'forMany' or 'collect'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + afoldr (:) [] (forMany (CaseTypeable (show . typeRep . (pure @Proxy))) x) `shouldBe` ["Int", "Bool", "Char", "Maybe Char", "Int", "Maybe Char"] + + it "can be folded with 'Many' handlers in index order using 'forManyN' or 'collectN'" $ do + let x = (5 :: Int) ./ False ./ 'X' ./ Just 'O' ./ (6 :: Int) ./ Just 'A' ./ nul + y = show @Int ./ show @Bool ./ show @Char ./ show @(Maybe Char) ./ show @Int ./ show @(Maybe Char) ./ nul + ret = ["5", "False", "'X'", "Just 'O'", "6", "Just 'A'"] + afoldr (:) [] (collectN x (casesN y)) `shouldBe` ret + afoldr (:) [] (forManyN (casesN y) x) `shouldBe` ret diff --git a/test/Data/Diverse/TypeSpec.hs b/test/Data/Diverse/TypeSpec.hs new file mode 100644 --- /dev/null +++ b/test/Data/Diverse/TypeSpec.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Diverse.TypeSpec (main, spec) where + +import Data.Diverse +import Data.Typeable +import GHC.TypeLits +import Test.Hspec + +-- `main` is here so that this module can be run from GHCi on its own. It is +-- not needed for automatic spec discovery. +main :: IO () +main = hspec spec + +spec :: Spec +spec = do + describe "TypeLevel" $ do + it "PositionOf" $ do + fromIntegral (natVal @(PositionOf String '[Bool, Int]) Proxy) `shouldBe` (0 :: Int) + fromIntegral (natVal @(PositionOf Bool '[Bool, Int]) Proxy) `shouldBe` (1 :: Int) + fromIntegral (natVal @(PositionOf Int '[Bool, Int]) Proxy) `shouldBe` (2 :: Int) + fromIntegral (natVal @(PositionOf Int '[Bool, Int, Char]) Proxy) `shouldBe` (2 :: Int) + fromIntegral (natVal @(PositionOf Int '[Bool, String, Char]) Proxy) `shouldBe` (0 :: Int) + + it "ComplementOf" $ do + let complementTest :: (Complement xs ys ~ comp) => Proxy xs -> Proxy ys -> Proxy comp -> Proxy comp + complementTest _ _ comp = comp + + complementTest (Proxy @[String, Int]) (Proxy @[Bool, Int]) (Proxy @'[String]) `shouldBe` Proxy + complementTest (Proxy @[String, Int, Char]) (Proxy @[Bool, Int]) (Proxy @[String, Char]) `shouldBe` Proxy + complementTest (Proxy @[Bool, Int]) (Proxy @[Bool, Int]) (Proxy @'[]) `shouldBe` Proxy + complementTest (Proxy @[String, Bool]) (Proxy @[Int, Char]) (Proxy @'[String, Bool]) `shouldBe` Proxy diff --git a/test/Data/Diverse/WhichSpec.hs b/test/Data/Diverse/WhichSpec.hs new file mode 100644 --- /dev/null +++ b/test/Data/Diverse/WhichSpec.hs @@ -0,0 +1,242 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Diverse.WhichSpec (main, spec) where + +import Control.Lens +import Data.Diverse +import Data.Typeable +import Test.Hspec + +-- `main` is here so that this module can be run from GHCi on its own. It is +-- not needed for automatic spec discovery. +main :: IO () +main = hspec spec + +-- | Utility to convert Either to Maybe +hush :: Either a b -> Maybe b +hush = either (const Nothing) Just + +spec :: Spec +spec = do + describe "Which" $ do + + it "is a Read and Show" $ do + let s = "pick 5" + x = read s :: Which '[Int, Bool] + show x `shouldBe` "pick 5" + "impossible" `shouldBe` show impossible + "impossible" `shouldBe` show (read "impossible" :: Which '[]) + + it "is an Eq" $ do + let y = pick (5 :: Int) :: Which '[Int, Bool] + let y' = pick (5 :: Int) :: Which '[Int, Bool] + y `shouldBe` y' + read (show impossible) `shouldBe` impossible + + it "is an Ord" $ do + let y5 = pick (5 :: Int) :: Which '[Int, Bool] + let y6 = pick (6 :: Int) :: Which '[Int, Bool] + compare y5 y5 `shouldBe` EQ + compare y5 y6 `shouldBe` LT + compare y6 y5 `shouldBe` GT + compare impossible impossible `shouldBe` EQ + + it "can be constructed by type with 'pick' and destructed with 'trial'" $ do + let y = pick (5 :: Int) :: Which '[Bool, Int, Char] + x = hush $ trial @Int y + x `shouldBe` (Just 5) + + it "may contain possiblities of duplicate types" $ do + let y = pick (5 :: Int) :: Which '[Bool, Int, Char, Bool, Char] + x = hush $ trial @Int y + x `shouldBe` (Just 5) + + it "can be constructed conveniently with 'pick'' and destructed with 'trial0'" $ do + let y = pickOnly (5 :: Int) + x = hush $ trial0 y + x `shouldBe` (Just 5) + + it "can be constructed by index with 'pickN' and destructed with 'trialN" $ do + let y = pickN (Proxy @4) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] + x = hush $ trialN (Proxy @4) y + x `shouldBe` (Just 5) + + it "can be 'trial'led until its final 'obvious' value" $ do + let a = pick @'[Char, Int, Bool, String] (5 :: Int) + b = pick @'[Char, Int, String] (5 :: Int) + c = pick @'[Int, String] (5 :: Int) + d = pick @'[Int] (5 :: Int) + trial @Int a `shouldBe` Right 5 + trial @Bool a `shouldBe` Left b + trial @Int b `shouldBe` Right 5 + trial @Char b `shouldBe` Left c + trial @Int c `shouldBe` Right 5 + trial @String c `shouldBe` Left d + trial @Int d `shouldBe` Right 5 + trial @Int d `shouldNotBe` Left impossible + obvious d `shouldBe` 5 + + it "can be 'trialN'led until its final 'obvious' value" $ do + let a = pickN @2 @'[Char, Bool, Int, Bool, Char, String] Proxy (5 :: Int) + b = pickN @2 @'[Char, Bool, Int, Char, String] Proxy (5 :: Int) + c = pickN @2 @'[Char, Bool, Int, String] Proxy (5 :: Int) + d = pickN @1 @'[Bool, Int, String] Proxy (5 :: Int) + e = pickN @1 @'[Bool, Int] Proxy (5 :: Int) + f = pickN @0 @'[Int] Proxy (5 :: Int) + trial @Int a `shouldBe` Right 5 + trialN @2 Proxy a `shouldBe` Right 5 + trialN @3 Proxy a `shouldBe` Left b + + trial @Int b `shouldBe` Right 5 + trialN @2 Proxy b `shouldBe` Right 5 + trialN @3 Proxy b `shouldBe` Left c + + trial @Int c `shouldBe` Right 5 + trialN @2 Proxy c `shouldBe` Right 5 + trial0 c `shouldBe` Left d + trialN @0 Proxy c `shouldBe` Left d + + trial @Int d `shouldBe` Right 5 + trialN @1 Proxy d `shouldBe` Right 5 + trialN @2 Proxy d `shouldBe` Left e + + trial @Int e `shouldBe` Right 5 + trialN @1 Proxy e `shouldBe` Right 5 + trialN @0 Proxy e `shouldBe` Left f + trial0 e `shouldBe` Left f + + trial @Int f `shouldBe` Right 5 + trial @Int f `shouldNotBe` Left impossible + trial0 f `shouldBe` Right 5 + obvious f `shouldBe` 5 + + it "can be constructed and destructed by type with 'facet'" $ do + let y = review (facet @Int) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Char] + x = preview (facet @Int) y + x `shouldBe` (Just 5) + + it "can be constructed and destructed by index with 'facetN'" $ do + let y = review (facetN (Proxy @4)) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] + x = preview (facetN (Proxy @4)) y + x `shouldBe` (Just 5) + + it "can be extended and rearranged by type with 'diversify'" $ do + let y = pickOnly (5 :: Int) + y' = diversify @[Int, Bool] y + y'' = diversify @[Bool, Int] y' + switch y'' (CaseTypeable (show . typeRep . (pure @Proxy))) `shouldBe` "Int" + + it "can be extended and rearranged by index with 'diversify'" $ do + let y = pickOnly (5 :: Int) + y' = diversifyN @'[0] @[Int, Bool] Proxy y + y'' = diversifyN @[1,0] @[Bool, Int] Proxy y' + switch y'' (CaseTypeable (show . typeRep . (pure @Proxy))) `shouldBe` "Int" + + it "the 'diversify'ed type can contain multiple fields if they aren't in the original 'Many'" $ do + let y = pick @[Int, Char] (5 :: Int) + x = diversify @[String, String, Char, Bool, Int] y + -- Compile error: Char is a duplicate + -- z = diversify @[String, String, Char, Bool, Int, Char] y + x `shouldBe` pick (5 :: Int) + + it "the 'diversify'ed type can't use indistinct fields from the original 'Many'" $ do + let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int + -- Compile error: Int is a duplicate + -- x = diversify @[String, String, Char, Bool, Int] y + y `shouldBe` y + + it "can be 'reinterpret'ed by type into a totally different Which" $ do + let y = pick @[Int, Char] (5 :: Int) + a = reinterpret @[String, Bool] y + a `shouldBe` Left y + let b = reinterpret @[String, Char] y + b `shouldBe` Left (pick (5 :: Int)) + let c = reinterpret @[String, Int] y + c `shouldBe` Right (pick (5 :: Int)) + + it "the 'reinterpret' type can contain indistinct fields if they aren't in the original 'Many'" $ do + let y = pick @[Int, Char] (5 :: Int) + x = reinterpret @[String, String, Char, Bool] y + -- Compile error: Char is a duplicate + -- z = reinterpret @[String, Char, Char, Bool] y + x `shouldBe` Left (pick (5 :: Int)) + + it "the 'reinterpret'ed from type can't indistinct fields'" $ do + let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int + -- Compile error: Int is a duplicate + -- x = reinterpret @[String, String, Char, Bool] y + y `shouldBe` y + + it "the 'reinterpret' type can't use indistinct fields from the original 'Many'" $ do + let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int + -- Compile error: Int is a duplicate + -- x = reinterpret @[String, String, Char, Bool, Int] y + y `shouldBe` y + + it "can be 'reinterpretN'ed by index into a subset Which" $ do + let y = pick @[Char, String, Int, Bool] (5 :: Int) + a = reinterpretN @[2, 0] @[Int, Char] Proxy y + a' = reinterpretN @[3, 0] @[Bool, Char] Proxy y + a `shouldBe` Just (pick (5 :: Int)) + a' `shouldBe` Nothing + + it "can be 'diversify'ed and 'reinterpreted' by type with 'inject'" $ do + let x = pick (5 :: Int) :: Which '[String, Int] + y = review (inject @_ @[Bool, Int, Char, String]) x + y `shouldBe` pick (5 :: Int) + let y' = preview (inject @[String, Int]) y + y' `shouldBe` Just (pick (5 :: Int)) + + it "can be 'diversifyN'ed and 'reinterpretedN' by index with 'injectN'" $ do + let x = pick (5 :: Int) :: Which '[String, Int] + y = review (injectN @[3, 1] @_ @[Bool, Int, Char, String] Proxy) x + y `shouldBe` pick (5 :: Int) + let y' = preview (injectN @[3, 1] @[String, Int] Proxy) y + y' `shouldBe` Just (pick (5 :: Int)) + + it "can be 'switch'ed with 'Many' handlers in any order" $ do + let y = pickN @0 Proxy (5 :: Int) :: Which '[Int, Bool, Bool, Int] + switch y ( + cases (show @Bool + ./ show @Int + ./ nul)) `shouldBe` "5" + + it "can be 'switch'ed with 'Many' handlers with extraneous content" $ do + let y = pick (5 :: Int) :: Which '[Int, Bool] + switch y ( + -- contrast with lowercase 'cases' which disallows extraneous content + Cases (show @Int + ./ show @Bool + ./ show @Char + ./ 'X' + ./ False + ./ nul + )) `shouldBe` "5" + + it "can be 'switchN'ed with 'Many' handlers in index order" $ do + let y = pickN @0 Proxy (5 :: Int) :: Which '[Int, Bool, Bool, Int] + switchN y ( + casesN (show @Int + ./ show @Bool + ./ show @Bool + ./ show @Int + ./ nul)) `shouldBe` "5" + + it "can be switched with a single 'CaseTypeable' handler" $ do + let y = pick (5 :: Int) :: Which '[Int, Bool] + switch y (CaseTypeable (show . typeRep . (pure @Proxy))) `shouldBe` "Int" + (show . typeRep . (pure @Proxy) $ y) `shouldBe` "Which (': * Int (': * Bool '[]))" + + it "is a compile error to 'trial', 'diversify', 'reinterpret 'impossible'" $ do + -- let a = diversify @[Int, Bool] impossible + -- let a = trial @Int impossible + -- let a = trialN (Proxy @0) impossible + -- let a = reinterpret @[Int, Bool] impossible + -- let a = reinterpretN (Proxy @'[0]) impossible + impossible `shouldBe` impossible diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}