Is it possible to disambiguate instances with an intermediate step?

Suppose a scenario where you have an application config, the structure of which has changed a few times. To provide ease of use for users, you wish to allow automatic migration from each version to the next.

The code below shows such a scenario, representing the configuration as VersionedConfig, which is parameterised over the version of the configuration structure.

Given it is possible to migrate between any two successive versions (V1 -> V2, V2 -> V3 and so on), is it possible to write an instance of MigrateableFromTo which composes those instances in the correct order to form the complete set of changes?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Represents different versions of a config file
data ConfigVersion = V1 | V2 | V3

-- | Represents the config itself, at different versions
data VersionedConfig (v :: ConfigVersion) where
  CV1 :: Int -> VersionedConfig V1
  CV2 :: Integer -> VersionedConfig V2
  CV3 :: String -> VersionedConfig V3
  
deriving instance Show (VersionedConfig v)
  
-- | Proof term for migration between versions
data MigrateableProof (from :: ConfigVersion) (to :: ConfigVersion) where
  MigrateableProof :: (VersionedConfig from -> VersionedConfig to) -> MigrateableProof from to
  
class MigrateableFromTo (from :: ConfigVersion) (to :: ConfigVersion) where
  migrateFromTo :: MigrateableProof from to
  
instance MigrateableFromTo V1 V2 where
  migrateFromTo = MigrateableProof (\(CV1 a) -> CV2 (toEnum a))
  
instance MigrateableFromTo V2 V3 where
  migrateFromTo = MigrateableProof (\(CV2 a) -> CV3 (show a))
  
instance forall from intermediate to.
  (MigrateableFromTo from intermediate, MigrateableFromTo intermediate to)
  => MigrateableFromTo from to where
  migrateFromTo = MigrateableProof (applyMigration @intermediate . applyMigration)
    
applyMigration :: MigrateableFromTo from to => VersionedConfig from -> VersionedConfig to
applyMigration = let MigrateableProof f = migrateFromTo in f 

main :: IO ()
main = do
  let
    cv1 = CV1 5
    cv3 = (applyMigration cv1) :: VersionedConfig V3
  print cv3

This code won't compile as from,intermediate, and to in the inductive instance could be the same type. Is it possible to disambiguate this such that the code compiles?

The result at present is as follows:

Main.hs:44:12: error:
    • Overlapping instances for MigrateableFromTo intermediate0 'V3
        arising from a use of ‘applyMigration’
      Matching instances:
        instance (MigrateableFromTo from intermediate,
                  MigrateableFromTo intermediate to) =>
                 MigrateableFromTo from to
          -- Defined at Main.hs:32:10
        instance MigrateableFromTo 'V2 'V3 -- Defined at Main.hs:29:10
      (The choice depends on the instantiation of ‘intermediate0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: (applyMigration cv1) :: VersionedConfig V3
      In an equation for ‘cv3’:
          cv3 = (applyMigration cv1) :: VersionedConfig V3
      In the expression:
        do let cv1 = CV1 5
               cv3 = ...
           print cv3
   |
44 |     cv3 = (applyMigration cv1) :: VersionedConfig V3
   |            ^^^^^^^^^^^^^^

This code is available in the Haskell Playground.

Yes, it's possible. Deep breath:

{-# Language AllowAmbiguousTypes #-}
{-# Language DataKinds #-}
{-# Language FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# Language MultiParamTypeClasses #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}
import Data.Kind

Here's the one-step class that you need to write instances for:

class DirectlyConvertible a where
type DirectConversion a
convertDirectly :: a -> DirectConversion a

And here's the supporting machinery that need only be done once:

class ConvertibleVia (path :: [*]) tgt where
type From path tgt
convert_ :: From path tgt -> tgt
instance ConvertibleVia '[] a where
type From '[] a = a
convert_ = id
instance (DirectlyConvertible a, DirectConversion a ~ From path c, ConvertibleVia path c) => ConvertibleVia (a:path) c where
type From (a:path) c = a
convert_ = convert_ @path . convertDirectly
type family ConversionPath a b where
ConversionPath a a = '[]
ConversionPath a b = a : ConversionPath (DirectConversion a) b
-- tiny wrapper to make the type applications a bit more convenient
convert :: forall src tgt path. (path ~ ConversionPath src tgt, ConvertibleVia path tgt, From path tgt ~ src) => src -> tgt
convert = convert_ @path

With that in place, we can toss in some mock instances:

data V1
data V2
data V3
data V4
instance DirectlyConvertible V1 where type DirectConversion V1 = V2
instance DirectlyConvertible V2 where type DirectConversion V2 = V3
instance DirectlyConvertible V3 where type DirectConversion V3 = V4

And now you can write e.g. convert @V1 @V4, or even convert @V1 if the V4 can be inferred from context, and it will Just Work. Ironic that disambiguating the instance resolution is done by turning on AllowAmbiguousTypes, isn't it?

Here is one approach that I find particularly easy to read.

No type classes are necessary for this approach. I only give a type class at the very end to make it easier to work with. Not only that, but that type class happens to do something very familiar.

This approach is based on the observation that migration is defined entirely by what happens between successive versions (1 -> 2, 2 -> 3, etc). How might we talk about "version successors?"

The other key point is that we want to define a function that will take a proof that version a is at least as old as version b and give back a MigrateableProof a b.

I would first generalize the version type like this, which will let us talk about "successor versions":

data Natural = Z | S Natural
deriving (Show)
-- | Represents different versions of a config file
type ConfigVersion = Natural
type V1 = Z
type V2 = S V1
type V3 = S V2

There are upsides and downsides to this. The main upside is that you can easily talk about successor versions. You can also now talk about any future versions. That might be seen as a downside if you only want to talk about versions that already exist. I don't think this is too much of a downside though. We will get to that next.

We re-implement VersionedConfig like this:

-- | Represents the config itself, at different versions
data VersionedConfig (v :: ConfigVersion) where
CV1 :: Int -> VersionedConfig V1
CV2 :: Integer -> VersionedConfig V2
CV3 :: String -> VersionedConfig V3

This only uses the versions that actually exist. This is why I don't think it's much of a downside that we now can represent non-existent versions in the ConfigVersion type.

Now, we can implement a function which (only) migrates a version to its successor:

migrateToSuccessor :: MigrateableProof from (S from)
migrateToSuccessor = MigrateableProof $ \case
CV1 a ->    -- 1 -> 2
CV2 (toEnum a)
CV2 a ->    -- 2 -> 3
CV3 (show a)

Before we generalize, we need a way to express proofs that a version is less than or equal to another version:

data (:<=) :: Natural -> Natural -> Type where
Refl :: a :<= a
LtS :: a :<= b -> a :<= S b
deriving instance Show (a :<= b)

From this, we can get the general migration function:

migrate :: from :<= to -> MigrateableProof from to
migrate Refl = id
migrate (LtS prf) = migrateToSuccessor . migrate prf

Note that I've used a Category instance for MigrateableProof to make that more readable.^[1] The instance is defined like this:

instance Category MigrateableProof where
id = MigrateableProof id
MigrateableProof p . MigrateableProof q = MigrateableProof (p . q)

So far, we haven't needed any type classes but constructing :<= proofs is tedious. In order to simplify this, we can make a type class that will automatically generate :<= values (proofs) where appropriate:

class Le a b where
le :: a :<= b
instance Le Z Z where
le = Refl
instance forall a b. Le a b => Le (S a) (S b) where
le =
case le @a @b of
Refl -> Refl
LtS prf -> LtS (leStepBoth prf)
leStepBoth :: a :<= b -> S a :<= S b
leStepBoth Refl = Refl
leStepBoth (LtS prf) = LtS $ leStepBoth prf

Finally, we can define applyMigration and rewrite main like this:

applyMigration :: from :<= to -> VersionedConfig from -> VersionedConfig to
applyMigration prf = let MigrateableProof f = migrate prf in f
main :: IO ()
main =
let
cv1 = CV1 5
cv3 = applyMigration le cv1 :: VersionedConfig V3
in
print cv3

Pros and cons

A drawback of this is that we are using a runtime representation of :<= proofs which is probably a bit less efficient than if it was resolved entirely at compile-time. I think it's very unlikely that this will be a performance bottleneck in an actual application, though.

Besides, we need to construct a MigrateableProof value regardless. Think of it like this: migrate turns a proof of a :<= b into a "migrateable proof" from version a to version b.

On the other hand, a benefit of this is that we minimize the usage of polymorphically recursive type classes and type class tricks in general. Such type classes can otherwise be somewhat complicated. I think separating things out like this makes the code more clear and better organized.

A limitation is that this approach can only express migrations that are exclusively given by "successor migrations."

I think it would be possible to modify the approach to allow for other migrations as well (for example, if there is a better way to migrate 1 -> 6 than going through each successor migration).

If you want to make this improvement, the key initial observations for this are probably:

1. The "structure" of :<= is "thin." To put it another way: For any versions a and b, a :<= b can only hold in at most one way.^[2]
2. The migrate function reflects the structure of the :<= value into the resulting MigrationProof value.^[3]

At least one of those would need to be addressed.^[4]

There is another limitation and a fix: migrateToSuccessor allows you to attempt to create the successor of the most recent version. As a result, so does migrate. One way to fix this is to package the code up into a module, avoid exporting migrate and applyMigration and instead export these constrained functions:

type VersionInBound a = Le a V3
migrateSafe :: (VersionInBound to, Le from to) => MigrateableProof from to
migrateSafe = migrate le
applyMigration :: (VersionInBound to, Le from to) => VersionedConfig from -> VersionedConfig to
applyMigration = let MigrateableProof f = migrate le in f 

^[1] ^{In order to use this Category instance like I have, you will need import Prelude hiding (id, (.)) to avoid name clashes as well as import Control.Category}

^[2] ^{Here is a theoretical point that is not necessary to understand what I've described here, but for completeness: I'm using "thin" in this sense.}

^[3] ^{There is another theoretical point that explains this bulletpoint, which is also not necessary to understand: The migrate function is actually a functor from the :<= preorder category to the MigrateableProof category. This is the categorical reason that migrate "reflects the structure of :<= into MigrateableProof." To be more explicit, we run into issues because of the composition law for functors: migrate (f . g) = migrate f . migrate g. This is exactly what we don't want if there are multiple ways to migrate between versions and we want migrate to choose the way that's better than using successors when possible}

^[4] ^{To again state this in categorical terms using the previous two footnotes, we want to do at least one of the following two things: (1) Replace :<= with a category that is not thin. (2) Re-implement migrate knowing that it should not be a functor.}