diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,12 @@ +Changelog +========= + +Version 0.1.0.0 +--------------- + +*March 6, 2019* + + + +* Initial release + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,12 @@ +[list-witnesses][docs] +====================== + +[![list-witnesses on Hackage](https://img.shields.io/hackage/v/list-witnesses.svg?maxAge=86400)](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. 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/list-witnesses.cabal b/list-witnesses.cabal new file mode 100644 --- /dev/null +++ b/list-witnesses.cabal @@ -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 diff --git a/src/Data/Type/List/Edit.hs b/src/Data/Type/List/Edit.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/Edit.hs @@ -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) diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List/Sublist.hs @@ -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