Search code examples
haskelltypeclassproof

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.

Solution

  • 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?