Type-level Haskell programming to ensure that type versions are "migratable"
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | 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