list-witnesses (empty) → 0.1.0.0
raw patch · 7 files changed
+934/−0 lines, 7 filesdep +basedep +decidabledep +profunctorssetup-changed
Dependencies added: base, decidable, profunctors, singletons, vinyl
Files
- CHANGELOG.md +12/−0
- LICENSE +30/−0
- README.md +12/−0
- Setup.hs +2/−0
- list-witnesses.cabal +51/−0
- src/Data/Type/List/Edit.hs +523/−0
- src/Data/Type/List/Sublist.hs +304/−0
+ CHANGELOG.md view
@@ -0,0 +1,12 @@+Changelog+=========++Version 0.1.0.0+---------------++*March 6, 2019*++<https://github.com/mstksg/list-witnesses/releases/tag/v0.1.0.0>++* Initial release+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Justin Le (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Justin Le nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,12 @@+[list-witnesses][docs]+======================++[](https://hackage.haskell.org/package/list-witnesses)++Collection of assorted inductive witnesses and functions for working with+type-level lists.++* *Data.Type.List.Edit* contains single-item edits of lists, including+ insertion, deletion, and substitution.+* *Data.Type.List.Sublist* contains witnesses for prefixes, suffixes, and+ two-way splits of type-level lists.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ list-witnesses.cabal view
@@ -0,0 +1,51 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: cac47cdc9c99203dbddf17af85d8059d9f0f1a5b418bcee9e763020655a5f1ab++name: list-witnesses+version: 0.1.0.0+synopsis: Witnesses for working with type-level lists+description: Collection of assorted inductive witnesses and functions for working with+ type-level lists.+ .+ * *Data.Type.List.Edit* contains single-item edits of lists, including+ insertion, deletion, and substitution.+ * *Data.Type.List.Sublist* contains witnesses for prefixes, suffixes, and+ two-way splits of type-level lists.+category: Dependent Types+homepage: https://github.com/mstksg/list-witnesses#readme+bug-reports: https://github.com/mstksg/list-witnesses/issues+author: Justin Le+maintainer: justin@jle.im+copyright: (c) Justin Le 2018+license: BSD3+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md+ CHANGELOG.md++source-repository head+ type: git+ location: https://github.com/mstksg/list-witnesses++library+ exposed-modules:+ Data.Type.List.Edit+ Data.Type.List.Sublist+ other-modules:+ Paths_list_witnesses+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat -Wredundant-constraints -Werror=incomplete-patterns+ build-depends:+ base >=4.7 && <5+ , decidable >=0.1.5+ , profunctors+ , singletons+ , vinyl+ default-language: Haskell2010
+ src/Data/Type/List/Edit.hs view
@@ -0,0 +1,523 @@+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module : Data.Type.List.Edit+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- Witnesses regarding single-item edits of lists.+module Data.Type.List.Edit (+ -- * Simple edits+ Insert(..)+ , Delete(..)+ , insToDel+ , delToIns+ , Substitute(..)+ , flipSub+ , subToDelIns+ -- ** Singletons+ , SInsert(..)+ , SDelete(..)+ , SSubstitute(..)+ -- * Compound edits+ , Edit(..)+ , compEdit+ , flipEdit+ -- * Rec+ , insertRec, deleteRec, deleteGetRec+ , recLens, substituteRec+ -- * Index+ -- ** Manipulating indices+ , insertIndex+ , DeletedIx(..), deleteIndex, deleteIndex_+ , SubstitutedIx(..), substituteIndex, substituteIndex_+ -- ** Converting from indices+ , withDelete, withInsert, withInsertAfter+ -- * Type-Level+ , InsertIndex, sInsertIndex+ , SDeletedIx(..)+ , DeleteIndex, sDeleteIndex+ , SSubstitutedIx(..)+ , SubstituteIndex, sSubstituteIndex+ -- ** Defunctionalization Symbols+ , InsertIndexSym0, InsertIndexSym+ , DeleteIndexSym0, DeleteIndexSym+ , SubstituteIndexSym0, SubstituteIndexSym+ ) where++import Data.Functor.Identity+import Data.Kind+import Data.Singletons+import Data.Type.Universe+import Data.Vinyl.Core+import qualified Control.Category as C++-- | An @'Insert' as bs x@ is a witness that you can insert @x@ into some+-- position in list @as@ to produce list @bs@. It is essentially 'Delete'+-- flipped.+--+-- Some examples:+--+-- @+-- InsZ :: Insert '[1,2,3] '[4,1,2,3] 4+-- InsS InsZ :: Insert '[1,2,3] '[1,4,2,3] 4+-- InsS (InsS InsZ) :: Insert '[1,2,3] '[1,2,4,3] 4+-- InsS (InsS (InsS InsZ) :: Insert '[1,2,3] '[1,2,3,4] 4+-- @+--+-- @bs@ will always be exactly one item longer than @as@.+data Insert :: [k] -> [k] -> k -> Type where+ InsZ :: Insert as (x ': as) x+ InsS :: Insert as bs x -> Insert (a ': as) (a ': bs) x++deriving instance Show (Insert as bs x)++-- | Kind-indexed singleton for 'Insert'.+data SInsert as bs x :: Insert as bs x -> Type where+ SInsZ :: SInsert as (x ': as) x 'InsZ+ SInsS :: SInsert as bs x ins -> SInsert (a ': as) (a ': bs) x ('InsS ins)++deriving instance Show (SInsert as bs x del)++-- | Flip an insertion.+insToDel :: Insert as bs x -> Delete bs as x+insToDel = \case+ InsZ -> DelZ+ InsS i -> DelS (insToDel i)++-- | A @'Delete' as bs x@ is a witness that you can delete item @x@ from+-- @as@ to produce the list @bs@. It is essentially 'Insert' flipped.+--+-- Some examples:+--+-- @+-- DelZ :: Delete '[1,2,3] '[2,3] 1+-- DelS DelZ :: Delete '[1,2,3] '[2,3] 2+-- DelS (DelS DelZ) :: Delete '[1,2,3] '[1,2] 3+-- @+--+-- @bs@ will always be exactly one item shorter than @as@.+data Delete :: [k] -> [k] -> k -> Type where+ DelZ :: Delete (x ': as) as x+ DelS :: Delete as bs x -> Delete (a ': as) (a ': bs) x++deriving instance Show (Delete as bs x)++-- | Kind-indexed singleton for 'Delete'.+data SDelete as bs x :: Delete as bs x -> Type where+ SDelZ :: SDelete (x ': as) as x 'DelZ+ SDelS :: SDelete as bs x del -> SDelete (a ': as) (a ': bs) x ('DelS del)++deriving instance Show (SDelete as bs x del)++-- | Flip a deletion.+delToIns :: Delete as bs x -> Insert bs as x+delToIns = \case+ DelZ -> InsZ+ DelS d -> InsS (delToIns d)++-- | A @'Substitute' as bs x y@ is a witness that you can replace item @x@ in+-- @as@ with item @y@ to produce @bs@.+--+-- Some examples:+--+-- @+-- SubZ :: Substitute '[1,2,3] '[4,2,3] 1 4+-- SubS SubZ :: Substitute '[1,2,3] '[1,4,3] 2 4+-- SubS (SubS SubZ) :: Substitute '[1,2,3] '[1,2,4] 3 4+-- @+--+data Substitute :: [k] -> [k] -> k -> k -> Type where+ SubZ :: Substitute (x ': as) (y ': as) x y+ SubS :: Substitute as bs x y -> Substitute (c ': as) (c ': bs) x y++deriving instance Show (Substitute as bs x y)++-- | Kind-indexed singleton for 'Substitute'.+data SSubstitute as bs x y :: Substitute as bs x y -> Type where+ SSubZ :: SSubstitute (x ': as) (y ': as) x y 'SubZ+ SSubS :: SSubstitute as bs x y sub+ -> SSubstitute (c ': as) (c ': bs) x y ('SubS sub)++-- | Flip a substitution+flipSub :: Substitute as bs x y -> Substitute bs as y x+flipSub = \case+ SubZ -> SubZ+ SubS s -> SubS (flipSub s)++-- | Decompose a 'Substitute' into a 'Delete' followed by an 'Insert'.+subToDelIns+ :: Substitute as bs x y+ -> (forall cs. Delete as cs x -> Insert cs bs y -> r)+ -> r+subToDelIns = \case+ SubZ -> \f -> f DelZ InsZ+ SubS s -> \f -> subToDelIns s $ \d i -> f (DelS d) (InsS i)++-- | An @'Edit' as bs@ is a reversible edit script transforming @as@ into+-- @bs@ through successive insertions, deletions, and substitutions.+--+-- TODO: implement Wagner-Fischer to minimize find a minimal edit distance+data Edit :: [k] -> [k] -> Type where+ ENil :: Edit as as+ EIns :: Insert bs cs x -> Edit as bs -> Edit as cs+ EDel :: Delete bs cs x -> Edit as bs -> Edit as cs+ ESub :: Substitute bs cs x y -> Edit as bs -> Edit as cs++deriving instance Show (Edit as bs)++-- | Compose two 'Edit's+compEdit :: Edit as bs -> Edit bs cs -> Edit as cs+compEdit xs = \case+ ENil -> xs+ EIns i ys -> EIns i (compEdit xs ys)+ EDel d ys -> EDel d (compEdit xs ys)+ ESub s ys -> ESub s (compEdit xs ys)++-- | 'Edit' composition+instance C.Category Edit where+ id = ENil+ xs . ys = compEdit ys xs++-- | Reverse an 'Edit' script. O(n^2). Please do not use.+--+-- TODO: Make O(n) using diff lists.+flipEdit :: Edit as bs -> Edit bs as+flipEdit = \case+ ENil -> ENil+ EIns i ys -> EDel (insToDel i) ENil `compEdit` flipEdit ys+ EDel d ys -> EIns (delToIns d) ENil `compEdit` flipEdit ys+ ESub s ys -> ESub (flipSub s) ENil `compEdit` flipEdit ys++-- | Insert a value into a 'Rec', at a position indicated by the 'Insert'.+insertRec :: Insert as bs x -> f x -> Rec f as -> Rec f bs+insertRec = \case+ InsZ -> (:&)+ InsS i -> \x -> \case+ y :& ys -> y :& insertRec i x ys++-- | Retrieve and delete a value in a 'Rec', at a position indicated by the 'Delete'.+deleteGetRec :: Delete as bs x -> Rec f as -> (f x, Rec f bs)+deleteGetRec = \case+ DelZ -> \case+ x :& xs -> (x, xs)+ DelS d -> \case+ x :& xs -> let (y, ys) = deleteGetRec d xs+ in (y, x :& ys)++-- | Delete a value in a 'Rec', at a position indicated by the 'Delete'.+deleteRec :: Delete as bs x -> Rec f as -> Rec f bs+deleteRec = \case+ DelZ -> \case+ _ :& xs -> xs+ DelS d -> \case+ x :& xs -> x :& deleteRec d xs++-- | A type-changing lens into a value in a 'Rec', given a 'Substitute'+-- indicating which value.+--+-- Read this type signature as:+--+-- @+-- 'recLens'+-- :: 'Substitute' as bs x y+-- -> Lens ('Rec' f as) (Rec f bs) (f x) (f y)+-- @+--+-- For example:+--+-- @+-- recLens (SubS SubZ)+-- :: Lens (Rec f '[a,b,c,d]) (Rec f '[a,e,c,d])+-- (f b) (f e)+-- @+--+-- The number of 'SubS' in the index essentially indicates the index to+-- edit at.+--+-- This is similar to 'rlensC' from /vinyl/, but is built explicitly and+-- inductively, instead of using typeclass magic.+recLens+ :: forall as bs x y g f. Functor f+ => Substitute as bs x y+ -> (g x -> f (g y))+ -> Rec g as+ -> f (Rec g bs)+recLens s0 f = go s0+ where+ go :: Substitute cs ds x y+ -> Rec g cs+ -> f (Rec g ds)+ go = \case+ SubZ -> \case+ x :& xs -> (:& xs) <$> f x+ SubS s -> \case+ x :& xs -> (x :&) <$> go s xs++-- | Substitute a value in a 'Rec' at a given position, indicated by the+-- 'Substitute'. This is essentially a specialized version of 'recLens'.+substituteRec+ :: Substitute as bs x y+ -> (f x -> f y)+ -> Rec f as+ -> Rec f bs+substituteRec s f = runIdentity . recLens s (Identity . f)++-- | If you add an item to @as@ to create @bs@, you also need to shift an+-- @'Index' as y@ to @Index bs y@. This shifts the 'Index' in @as@ to+-- become an 'Index' in @bs@, but makes sure that the index points to the+-- same original value.+insertIndex :: Insert as bs x -> Index as y -> Index bs y+insertIndex = \case+ InsZ -> IS+ InsS ins -> \case+ IZ -> IZ+ IS i -> IS (insertIndex ins i)++-- | Used as the return type of 'deleteIndex'. An @'DeletedIx' bs x y@ is+-- like a @'Maybe' ('Index' bs y)@, except the 'Nothing' case witnesses+-- that @x ~ y@.+data DeletedIx :: [k] -> k -> k -> Type where+ GotDeleted :: DeletedIx bs x x+ NotDeleted :: Index bs y -> DeletedIx bs x y++deriving instance Show (DeletedIx bs x y)++-- | If you delete an item in @as@ to create @bs@, you also need to move+-- @'Index' as y@ into @Index bs y@. This transforms the 'Index' in @as@+-- to become an 'Index' in @bs@, making sure the index points to the same+-- original value.+--+-- However, there is a possibility that the deleted item is the item that+-- the index was originally pointing to. If this is the case, this+-- function returns 'GotDeleted', a witness that @x ~ y@. Otherwise, it+-- returns 'NotDeleted' with the unshifted index.+deleteIndex :: Delete as bs x -> Index as y -> DeletedIx bs x y+deleteIndex = \case+ DelZ -> \case+ IZ -> GotDeleted+ IS i -> NotDeleted i+ DelS del -> \case+ IZ -> NotDeleted IZ+ IS i -> case deleteIndex del i of+ GotDeleted -> GotDeleted+ NotDeleted j -> NotDeleted (IS j)++-- | A version of 'deleteIndex' returning a simple 'Maybe'. This can be+-- used if you don't care about witnessing that @x ~ y@ in the case that+-- the index is the item that is deleted.+deleteIndex_ :: Delete as bs x -> Index as y -> Maybe (Index bs y)+deleteIndex_ del i = case deleteIndex del i of+ GotDeleted -> Nothing+ NotDeleted j -> Just j++-- | Used as the return type of 'substituteIndex'. An @'SubstitutedIx' bs x y z@ is+-- like an @'Either' ('Index' bs y) ('Index' bs z)@, except the 'Left' case+-- witnesses that @x ~ z@.+data SubstitutedIx :: [k] -> k -> k -> k -> Type where+ GotSubbed :: Index bs y -> SubstitutedIx bs z y z+ NotSubbed :: Index bs z -> SubstitutedIx bs x y z++-- | If you substitute an item in @as@ to create @bs@, you also need to+-- reshift @'Index' as z@ into @'Index' bs z@. This reshifts the 'Index'+-- in @as@ to become an 'Index' in @bs@, making sure the index points to+-- the same original value.+--+-- However, there is a possibility that the substituted item is the item+-- that the index was originally pointing to. If this is the case, this+-- function returns 'GotSubbed', a witness that @x ~ z@. Otherwise, it+-- returns 'NotSubbed'. Both contain the updated index.+substituteIndex+ :: Substitute as bs x y+ -> Index as z+ -> SubstitutedIx bs x y z+substituteIndex = \case+ SubZ -> \case+ IZ -> GotSubbed IZ+ IS i -> NotSubbed (IS i)+ SubS s -> \case+ IZ -> NotSubbed IZ+ IS i -> case substituteIndex s i of+ GotSubbed j -> GotSubbed (IS j)+ NotSubbed j -> NotSubbed (IS j)++-- | A version of 'substituteIndex' returning a simple 'Either'. This can be+-- the case if you don't care about witnessing @x ~ z@ in the case that the+-- index is the item that was substituted.+substituteIndex_+ :: Substitute as bs x y+ -> Index as z+ -> Either (Index bs y) (Index bs z)+substituteIndex_ sub i = case substituteIndex sub i of+ GotSubbed j -> Left j+ NotSubbed j -> Right j++-- | Given an 'Index' pointing to an element, create a 'Delete'+-- corresponding to the given item. The type of the resulting list is+-- existentially quantified, is guaranteed to be just exactly the original+-- list minus the specified element.+withDelete+ :: Index as x+ -> (forall bs. Delete as bs x -> r)+ -> r+withDelete = \case+ IZ -> \f -> f DelZ+ IS i -> \f -> withDelete i (f . DelS)++-- | Given an 'Index' pointing to an element, create an 'Insert' placing an+-- item /directly before/ the given element. The type is existentailly+-- quantified.+withInsert+ :: Index as x+ -> (forall bs. Insert as bs y -> r)+ -> r+withInsert = \case+ IZ -> \f -> f InsZ+ IS i -> \f -> withInsert i (f . InsS)++-- | Given an 'Index' pointing to an element, create an 'Insert' placing an+-- item /directly after/ the given element. The type is existentailly+-- quantified.+withInsertAfter+ :: Index as x+ -> (forall bs. Insert as bs y -> r)+ -> r+withInsertAfter = \case+ IZ -> \f -> f (InsS InsZ)+ IS i -> \f -> withInsertAfter i (f . InsS)++-- | Type-level version of 'insertIndex'. Because of how GADTs and type+-- families interact, the type-level lists and kinds of the insertion and+-- index must be provided.+type family InsertIndex as bs x y (ins :: Insert as bs x) (i :: Index as y) :: Index bs y where+ InsertIndex as (x ': as) x y 'InsZ i = 'IS i+ InsertIndex (y ': as) (y ': bs) x y ('InsS ins) 'IZ = 'IZ+ InsertIndex (a ': as) (a ': bs) x y ('InsS ins) ('IS i) = 'IS (InsertIndex as bs x y ins i)++-- | Defunctionalization symbol for 'InsertIndex', expecting only the kind+-- variables.+data InsertIndexSym0 as bs x y :: Insert as bs x ~> Index as y ~> Index bs y++-- | Defunctionalization symbol for 'InsertIndex', expecting the 'Insert'+-- along with the kind variables.+data InsertIndexSym as bs x y :: Insert as bs x -> Index as y ~> Index bs y++type instance Apply (InsertIndexSym0 as bs x y) ins = InsertIndexSym as bs x y ins+type instance Apply (InsertIndexSym as bs x y ins) i = InsertIndex as bs x y ins i++-- | Singleton witness for 'InsertIndex'.+sInsertIndex+ :: SInsert as bs x ins+ -> SIndex as y i+ -> SIndex bs y (InsertIndex as bs x y ins i)+sInsertIndex = \case+ SInsZ -> SIS+ SInsS ins -> \case+ SIZ -> SIZ+ SIS i -> SIS (sInsertIndex ins i)++-- | Helper type family for the implementation of 'DeleteIndex', to get+-- around the lack of case statements at the type level.+type family SuccDeletedIx b bs x y (del :: DeletedIx bs x y) :: DeletedIx (b ': bs) x y where+ SuccDeletedIx b bs x x 'GotDeleted = 'GotDeleted+ SuccDeletedIx b bs x y ('NotDeleted i) = 'NotDeleted ('IS i)++-- | Type-level version of 'deleteIndex'. Because of how GADTs and type+-- families interact, the type-level lists and kinds of the insertion and+-- index must be provided.+type family DeleteIndex as bs x y (del :: Delete as bs x) (i :: Index as y) :: DeletedIx bs x y where+ DeleteIndex (x ': bs) bs x x 'DelZ 'IZ = 'GotDeleted+ DeleteIndex (x ': bs) bs x y 'DelZ ('IS i) = 'NotDeleted i+ DeleteIndex (y ': as) (y ': bs) x y ('DelS del) 'IZ = 'NotDeleted 'IZ+ DeleteIndex (b ': as) (b ': bs) x y ('DelS del) ('IS i) = SuccDeletedIx b bs x y (DeleteIndex as bs x y del i)++-- | Defunctionalization symbol for 'DeleteIndex', expecting only the kind+-- variables.+data DeleteIndexSym0 as bs x y :: Delete as bs x ~> Index as y ~> DeletedIx bs x y++-- | Defunctionalization symbol for 'DeleteIndex', expecting the 'Delete'+-- along with the kind variables.+data DeleteIndexSym as bs x y :: Delete as bs x -> Index as y ~> DeletedIx bs x y++type instance Apply (DeleteIndexSym0 as bs x y) del = DeleteIndexSym as bs x y del+type instance Apply (DeleteIndexSym as bs x y del) i = DeleteIndex as bs x y del i++-- | Kind-indexed singleton for 'DeletedIx'.+data SDeletedIx bs x y :: DeletedIx bs x y -> Type where+ SGotDeleted :: SDeletedIx bs x x 'GotDeleted+ SNotDeleted :: SIndex bs y i -> SDeletedIx bs x y ('NotDeleted i)++-- | Singleton witness for 'DeleteIndex'.+sDeleteIndex+ :: SDelete as bs x del+ -> SIndex as y i+ -> SDeletedIx bs x y (DeleteIndex as bs x y del i)+sDeleteIndex = \case+ SDelZ -> \case+ SIZ -> SGotDeleted+ SIS i -> SNotDeleted i+ SDelS del -> \case+ SIZ -> SNotDeleted SIZ+ SIS i -> case sDeleteIndex del i of+ SGotDeleted -> SGotDeleted+ SNotDeleted j -> SNotDeleted (SIS j)++-- | Helper type family for the implementation of 'SubstituteIndex', to get+-- around the lack of case statements at the type level.+type family SuccSubstitutedIx b bs x y z (s :: SubstitutedIx bs x y z) :: SubstitutedIx (b ': bs) x y z where+ SuccSubstitutedIx b bs x y x ('GotSubbed i) = 'GotSubbed ('IS i)+ SuccSubstitutedIx b bs x y z ('NotSubbed i) = 'NotSubbed ('IS i)++-- | Type-level version of 'subsituteIndex'. Because of how GADTs and type+-- families interact, the type-level lists and kinds of the insertion and+-- index must be provided.+type family SubstituteIndex as bs x y z (s :: Substitute as bs x y) (i :: Index as z) :: SubstitutedIx bs x y z where+ SubstituteIndex (z ': as) (y ': as) z y z 'SubZ 'IZ = 'GotSubbed 'IZ+ SubstituteIndex (x ': as) (y ': as) x y z 'SubZ ('IS i) = 'NotSubbed ('IS i)+ SubstituteIndex (z ': as) (z ': bs) x y z ('SubS s) 'IZ = 'NotSubbed 'IZ+ SubstituteIndex (b ': as) (b ': bs) x y z ('SubS s) ('IS i) = SuccSubstitutedIx b bs x y z (SubstituteIndex as bs x y z s i)++-- | Defunctionalization symbol for 'SubstituteIndex', expecting only the kind+-- variables.+data SubstituteIndexSym0 as bs x y z :: Substitute as bs x y ~> Index as z ~> SubstitutedIx bs x y z++-- | Defunctionalization symbol for 'SubstituteIndex', expecting the 'Substitute'+-- along with the kind variables.+data SubstituteIndexSym as bs x y z :: Substitute as bs x y -> Index as z ~> SubstitutedIx bs x y z++type instance Apply (SubstituteIndexSym0 as bs x y z) s = SubstituteIndexSym as bs x y z s+type instance Apply (SubstituteIndexSym as bs x y z s) i = SubstituteIndex as bs x y z s i++-- | Kind-indexed singleton for 'SubstitutedIx'.+data SSubstitutedIx bs x y z :: SubstitutedIx bs x y z -> Type where+ SGotSubbed :: SIndex bs y i -> SSubstitutedIx bs z y z ('GotSubbed i)+ SNotSubbed :: SIndex bs z i -> SSubstitutedIx bs x y z ('NotSubbed i)++-- | Singleton witness for 'SubstituteIndex'.+sSubstituteIndex+ :: SSubstitute as bs x y s+ -> SIndex as z i+ -> SSubstitutedIx bs x y z (SubstituteIndex as bs x y z s i)+sSubstituteIndex = \case+ SSubZ -> \case+ SIZ -> SGotSubbed SIZ+ SIS i -> SNotSubbed (SIS i)+ SSubS s -> \case+ SIZ -> SNotSubbed SIZ+ SIS i -> case sSubstituteIndex s i of+ SGotSubbed j -> SGotSubbed (SIS j)+ SNotSubbed j -> SNotSubbed (SIS j)
+ src/Data/Type/List/Sublist.hs view
@@ -0,0 +1,304 @@+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}++-- |+-- Module : Data.Type.List.Sublist+-- Copyright : (c) Justin Le 2018+-- License : BSD3+--+-- Maintainer : justin@jle.im+-- Stability : experimental+-- Portability : non-portable+--+-- Witnesses regarding sublists of lists.+module Data.Type.List.Sublist (+ -- * Prefix and Suffix+ -- ** Prefix+ Prefix(..)+ , takeRec, prefixLens, takeIndex, weakenIndex+ -- ** Suffix+ , Suffix(..)+ , dropRec, suffixLens, dropIndex, shiftIndex+ -- * Append+ , Append(..)+ , prefixToAppend, suffixToAppend+ , appendToPrefix, appendToSuffix, splitAppend+ -- ** Recuct+ , splitRec, appendRec, splitRecIso+ -- ** Index+ , splitIndex+ ) where++import Control.Applicative+import Data.Bifunctor+import Data.Kind+import Data.Profunctor+import Data.Type.Universe+import Data.Vinyl.Core++-- | A @'Prefix' as bs@ witnesses that @as@ is a prefix of @bs@.+--+-- Some examples:+--+-- @+-- PreZ :: Prefix '[] '[1,2,3]+-- PreS PreZ :: Prefix '[1] '[1,2,3]+-- PreS (PreS PreZ) :: Prefix '[1,2] '[1,2,3]+-- PreS (PreS (PreS PreZ)) :: Prefix '[1,2,3] '[1,2,3]+-- @+--+-- Rule of thumb for construction: the number of 'PreS' is the number of+-- items in the prefix.+--+-- This is essentially the first half of an 'Append', but is conceptually+-- easier to work with.+data Prefix :: [k] -> [k] -> Type where+ PreZ :: Prefix '[] as+ PreS :: Prefix as bs -> Prefix (a ': as) (a ': bs)++deriving instance Show (Prefix as bs)++-- | A lens into the prefix of a 'Rec'.+--+-- Read this type signature as:+--+-- @+-- 'prefixLens'+-- :: Prefix as bs+-- -> Lens' (Rec f bs) (Rec f as)+-- @+prefixLens+ :: forall as bs g f. Functor f+ => Prefix as bs+ -> (Rec g as -> f (Rec g as))+ -> Rec g bs+ -> f (Rec g bs)+prefixLens p = prefixToAppend p $ \a -> splitRecIso a . _1+ where+ _1 :: (a -> f b) -> (a, c) -> f (b, c)+ _1 f (x, y) = (, y) <$> f x++-- | Take items from a 'Rec' corresponding to a given 'Prefix'.+takeRec :: Prefix as bs -> Rec f bs -> Rec f as+takeRec p = getConst . prefixLens p Const++-- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@.+--+-- Some examples:+--+-- @+-- SufZ :: Suffix '[1,2,3] '[1,2,3]+-- SufS SufZ :: Suffix '[2,3] '[1,2,3]+-- SufS (SufS SufZ) :: Suffix '[3] '[1,2,3]+-- SufS (SufS (SufS SufZ)) :: Suffix '[] '[1,2,3]+-- @+--+-- Rule of thumb for construction: the number of 'SufS' is the number of+-- items to "drop" before getting the suffix.+--+-- This is essentially the second half of an 'Append', but is conceptually+-- easier to work with.+data Suffix :: [k] -> [k] -> Type where+ SufZ :: Suffix as as+ SufS :: Suffix as bs -> Suffix as (b ': bs)++deriving instance Show (Suffix as bs)++-- | A lens into the suffix of a 'Rec'.+--+-- Read this type signature as:+--+-- @+-- 'suffixLens'+-- :: Suffix as bs+-- -> Lens' (Rec f bs) (Rec f as)+-- @+suffixLens+ :: forall as bs g f. Functor f+ => Suffix as bs+ -> (Rec g as -> f (Rec g as))+ -> Rec g bs+ -> f (Rec g bs)+suffixLens p = suffixToAppend p $ \a -> splitRecIso a . _2+ where+ _2 :: (a -> f b) -> (c, a) -> f (c, b)+ _2 f (x, y) = (x ,) <$> f y++-- | Drop items from a 'Rec' corresponding to a given 'Suffix'.+dropRec :: Suffix as bs -> Rec f bs -> Rec f as+dropRec p = getConst . suffixLens p Const++-- | An @'Append' as bs cs@ witnesses that @cs@ is the result of appending+-- @as@ and @bs@.+--+-- Some examples:+--+-- @+-- AppZ :: Append '[] '[1,2] '[1,2]+-- AppZ :: Append '[] '[1,2,3] '[1,2,3]+-- AppS AppZ :: Append '[0] '[1,2] '[0,1,2]+-- @+--+-- Rule of thumb for construction: the number of 'AppS' is the number of+-- items in the /first/ list.+--+-- This basically combines 'Prefix' and 'Suffix'.+data Append :: [k] -> [k] -> [k] -> Type where+ AppZ :: Append '[] as as+ AppS :: Append as bs cs -> Append (a ': as) bs (a ': cs)++deriving instance Show (Append as bs cs)++-- | Witness an isomorphism between 'Rec' and two parts that compose it.+--+-- Read this type signature as:+--+-- @+-- 'splitRecIso'+-- :: Append as bs cs+-- -> Iso (Rec f cs) (Rec f cs)+-- (Rec f as, Rec f bs) (Rec f as, Rec f bs)+-- @+--+-- This can be used with the combinators from the lens library.+--+-- The 'Append' tells the point to split the 'Rec' at.+splitRecIso+ :: (Profunctor p, Functor f)+ => Append as bs cs+ -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs))+ -> p (Rec g cs) (f (Rec g cs))+splitRecIso a = dimap (splitRec a) ((fmap . uncurry) (appendRec a))++-- | Split a 'Rec' into a prefix and suffix. Basically 'takeRec'+-- and 'dropRec' combined.+splitRec+ :: Append as bs cs+ -> Rec f cs+ -> (Rec f as, Rec f bs)+splitRec = \case+ AppZ -> (RNil,)+ AppS a -> \case+ x :& xs -> first (x :&) . splitRec a $ xs++-- | Append two 'Rec's together according to an 'Append'.+appendRec+ :: Append as bs cs+ -> Rec f as+ -> Rec f bs+ -> Rec f cs+appendRec = \case+ AppZ -> \_ -> id+ AppS a -> \case+ x :& xs -> (x :&) . appendRec a xs++-- | Convert a 'Prefix' to an 'Append', with an existential @bs@.+prefixToAppend+ :: Prefix as cs+ -> (forall bs. Append as bs cs -> r)+ -> r+prefixToAppend = \case+ PreZ -> ($ AppZ)+ PreS p -> \f -> prefixToAppend p (f . AppS)++-- | Convert a 'Suffix' to an 'Append', with an existential @as@.+suffixToAppend+ :: Suffix bs cs+ -> (forall as. Append as bs cs -> r)+ -> r+suffixToAppend = \case+ SufZ -> ($ AppZ)+ SufS s -> \f -> suffixToAppend s (f . AppS)++-- | Split an 'Append' into a 'Prefix' and 'Suffix'. Basically+-- 'appendToPrefix' and 'appendToSuffix' at the same time.+splitAppend+ :: Append as bs cs+ -> (Prefix as cs, Suffix bs cs)+splitAppend = \case+ AppZ -> (PreZ, SufZ)+ AppS a -> bimap PreS SufS . splitAppend $ a++-- | Convert an 'Append' to a 'Prefix', forgetting the suffix.+appendToPrefix :: Append as bs cs -> Prefix as cs+appendToPrefix = \case+ AppZ -> PreZ+ AppS a -> PreS . appendToPrefix $ a++-- | Convert an 'Append' to a 'Suffix', forgetting the prefix+appendToSuffix :: Append as bs cs -> Suffix bs cs+appendToSuffix = \case+ AppZ -> SufZ+ AppS a -> SufS . appendToSuffix $ a++-- | Split an 'Index' by an 'Append'. If the 'Index' was in the first part+-- of the list, it'll return 'Left'. If it was in the second part, it'll+-- return 'Right'.+--+-- This is essentially 'takeIndex' and 'dropIndex' at the same time.+splitIndex+ :: Append as bs cs+ -> Index cs x+ -> Either (Index as x) (Index bs x)+splitIndex = \case+ AppZ -> Right+ AppS a -> \case+ IZ -> Left IZ+ IS i -> first IS . splitIndex a $ i++-- | Shave off the final inhabitants of an 'Index', keeping only indices+-- a part of a given prefix. If the index is out of range, 'Nothing' will+-- be returned.+--+-- This is essentially 'splitIndex', but taking only 'Left' results.+takeIndex+ :: Prefix as bs+ -> Index bs x+ -> Maybe (Index as x)+takeIndex p i = prefixToAppend p $ either Just (const Nothing)+ . (`splitIndex` i)++-- | Shave off the initial inhabitants of an 'Index', keeping only indices+-- a part of a given suffix If the index is out of range, 'Nothing' will+-- be returned.+--+-- This is essentially 'splitIndex', but taking only 'Right' results.+dropIndex+ :: Suffix as bs+ -> Index bs x+ -> Maybe (Index as x)+dropIndex s i = suffixToAppend s $ either (const Nothing) Just+ . (`splitIndex` i)++-- | An index pointing to a given item in a prefix is also an index+-- pointing to the same item in the full list. This "weakens" the bounds+-- of an index, widening the list at the end but preserving the original+-- index. This is the inverse of 'takeIndex'.+weakenIndex+ :: Prefix as bs+ -> Index as x+ -> Index bs x+weakenIndex = \case+ PreZ -> \case {}+ PreS p -> \case+ IZ -> IZ+ IS i -> IS (weakenIndex p i)++-- | An index pointing to a given item in a suffix can be transformed into+-- an index pointing to the same item in the full list. This is the+-- inverse of 'dropIndex'.+shiftIndex+ :: Suffix as bs+ -> Index as x+ -> Index bs x+shiftIndex = \case+ SufZ -> id+ SufS s -> IS . shiftIndex s