Type-level Haskell programming to ensure that type versions are "migratable"
-- | A type-level, constraint-writing function that ensures that some | |
-- versioned type is migratable throughout its entire version history. | |
-- | |
-- Assumes that type version history starts at '1'. | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE UndecidableSuperClasses #-} | |
import Data.Kind | |
import Data.Ord | |
import GHC.Exts | |
import GHC.TypeNats | |
-- | "Dummy" constraint | |
class NoConstraint (a :: Nat -> *) where | |
instance NoConstraint a where | |
-- | Haskell does not allow us to define a type family instance for | |
-- both a concrete and a polymorphic type, so we work around it by | |
-- using peano representation. | |
data Nat1 = Zero | Succ Nat1 | |
type family FromNat1 (n :: Nat1) :: Nat where | |
FromNat1 Zero = 0 | |
FromNat1 (Succ n) = 1 + FromNat1 n | |
type family ToNat1 (n :: Nat) :: Nat1 where | |
ToNat1 0 = Zero | |
ToNat1 1 = Succ (ToNat1 0) | |
ToNat1 2 = Succ (ToNat1 1) | |
ToNat1 3 = Succ (ToNat1 2) | |
ToNat1 4 = Succ (ToNat1 3) | |
ToNat1 5 = Succ (ToNat1 4) | |
ToNat1 6 = Succ (ToNat1 5) | |
ToNat1 7 = Succ (ToNat1 6) | |
ToNat1 8 = Succ (ToNat1 7) | |
ToNat1 9 = Succ (ToNat1 8) | |
ToNat1 10 = Succ (ToNat1 9) | |
ToNat1 11 = Succ (ToNat1 10) | |
type family MigrateBound (n :: Nat1) :: (Nat -> Type) -> Constraint | |
type instance MigrateBound Zero = NoConstraint | |
type instance MigrateBound (Succ n) = Migrate (FromNat1 (Succ n)) | |
class ((1 <= n), MigrateBound (ToNat1 (n - 1)) t) => Migrate (n :: Nat) (t :: Nat -> Type) where | |
migrate :: t (n - 1) -> t n | |
data Event (version :: Nat) = SomeEvent | |
instance Migrate 3 Event where | |
migrate = undefined | |
-- -- as expected: | |
-- -- | |
-- Migrate.hs:27:10-24: error: | |
-- • No instance for (Migrate 2 Event) | |
-- arising from the superclasses of an instance declaration | |
-- • In the instance declaration for ‘Migrate 3 Event’ | |
-- | | |
-- 27 | instance Migrate 3 Event where | |
-- | ^^^^^^^^^^^^^^^ | |
-- Failed, no modules loaded. | |
-- -- so lets make it happy: | |
instance Migrate 2 Event where | |
migrate = undefined | |
instance Migrate 1 Event where | |
migrate = undefined | |
-- bonus, if we tried to define: | |
-- | |
-- instance Migrate 0 Event where | |
-- migrate = undefined | |
-- | |
-- we get a type error: | |
-- | |
-- /tmp/Constraints.hs:78:10-24: error: | |
-- • Couldn't match type ‘'False’ with ‘'True’ | |
-- arising from the superclasses of an instance declaration | |
-- • In the instance declaration for ‘Migrate 0 Event’ | |
-- | | |
-- 78 | instance Migrate 0 Event where |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment