diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,17 @@ Changelog ========= +Version 0.1.3.2 +--------------- + +*August 25, 2019* + + + +* Fixed overlapping instance issues resulting from ambiguities in `Auto` + instances for `Insert`, `Delete`, `Substitute`, `Suffix`, `Interleave`, and + `Subset`. + Version 0.1.3.1 --------------- diff --git a/list-witnesses.cabal b/list-witnesses.cabal --- a/list-witnesses.cabal +++ b/list-witnesses.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 4055090befaa2d0679560c0b267262ff97d3c618a1503a0e4d5497fdbf73242d +-- hash: b5cd1b4dd5aa9afa7ec4fbf2fbfb27e461d5361e5bd05a2edf0ad347669f5c77 name: list-witnesses -version: 0.1.3.1 +version: 0.1.3.2 synopsis: Witnesses for working with type-level lists description: Collection of assorted inductive witnesses and functions for working with type-level lists. diff --git a/src/Data/Type/List/Edit.hs b/src/Data/Type/List/Edit.hs --- a/src/Data/Type/List/Edit.hs +++ b/src/Data/Type/List/Edit.hs @@ -106,10 +106,11 @@ -- @since 0.1.2.0 type IsInsert as bs = TyPred (Insert as bs) +-- | Prefers the "earlier" insert if there is ambiguity instance Auto (IsInsert as (x ': as)) x where auto = InsZ -instance Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where +instance {-# INCOHERENT #-} Auto (IsInsert as bs) x => Auto (IsInsert (a ': as) (a ': bs)) x where auto = InsS (auto @_ @(IsInsert as bs) @x) instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInsert as bs) where @@ -184,6 +185,14 @@ -- | Automatically generate an 'Insert' if @as@, @bs@ and @x@ are known -- statically. -- +-- Prefers the earlier insertion if there is an ambiguity. +-- +-- @ +-- InsS InsZ :: Insert '[1,2] '[1,2,2] 2 +-- InsS (InsS InsZ) :: Insert '[1,2] '[1,2,2] 2 +-- autoInsert @'[1,2] @'[1,2,2] @2 == InsS InsZ +-- @ +-- -- @since 0.1.2.0 autoInsert :: forall as bs x. Auto (IsInsert as bs) x => Insert as bs x autoInsert = auto @_ @(IsInsert as bs) @x @@ -225,10 +234,11 @@ -- @since 0.1.2.0 type IsDelete as bs = TyPred (Delete as bs) +-- | Prefers the "earlier" delete if there is ambiguity instance Auto (IsDelete (x ': as) as) x where auto = DelZ -instance Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where +instance {-# INCOHERENT #-} Auto (IsDelete as bs) x => Auto (IsDelete (a ': as) (a ': bs)) x where auto = DelS (auto @_ @(IsDelete as bs) @x) instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsDelete as bs) where @@ -263,6 +273,14 @@ -- | Automatically generate an 'Delete' if @as@, @bs@ and @x@ are known -- statically. -- +-- Prefers the earlier deletion if there is an ambiguity. +-- +-- @ +-- DelS DelZ :: Delete '[1,2,2] '[1,2] 2 +-- DelS (DelS DelZ) :: Delete '[1,2,2] '[1,2] 2 +-- autoDelete @'[1,2,2] @'[1,2] @2 == DelS DelZ +-- @ +-- -- @since 0.1.2.0 autoDelete :: forall as bs x. Auto (IsDelete as bs) x => Delete as bs x autoDelete = auto @_ @(IsDelete as bs) @x @@ -306,17 +324,28 @@ instance Auto (IsSubstitute (x ': as) (y ': as) x) y where auto = SubZ +-- | Prefers the earlier subsitution if there is ambiguity. instance Auto (IsSubstitute as bs x) y => Auto (IsSubstitute (c ': as) (c ': bs) x) y where auto = SubS (auto @_ @(IsSubstitute as bs x) @y) +instance {-# INCOHERENT #-} Auto (IsSubstitute (x ': as) (x ': as) x) x where + auto = SubZ + -- | Automatically generate an 'Substitute' if @as@, @bs@, @x@, and @y@ are -- known statically. -- +-- Prefers the "earlier" substitution if there is an ambiguity +-- +-- @ +-- SubZ :: Substitute '[1,1] '[1,1] 1 1 +-- SubS SubZ :: Substitute '[1,1] '[1,1] 1 1 +-- autoSubstitute @'[1,1] @'[1,1] @1 @1 == SubZ +-- @ +-- -- @since 0.1.2.0 autoSubstitute :: forall as bs x y. Auto (IsSubstitute as bs x) y => Substitute as bs x y autoSubstitute = auto @_ @(IsSubstitute 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 @@ -341,7 +370,8 @@ -- | 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 +-- TODO: implement Wagner-Fischer or something similar 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 diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs --- a/src/Data/Type/List/Sublist.hs +++ b/src/Data/Type/List/Sublist.hs @@ -187,10 +187,13 @@ -- @since 0.1.2.0 type IsSuffix as = TyPred (Suffix as) -instance Auto (IsSuffix as) as where +instance Auto (IsSuffix '[]) '[] where auto = SufZ -instance Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where +instance {-# OVERLAPPABLE #-} Auto (IsSuffix (a ': as)) (a ': as) where + auto = SufZ + +instance {-# OVERLAPPABLE #-} Auto (IsSuffix as) bs => Auto (IsSuffix as) (b ': bs) where auto = SufS (auto @_ @(IsSuffix as) @bs) instance (SDecide k, SingI (as :: [k])) => Decidable (IsSuffix as) where @@ -603,10 +606,11 @@ instance Auto (IsInterleave '[] '[]) '[] where auto = IntZ +-- | Prefers 'IntL' if there is an ambiguity. instance Auto (IsInterleave as bs) cs => Auto (IsInterleave (a ': as) bs) (a ': cs) where auto = IntL (auto @_ @(IsInterleave as bs) @cs) -instance Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where +instance {-# INCOHERENT #-} Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs)) (b ': cs) where auto = IntR (auto @_ @(IsInterleave as bs) @cs) instance (SDecide k, SingI (as :: [k]), SingI bs) => Decidable (IsInterleave as bs) where @@ -658,9 +662,18 @@ IntL _ -> v Refl IntR _ -> u Refl --- | Automatically generate an 'Interleave' if @as@ and @bs@ are known --- statically. +-- | Automatically generate an 'Interleave' if @as@, @bs@, and @cs@ are +-- known statically. -- +-- Prefers the left side if there is an ambiguity: +-- +-- @ +-- IntL (IntR (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2] +-- IntR (IntL (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2] +-- +-- autoInterleave @'[1] @'[1,2] '[1,1,2] == IntL (IntR (IntR IntZ) +-- @ +-- -- @since 0.1.2.0 autoInterleave :: forall as bs cs. Auto (IsInterleave as bs) cs => Interleave as bs cs autoInterleave = auto @_ @(IsInterleave as bs) @cs @@ -873,10 +886,10 @@ instance Auto (IsSubset '[]) '[] where auto = SubsetNil -instance Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where +instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where auto = SubsetNo (auto @_ @(IsSubset as) @bs) -instance Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where +instance {-# OVERLAPPING #-} Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where auto = SubsetYes (auto @_ @(IsSubset as) @bs) instance (SDecide k, SingI (as :: [k])) => Decidable (IsSubset as) where