Skip to content

Instantly share code, notes, and snippets.

@tazjin

tazjin/Migratatable.hs

Last active Aug 9, 2018
Embed
What would you like to do?
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