diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for coerce-with-substitution + +## 0.0.0.0 -- 2025-07-21 + +* Proof of concept release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +Copyright (c) 2025, Ryan Hendrickson + + +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 the copyright holder nor the names of its + 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 +HOLDER 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/coerce-with-substitution.cabal b/coerce-with-substitution.cabal new file mode 100644 --- /dev/null +++ b/coerce-with-substitution.cabal @@ -0,0 +1,60 @@ +cabal-version: 3.4 +name: coerce-with-substitution +version: 0.0.0.0 +synopsis: Coercions with improved type inference +description: + This package defines aliases of 'Data.Coerce.coerce' and + 'Unsafe.Coerce.unsafeCoerce' that accept a type argument containing type + substitutions, creating a relationship between the argument and result + types of the coercion that GHC can use when inferring one type from the + other. + + See "Data.CoerceSubst" for a full introduction to this package. + + Requires GHC 9.6 or later, due to use of the + [`TypeData`](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_data.html) + extension. +license: BSD-3-Clause +license-file: LICENSE +author: Ryan Hendrickson +maintainer: contact-project+rhendric-haskell-coerce-with-substitution-71023049-issue-@incoming.gitlab.com +homepage: https://gitlab.com/rhendric/haskell-coerce-with-substitution +bug-reports: https://gitlab.com/rhendric/haskell-coerce-with-substitution/-/issues +copyright: © 2025 Ryan Hendrickson +category: Development +build-type: Simple +extra-doc-files: CHANGELOG.md +tested-with: GHC == { 9.12.2, 9.10.2, 9.8.4, 9.6.7, 9.6.1 } + +source-repository head + type: git + location: https://gitlab.com/rhendric/haskell-coerce-with-substitution.git + +library + hs-source-dirs: src + exposed-modules: Data.CoerceSubst + build-depends: base >=4.7 && <5 + ghc-options: + -fprint-unicode-syntax + -haddock + -Wall + -Wcompat + -Winvalid-haddock + -Wmissing-export-lists + -Woperator-whitespace + -Wunused-packages + -Wunused-type-patterns + if impl(ghc >= 9.10.1) + ghc-options: + -Wmissing-poly-kind-signatures + default-language: GHC2021 + default-extensions: + AllowAmbiguousTypes, + DataKinds, + FunctionalDependencies, + NoImplicitPrelude, + NoStarIsType, + TypeData, + TypeFamilies, + UndecidableInstances, + UnicodeSyntax, diff --git a/src/Data/CoerceSubst.hs b/src/Data/CoerceSubst.hs new file mode 100644 --- /dev/null +++ b/src/Data/CoerceSubst.hs @@ -0,0 +1,719 @@ +{-# LANGUAGE CPP #-} +{-# OPTIONS_HADDOCK redact-type-synonyms #-} +-- | +-- Copyright: © 2025 Ryan Hendrickson +-- License: BSD-3-Clause +-- +-- This module exposes two functions, 'coerceSubst' and 'unsafeCoerceSubst', +-- which are aliases for 'coerce' and 'unsafeCoerce' respectively. Use these +-- functions to help guide type inference for the types you are coercing. +-- +module Data.CoerceSubst ( + -- * Motivation + + -- $motivation + + -- * Reference + coerceSubst, + -- $basicRef + type (↦), (:\), (:/), + -- $injectiveIntroduction + type (↦!), (:\!), (:/!), + -- $injectiveRef + + -- ** Advanced usage + -- $advancedRef + + -- *** @To@ and @Un@ + -- $asUnIntroduction + To, Un, ToI, UnI, + -- $polymorphicToUn + To_, Un_, ToI_, UnI_, + + -- *** @Within@ + -- $withinIntroduction + Within, + -- $withinRef + + -- ** Unsafe + unsafeCoerceSubst, + -- $unsafeRef + + -- ** Auxiliary types + Subst, + Substitute, +) where + +import Data.Bool (Bool(..)) +import Data.Coerce (Coercible, coerce) +import Data.Kind (Constraint) +import Data.Type.Equality (type (~)) +import GHC.List (List) +import GHC.TypeLits (type (-)) +import Numeric.Natural (Natural) +import Unsafe.Coerce (unsafeCoerce) + +#ifdef DOCTEST +import Prelude + +import Control.Applicative (Const(..), ZipList(..)) +import Data.Kind (Type) +import Data.Ord (Down(..)) +#endif + + +infix 6 ↦, :\, :/, ↦!, :\!, :/! + +-- $setup +-- +-- >>> :set -XQuantifiedConstraints +-- >>> :{ +-- >>> -- (This omits features irrelevant to the demonstration.) +-- >>> class Constrained (f :: Type -> Type) where +-- >>> type Dom f (a :: Type) :: Constraint +-- >>> type Dom f a = () +-- >>> class Constrained f => CFunctor f +-- >>> class CFunctor m => CBind m where +-- >>> (>>-) :: (Dom m a, Dom m b) => m a -> (a -> m b) -> m b +-- >>> newtype WrapFunctor f (a :: Type) = WrapFunctor {runFunctor :: f a} +-- >>> instance Constrained (WrapFunctor f) where +-- >>> type Dom (WrapFunctor f) a = () +-- >>> instance Functor f => CFunctor (WrapFunctor f) +-- >>> :} + +-- $motivation +-- +-- The type signature of 'coerce' does nothing to relate the argument and +-- result types to each other. If both types are already known to the compiler, +-- this is fine: +-- +-- > coerceMaybe ∷ Maybe A → Maybe B +-- > coerceMaybe = coerce +-- +-- But if you are leaning on the compiler to infer one or both types, using +-- 'coerce' to greatest effect can be frustrating. Take +-- [this](/package/subcategories-0.2.1.1/docs/src/Control.Subcategory.Bind.html#line-37) +-- example from the @subcategories@ package: +-- +-- > instance (Monad m) => CBind (WrapFunctor m) where +-- > (>>-) :: forall a b. +-- > WrapFunctor m a +-- > -> (a -> WrapFunctor m b) -> WrapFunctor m b +-- > (>>-) = coerce @(m a -> (a -> m b) -> m b) (>>=) +-- +-- All that type information is there because 'coerce' does nothing to relate +-- the type of @(>>=)@ to the expected type of @(>>-)@. But the only piece of +-- information that the compiler is missing is that the result of the coercion +-- is the type of @(>>=)@, but with @m@ replaced by @WrapFunctor m@. +-- +-- 'coerceSubst' allows for that information to be encoded directly, with less +-- ceremony and more clarity: +-- +-- >>> :{ +-- >>> instance (Monad m) => CBind (WrapFunctor m) where +-- >>> (>>-) = coerceSubst @'[m ↦! WrapFunctor m] (>>=) +-- >>> :} + +-- $basicRef +-- +-- The first type argument to 'coerceSubst' is a list of substitutions. Simple +-- substitutions can be written as @original '↦' replacement@. +-- +-- >>> coerceSubst @'[Bool ↦ Down Bool] (True, False, 'x') +-- (Down True,Down False,'x') +-- +-- For the Unicode-averse, two alternate spellings are provided: +-- +-- * @replacement ':/' original@ is inspired by the other notation frequently +-- used for substitutions (\(M[N/x]\), in which free occurrences of \(x\) +-- in \(M\) are to be replaced with \(N\)). +-- * @original ':\' replacement@ mirrors the above to match the left-to-right +-- order of '↦'. +-- +-- >>> coerceSubst @'[Bool :\ Down Bool] (True, False, 'x') +-- (Down True,Down False,'x') +-- +-- (I couldn't make up my mind which is best so you get all three.) + +-- $injectiveIntroduction +-- +-- However it is written, the effect of a substitution is to start with the +-- type of the argument of 'coerceSubst', and replace every occurrence of the +-- ‘original’ type with the ‘replacement’ type. The result is the type of the +-- result of 'coerceSubst'. +-- +-- This presumes that the type of the argument is known, and the type of the +-- result is to be inferred. Sometimes, the opposite is the case. For such +-- cases, a substitution operator can be marked as /injective/ with a @!@ +-- character. An injective substitution will additionally look for occurrences +-- of the /replacement/ type in the type of the /result/, and +-- reverse-substitute them into the argument type. + +-- $injectiveRef +-- +-- An example of this was shown in the Motivation section, above. Without the +-- injectivity marker, GHC would not infer that the @(>>=)@ operator is to be +-- instantiated at the type @m@. With it, GHC can infer this by working +-- backwards from the occurrences of @WrapFunctor m@ in the expected type of +-- @(>>-)@. +-- +-- (Not all substitutions should be injective! You may want to coerce multiple +-- types to the same ‘replacement’ type, or there may be existing occurrences +-- of a ‘replacement’ type in the input.) + +-- $advancedRef +-- +-- Substitutions that match a whole type take precedence over substitutions +-- that match a part of a type. In this next example, see how the @Const Bool +-- Int@ value is not translated by the first substitution into a @Const (Down +-- Bool) Int@, because the second substitution takes precedence. +-- +-- >>> coerceSubst @[Bool ↦ Down Bool, Const Bool Int ↦ Bool] (True, Const @_ @Int False) +-- (Down True,False) +-- +-- (Aside: the @'@ character that appeared in the examples before this one is +-- for +-- [distinguishing](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/data_kinds.html#distinguishing-between-types-and-constructors) +-- between @[a]@, a list with @a@ as its single element, and @[a]@, the type of +-- lists of @a@. It is optional if you compile with +-- [@NoListTuplePuns@](https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/data_kinds.html#unique-syntax-for-type-level-lists-and-tuples), +-- or if the list of substitutions has more than one element, as in this most +-- recent example.) +-- +-- This behavior can be used to ‘protect’ a type from another substitution via +-- an identity substitution. In this example, 'Data.String.String' is a +-- specific kind of 'List' that we don't want to become a +-- 'Control.Applicative.ZipList'. +-- +-- >>> coerceSubst @[String ↦ String, [] ↦ ZipList] ("hello", [True]) +-- ("hello",ZipList {getZipList = [True]}) +-- +-- Once part of a type has been substituted, that part is not considered for +-- any further substitutions. In other words, multiple substitutions can be +-- thought of as executed in parallel, not in sequence. +-- +-- >>> coerceSubst @[Bool ↦ Down Bool, Down Bool ↦ Bool] (True, Down False) +-- (Down True,False) +-- +-- If two substitutions have the same ‘original’ type, the earlier substitution +-- takes precedence. +-- +-- >>> coerceSubst @[Bool ↦ Down Bool, Bool ↦ Const Bool Int] True +-- Down True +-- +-- Likewise if two injective substitutions have the same ‘replacement’ type. +-- +-- >>> coerceSubst @[Down Bool ↦! Bool, Const Bool Int ↦! Bool] (read "Down True") ∷ Bool +-- True +-- >>> coerceSubst @[Down Bool ↦! Bool, Const Bool Int ↦! Bool] (read "Const True") ∷ Bool +-- *** Exception: Prelude.read: no parse +-- +-- Order in a substitution list doesn't matter otherwise. +-- +-- (This is little more than a curiosity with only simple substitutions, but +-- will become more relevant when 'Within' substitutions are introduced.) +-- +-- Finally, a known limitation: A polykinded type can't be substituted in its +-- general form; it must be instantiated at each kind for which it is used. (If +-- only one side of the substitution is polykinded, you won't need to worry +-- about this, as the kind of '(↦)' ensures that both operands have the same +-- kind.) + +-- $asUnIntroduction +-- +-- A very common case for coercions is wrapping and unwrapping newtypes. It +-- isn't terribly burdensome to write these out as substitutions in some cases +-- (@Bool '↦' Down Bool@, as an example we have seen several times already). +-- However, you may not want to write out @(Int, String, Bool) '↦' Down (Int, +-- String, Bool)@ in full, with a complex type repeated unnecessarily. Some +-- newtypes use their type parameters multiple times, increasing the +-- duplication. +-- +-- For such cases, this module offers the following convenience types. + +-- $polymorphicToUn +-- +-- The above conveniences work for 'Data.Kind.Type'-kinded substitutions. +-- Function-kinded substitutions, which replace type constructors instead of +-- ground types, can also be expressed with a similar shorthand. +-- +-- As a demonstration, the example given in the Motivation section used the +-- substitution @m '↦!' WrapFunctor m@. @WrapFunctor@ is a newtype, but we +-- can't use 'ToI' with this wrapping operation because @m@ and @WrapFunctor m@ +-- are function-kinded. But we can use the polymorphic version, 'ToI_', +-- providing (as a ‘subscript’) the number of parameters over which to be +-- polymorphic. +-- +-- >>> :{ +-- >>> instance (Monad m) => CBind (WrapFunctor m) where +-- >>> (>>-) = coerceSubst @'[ToI_ 1 ('WrapFunctor @m)] (>>=) +-- >>> :} +-- +-- As in the 'Data.Kind.Type'-kinded case, this is exactly equivalent to @m +-- '↦!' WrapFunctor m@, and in such a simple case one is likely to prefer to +-- write @m@ twice instead of using this more advanced (and longer!) +-- ‘shorthand’. +-- +-- Note that while @WrapFunctor@ has two type parameters, since the last one is +-- being abstracted away, only the @\@m@ needs to be written out. In general, +-- if \(n\) is the subscript, you shouldn't need to explicitly instantiate the +-- last \(n\) type parameters. (If you do, they are ignored.) + +-- $withinIntroduction +-- +-- In more complex scenarios, you may not want to substitute everywhere inside +-- a type. The 'Within' combinator allows some substitutions to be active only +-- in the arguments to a provided type constructor, which acts as a selector. +-- +-- >>> x = (True, Left False ∷ Either Bool Int) +-- >>> coerceSubst @'[Within Either '[Bool ↦ Down Bool]] x +-- (True,Left (Down False)) + +-- $withinRef +-- +-- A 'Within' combinator, when active, behaves as if expanded to its contents +-- in place. For example, any substitutions that follow the 'Within' will be +-- considered after the contents of the 'Within'. In this next example, because +-- the 'Within' precedes the @Bool '↦' Const Bool Int@ substitution, the @Bool +-- '↦' Down Bool@ substitution takes precedence inside the pair, while the +-- @Bool '↦' Const Bool Int@ has an effect outside of it. +-- +-- >>> x = (False, ([True], [True]), [False]) +-- >>> coerceSubst @[Within (,) '[Bool ↦ Down Bool], Bool ↦ Const Bool Int] x +-- (Const False,([Down True],[Down True]),[Const False]) +-- +-- The 'Within' would not have any effect in the opposite order. +-- +-- >>> x = (False, ([True], [True]), [False]) +-- >>> coerceSubst @[Bool ↦ Down Bool, Within (,) '[Bool ↦ Const Bool Int]] x +-- (Down False,([Down True],[Down True]),[Down False]) +-- +-- The selector of a 'Within' can be any type-level expression, including +-- compounds formed by applying a constructor to other type expressions, but +-- keep in mind that the effect of the 'Within' is on the selector's arguments, +-- not types in the selector itself. Notice how in this example, the selector +-- @(,) Bool@ causes the payload of the 'Within' to apply to the second element +-- of the pair, but not the first. +-- +-- >>> coerceSubst @'[Within ((,) Bool) '[Bool ↦ Down Bool]] (False, True) +-- (False,Down True) +-- +-- The type of the pair is @(,) Bool Bool@, and only the second @Bool@ is in +-- the argument of the selector @(,) Bool@. The first @Bool@ is /part/ of the +-- selector. +-- +-- You can even use type parameters as 'Within' selectors, though in such +-- circumstances you will need to ensure that the relevant 'Coercible' +-- instances are available. +-- +-- >>> :{ +-- >>> example ∷ ∀ f g a. +-- >>> (∀ b b'. Coercible b b' ⇒ Coercible (f (g b)) (f (g b'))) ⇒ +-- >>> Show (a, f (g (Down a))) ⇒ +-- >>> (a, f (g a)) → +-- >>> String +-- >>> example = show . coerceSubst @'[Within g '[a ↦ Down a]] +-- >>> :} +-- +-- 'Within' selectors are always matched against the argument type, even if the +-- selector is also substituted to another type constructor. +-- +-- >>> coerceSubst @'[Within [] '[Bool ↦ Down Bool], [] ↦ ZipList] (False, [True]) +-- (False,ZipList {getZipList = [Down True]}) +-- +-- This remains the case even when injective substitutions are used; the 'Within' +-- matches the argument type, even though an injective substitution could cause +-- inference of the argument type to be driven by the result type. +-- +-- >>> :{ +-- >>> coerceSubst @'[Within [] '[Bool ↦! Down Bool], [] ↦! ZipList] +-- >>> (read "(False, [True])") +-- >>> ∷ (Bool, ZipList (Down Bool)) +-- >>> :} +-- (False,ZipList {getZipList = [Down True]}) +-- +-- 'Within's can be nested, resulting in substitutions that will take effect +-- only if multiple selectors are matched in the correct order. +-- +-- >>> x = ([(True, True)], ([False], [False]), ()) +-- >>> coerceSubst @'[Within [] '[Within (,) '[Bool ↦ Down Bool]]] x +-- ([(Down True,Down True)],([False],[False]),()) + +-- $unsafeRef +-- +-- All of the above applies equally to 'unsafeCoerceSubst' (except for +-- requiring 'Coercible' instances), though with this function you gain the +-- ability to do less safe things, like coercing through an unknown +-- 'Data.Functor.Functor'. +-- +-- >>> caution = unsafeCoerceSubst @'[Bool ↦ Down Bool] . fmap even +-- >>> :t caution +-- caution ∷ (Functor f', Integral a) ⇒ f' a → f' (Down Bool) +-- >>> caution [3..5] -- not so dangerous on lists! +-- [Down False,Down True,Down False] + +-- | The kind of an element in the type substitution DSL. +-- +-- To make 'Subst's, see '(↦)', '(:\)', '(:/)', '(↦!)', '(:\!)', '(:/!)', 'To', +-- 'Un', 'ToI', 'UnI', 'To_', 'Un_', 'ToI_', 'UnI_', and 'Within'. +type data Subst + = ∀ k. k :\ k + -- ^ An alternate spelling of '↦', representing a substitution replacing + -- the left operand with the right. + + | ∀ k. k :\! k + -- ^ An alternate spelling of '↦!', representing an injective substitution + -- replacing the left operand with the right. + + | ∀ k. Within k (List Subst) + -- ^ A list of substitutions scoped to take effect only within arguments to + -- the provided type expression. + +-- | A simple substitution, replacing the left operand with the right. +type (↦) ∷ ∀ k. k → k → Subst +type (↦) = (:\) + +-- | A simple injective substitution, replacing the left operand with the +-- right. +type (↦!) ∷ ∀ k. k → k → Subst +type (↦!) = (:\!) + +-- | A reversed spelling of '↦', representing a substitution replacing the +-- /right/ operand with the /left/. +type (:/) ∷ ∀ k. k → k → Subst +type a :/ b = b ↦ a + +-- | A reversed spelling of '↦!', representing a injective substitution +-- replacing the /right/ operand with the /left/. +type (:/!) ∷ ∀ k. k → k → Subst +type a :/! b = b ↦! a + +-- | An alias for 'coerce' that accepts a type-level list of type substitutions +-- to perform. As with 'coerce', the compiler will check that the argument and +-- result types are safely coercible using the 'Coercible' constraint, and the +-- coercion is free of cost at run time. +coerceSubst ∷ ∀ σ a b. Substitute σ a b ⇒ Coercible a b ⇒ a → b +coerceSubst = coerce +{-# INLINE coerceSubst #-} + +-- | Just like 'coerceSubst', but without the compiler-checked guarantee that +-- the argument and result types are safely coercible. +unsafeCoerceSubst ∷ ∀ σ a b. Substitute σ a b ⇒ a → b +unsafeCoerceSubst = unsafeCoerce +{-# INLINE unsafeCoerceSubst #-} + + +-- | As a shorthand for the common case of substituting a type with a newtype +-- that wraps it, you can write @'To' 'MkNewtype@. The argument to 'To' should +-- be the promoted data constructor for the newtype, not the newtype's type +-- constructor (in many cases, these names are punned, and the @'@ is necessary +-- to disambiguate them). +-- +-- If the constructor is polymorphic, you must instantiate all of its type +-- parameters, as in this example. +-- +-- >>> coerceSubst @'[To ('Down @(String, Bool))] (("a", True), ("b", False)) +-- (Down ("a",True),Down ("b",False)) +-- +-- This is a bit more concise than the equivalent @(String, Bool) '↦' Down +-- (String, Bool)@, but may look less natural. The trade-off is yours to make. +type To (_con ∷ a → b) = a ↦ b + +-- | Like 'To', but injective. +type ToI (_con ∷ a → b) = a ↦! b +-- $ +-- >>> f x = coerceSubst @'[ToI ('Down @(String, Bool))] x ∷ (Down (String, Bool), Bool) +-- >>> f $ read "((\"a\", True), False)" +-- (Down ("a",True),False) + +-- | Like 'To', but for unwrapping a newtype. +-- +-- >>> coerceSubst @'[Un ('Down @(String, Bool))] (Down ("a", True), Down ("b", False)) +-- (("a",True),("b",False)) +type Un (_con ∷ a → b) = b ↦ a + +-- | Like 'Un', but injective. +type UnI (_con ∷ a → b) = b ↦! a +-- $ +-- >>> f x = coerceSubst @'[UnI ('Down @(String, Bool))] x ∷ ((String, Bool), Bool) +-- >>> f $ read "(Down (\"a\", True), False)" +-- (("a",True),False) + +-- | A variant of 'To' for polymorphic substitution, accepting the number of +-- type arguments over which to abstract. @'To_' 0 'Con@ is equivalent to @'To' +-- 'Con@. +type To_ n (_con ∷ a → b) = MkTo_ False n a b +-- $ +-- >>> coerceSubst @'[To_ 1 'ZipList] ("a", ([True], False)) +-- (ZipList {getZipList = "a"},(ZipList {getZipList = [True]},False)) + +-- | Like 'To_', but injective. @'ToI_' 0 'Con@ is equivalent to @'ToI' 'Con@. +type ToI_ n (_con ∷ a → b) = MkTo_ True n a b +-- $ +-- >>> f x = coerceSubst @'[ToI_ 1 'ZipList] x ∷ (ZipList Char, (ZipList Bool, Bool)) +-- >>> f $ read "(\"a\", ([True], False))" +-- (ZipList {getZipList = "a"},(ZipList {getZipList = [True]},False)) + +-- | Like 'To_', but for unwrapping a newtype. @'Un_' 0 'Con@ is equivalent to +-- @'Un' 'Con@. +type Un_ n (_con ∷ a → b) = MkTo_ False n b a +-- $ +-- >>> coerceSubst @'[Un_ 1 'ZipList] (ZipList "a", (ZipList [True], False)) +-- ("a",([True],False)) + +-- | Like 'Un_', but injective. @'UnI_' 0 'Con@ is equivalent to @'UnI' 'Con@. +type UnI_ n (_con ∷ a → b) = MkTo_ True n b a +-- $ +-- >>> f x = coerceSubst @'[UnI_ 1 'ZipList] x ∷ (String, ([Bool], Bool)) +-- >>> f $ read "(ZipList {getZipList = \"a\"}, (ZipList {getZipList = [True]}, False))" +-- ("a",([True],False)) + +-- | The shared implementation of polymorphic 'To_', 'ToI_', 'Un_', and 'UnI_'. +type MkTo_ ∷ ∀ k. Bool → Natural → k → k → Subst +type family MkTo_ inj n a b where + MkTo_ False 0 a b = a ↦ b + MkTo_ True 0 a b = a ↦! b + MkTo_ inj n (f x) (g x) = MkTo_ inj (n - 1) f g + + +-- What follows is hideous, and I make no apologies for it. +-- +-- The type-level computation needed to perform substitutions is, when +-- distilled into a more familiar term-level pseudocode form, not very +-- complicated. +-- +-- > substitute ∷ ∀ k₀. List Subst → k₀ → k₀ → Constraint +-- > substitute σ₀ = go σ₀ +-- > where +-- > go ∷ ∀ k. List Subst → k → k → Constraint +-- > go = \cases +-- > (from ↦ to : _) arg res | from ~ arg → to ~ res +-- > (from ↦! to : _) arg res | from ~ arg → to ~ res +-- > | to ~ res → from ~ arg +-- > (_ : σ) arg res → go σ arg res +-- > [] (f a) res → ∃ f' a'. +-- > (substitute σ₀ f f', substitute (expand σ₀ f) a a', f' a' ~ res) +-- > [] arg (f b) → ∃ f' b'. +-- > (substitute σ₀ f' f, substitute (expand σ₀ f') b' b, arg ~ f' b') +-- > [] arg res → arg ~ res +-- > +-- > expand ∷ ∀ k₀. List Subst → k₀ → List Subst +-- > expand (Within w_f w_σ : σ) f₀ = doWithin f₀ +-- > where +-- > doWithin ∷ ∀ k. k → List Subst +-- > doWithin = \case +-- > f | w_f ~ f → w_σ ++ σ' +-- > (f _) → doWithin f +-- > _ → Within w_f w_σ : σ' +-- > σ' = expand σ f₀ +-- > expand (s : σ) f = s : expand σ f +-- > expand [] _ = [] +-- +-- As much as possible of the above has been translated into type families. One +-- might ask, why not all of it? To which I would reply, type families have no +-- ability to do incoherent matches, which would make this module unusable with +-- parameterized types. There are a few places in the above where I have +-- written pseudocode representing testing two types for equality, or +-- decomposing a type into an @f a@ application. One can encode these matches +-- with type families, but the resulting type gets stuck in cases like @IsEq a +-- Char@ (@IsEq@ being the notional type-family-based equality tester), because +-- the compiler will nobly insist on not telling us any convenient lies. (@a@ +-- /could/ be @Char@!) +-- +-- So instead I am incorporating incoherent instances with functional +-- dependencies, which enable a more allistic disposition on such questions as +-- whether @a@ and @Char@ are the same (‘shut up nerd, they aren't’). They are +-- also, sadly, much more verbose and difficult to write (not to mention read), +-- so rather than encode the entire type-level algorithm in class instances, I +-- have put the bulk of the pattern matching and control flow into a +-- 'Constraint'-kinded closed type family named, uncreatively, 'Eval', which +-- dispatches on a single 'Expr'. (‘Haskell is a dynamically-typed, interpreted +-- language,’ as Vidrun helpfully teaches us.) Returning a 'Constraint' allows +-- us to step outside the type family paradigm as needed by returning a real +-- class, but fortunately this isn't necessary very much: only for terminal +-- equalities ('(~)'), the incoherent-by-design instances ('KnownEq' and +-- 'KnownApp'), and a pair of auxiliary classes representing tuples of +-- constraints related by newly-introduced unknown type parameters +-- ('EvalSubstituteApp' and '(:&:)', of which the latter is more often invoked +-- through the '(:?:)' / '(:::)' ternary interface than directly). +-- +-- Note that having monolithic 'Expr' and 'Eval' instead of a number of smaller +-- type families is very useful, as it enables one set of generic operators to +-- be reused in different parts of the algorithm. They work by holding +-- partially-applied 'Expr' values instead of attempting to partially apply a +-- type family (which is illegal). + + +-- | An empty class witnessing a substitution relationship between two types. +type Substitute ∷ List Subst → k → k → Constraint +type Substitute σ a b = Eval (Substitute_go σ σ a b) + + +-- | A representation of work to be done while solving a 'Substitute' +-- constraint. Some of these constructors are ad-hoc for this application, and +-- some are generic combinators that save me from repeating the same pattern +-- multiple times. +-- +-- The choice of final argument is often significant, so that it can be used +-- with '(:&:)'. +type data Expr + -- | The worker function of 'Substitute'. + = ∀ k. Substitute_go + (List Subst) + -- ^ initial list of substitutions + (List Subst) + -- ^ substitutions still to be handled + k + -- ^ input type of the coercion + k + -- ^ result type of the coercion + + -- | Find any matching 'Within' substitutions and expand them in place. + | ∀ k. Expand + (List Subst) + -- ^ list of substitutions + k + -- ^ type to scrutinize for matching 'Within' fragments + (List Subst) + -- ^ expanded list + + -- | Helper function for expanding a single 'Within'. + | ∀ k₁ k₂. Expand_doWithin + (ExpandWithinEnv k₁) + k₂ + -- ^ type to scrutinize + (List Subst) + -- ^ a suffix of already-expanded substitutions to append to the result + + -- | Helper function for continuing a 'Within' expansion in an applied type. + | ∀ k₁ k₂. Expand_doWithinApp + (ExpandWithinEnv k₁) + k₂ + -- ^ type to scrutinize + (List Subst) + -- ^ a suffix of already-expanded substitutions to append to the result + + -- | Helper function for building a list. + | ∀ k. DoCons k {-^ head -} (List k) {-^ head : tail -} (List k) {-^ tail -} + + -- | Generic holder for a unary 'Constraint'-kinded function. + | ∀ k. Lift1 (k → Constraint) k + + -- | Generic holder for a pair of control branches. + | (:::) Constraint {-^ if true -} Constraint {-^ if false -} Bool + +type ExpandWithinEnv k = + ( k -- selector of the 'Within' + , List Subst -- payload of the 'Within' + , List Subst -- result of the expansion, starting with either this payload or + -- a re-wrapped 'Within' + ) + + +-- | Constraint-kinded ternary operator: @Condition :?: IfTrue ::: IfFalse@ +type (:?:) ∷ (Bool → Constraint) → (Bool → Expr) → Constraint +type (:?:) cond = (:&:) (Lift1 cond) +infixr 0 :?:, ::: + + +-- | Generic operator for cutting two 'Expr's with an unknown parameter to be +-- solved. A little bit like a symmetric type-level @$@ or @&@, but don't lean +-- on that too hard. +class (f ∷ k → Expr) :&: (g ∷ k → Expr) +instance (Eval (f a), Eval (g a)) ⇒ f :&: g + + +type family Eval (expr ∷ Expr) ∷ Constraint where + Eval (Substitute_go σ₀ (from ↦ to : σ) arg res) = + from `KnownEq` arg :?: to ~ res ::: Eval (Substitute_go σ₀ σ arg res) + + Eval (Substitute_go σ₀ (from ↦! to : σ) arg res) = + from `KnownEq` arg :?: to ~ res ::: + to `KnownEq` res :?: from ~ arg ::: Eval (Substitute_go σ₀ σ arg res) + + Eval (Substitute_go σ₀ (_ : σ) arg res) = Eval (Substitute_go σ₀ σ arg res) + + Eval (Substitute_go σ₀ '[] arg res) = + -- Once all 'Subst's have been examined, if we can recurse into @arg@ or + -- @res@, do so; otherwise @arg@ doesn't get modified. + KnownApp arg :?: EvalSubstituteApp σ₀ arg res False ::: + KnownApp res :?: EvalSubstituteApp σ₀ arg res True ::: arg ~ res + + -- Expand this 'Within' and prepend it to the result of expanding the + -- remaining 'Subst's. + Eval (Expand (Within w_f w_σ : σ) f₀ res_σ) = + Expand_doWithin '(w_f, w_σ, res_σ) f₀ :&: Expand σ f₀ + + -- Non-'Within's don't get expanded, but they are preserved. + Eval (Expand (s : σ) f₀ res_σ) = DoCons s res_σ :&: Expand σ f₀ + Eval (Expand '[] _ res_σ) = '[] ~ res_σ + + Eval (Expand_doWithin '(w_f, w_σ, res_σ) f σ') = + -- If this 'Within' matches the current scrutinee, prepend its payload. + w_f `KnownEq` f :?: w_σ ++ σ' ~ res_σ ::: + -- Otherwise, advance up the spine of the scrutinee if we can. + KnownApp f :?: Eval (Expand_doWithinApp '(w_f, w_σ, res_σ) f σ') ::: + -- If we can't, this 'Within' does not trigger. Preserve it as-is in the + -- result. + Within w_f w_σ : σ' ~ res_σ + + -- Exists only to decompose the scrutinee into @f _@. Generally, doing this + -- in a type family would risk getting stuck on unknown cases, but this + -- helper is only used guarded by 'KnownApp'. + Eval (Expand_doWithinApp env (f _) σ') = Eval (Expand_doWithin env f σ') + + + Eval (DoCons a α₁ α₂) = a : α₂ ~ α₁ + Eval ((c ::: _) True) = c + Eval ((_ ::: c) False) = c + Eval (Lift1 f a) = f a + + +-- | Independently substitute in the two parts of a type application and +-- recombine the results. Can be driven ‘forward’ or ‘in reverse’, meaning that +-- @f_a@ or @f_b@ respectively are to be used as the source of type information +-- for the next substitution passes. +class EvalSubstituteApp + (σ ∷ List Subst) + -- ^ list of substitutions + (f_a ∷ k) + -- ^ a type, known to be an application, and not matching anything in @σ@ + (f_b ∷ k) + -- ^ @f_a@ after applying @σ@, known to be an application, and not matching + -- anything injective in @σ@ + (in_reverse ∷ Bool) +instance + ( Substitute σ f f' + , Eval (Expand σ f σ') + , Substitute σ' a a' + , f' a' ~ f_b + ) ⇒ EvalSubstituteApp σ (f a) f_b False +instance + ( Substitute σ f' f + , Eval (Expand σ f' σ') + , Substitute σ' b' b + , f_a ~ f' b' + ) ⇒ EvalSubstituteApp σ f_a (f b) True + + +-- | Put 'True' in @result@ if the compiler knows that the two argument types +-- are equal, and 'False' if there is any doubt. For this use case, this level +-- of certainty is good enough. +class KnownEq (a ∷ k₁) (b ∷ k₂) (result ∷ Bool) | a b → result +instance True ~ result ⇒ KnownEq a a result +instance {-# INCOHERENT #-} False ~ result ⇒ KnownEq _₁ _₂ result + + +-- | Put 'True' in @result@ if the compiler knows that the argument type is an +-- application of one type to another, and 'False' if there is any doubt. For +-- this use case, this level of certainty is good enough. +class KnownApp (a ∷ k) (result ∷ Bool) | a → result +instance True ~ result ⇒ KnownApp (f _₁) result +instance {-# INCOHERENT #-} False ~ result ⇒ KnownApp _₁ result + + +-- | Append two type-level lists. Come on, did you expect anything else? +type (++) ∷ List a → List a → List a +type family α₁ ++ α₂ where + '[] ++ α = α + (a : α₁) ++ α₂ = a : (α₁ ++ α₂)