I’m trying to automatically derive a permutation between two type-level lists.
I have the following code
{-# LANGUAGE GHC2021, UndecidableInstances, DataKinds, FunctionalDependencies, TypeFamilies #-}
import Data.Kind (Type)
import Unsafe.Coerce (unsafeCoerce)
import Data.Proxy (Proxy (Proxy))
-- Insert x xs ys proves that x inserted into xs somewhere is equal to ys,
-- equivalently, removing an x from somewhere in ys gives you xs.
data Insert x xs ys where
IN :: Insert x xs (x : xs)
IS :: Insert x xs ys -> Insert x (y : xs) (y : ys)
-- Permutation xs ys proves that there exists a permutation from xs to ys (or vice versa),
-- i.e. there is a way to reorder xs into ys.
type Permutation :: [a] -> [a] -> Type
data Permutation xs ys where
PN :: Permutation '[] '[]
PS :: Insert x ys ys' -> Permutation xs ys -> Permutation (x : xs) ys'
-- Returns true if the inputs are equal.
-- Used as a hint to helper type class.
type family IsEq (x :: a) (y :: a) :: Bool where
IsEq x x = True
IsEq x y = False
-- CInsert x xs ys tries to prove it for you given an x and a ys.
-- It should remove some x from ys and figure out what xs should be.
-- Currently it removes the first x in ys.
class CInsert x xs ys | x ys -> xs where
cinsert :: Insert x xs ys
-- The helper class is an expansion of CInsert along with an is_eq hint.
-- The ys of CInsert must always be non-nil, hence we can expand it.
-- The hint tells us whether x and y should be equal, i.e., whether
-- we should try to unify them.
class Helper (is_eq :: Bool) (x :: a) (xs :: [a]) (y :: a) (ys :: [a]) | is_eq x y ys -> xs where
helper :: Proxy is_eq -> Insert x xs (y : ys)
-- If x and y (head of original ys) seem equal, make them equal,
-- and make original xs the tail of the list.
-- I.e. this is the case where the element we're looking for can
-- be found at the beginning of ys.
instance x ~ y => Helper True x xs y xs where
helper Proxy = IN
-- If they are unequal, recurse.
instance CInsert x xs ys => Helper False x (y : xs) y ys where
helper Proxy = IS cinsert
-- Convert Helper instance into CInsert instance
instance Helper (IsEq x y) x xs y ys => CInsert x xs (y : ys) where
cinsert = helper (Proxy @(IsEq x y))
-- Automatically tries to find a permutation between xs and ys.
class CPermutation (xs :: [a]) (ys :: [a]) where
cpermutation :: Permutation xs ys
instance CPermutation '[] '[] where
cpermutation = PN
-- If the first list is non-nil, we try to remove the head of the first list
-- from somewhere in the second list.
instance (CInsert x ys ys', CPermutation xs ys) => CPermutation (x : xs) ys' where
cpermutation = PS cinsert cpermutation
-- examples
data A
data B
-- the below are all [1,0] (i.e. `PS (IS IN) (PS IN PN)`)
works :: Permutation '[B, A] '[A, B]
works = cpermutation
doesn't_work_rigid :: Proxy a -> Proxy b -> Permutation '[b, a] '[a, b]
-- doesn't_work_rigid Proxy Proxy = cpermutation
doesn't_work_rigid Proxy Proxy = PS (IS IN) (PS IN PN)
doesn't_work_ambiguous :: (forall a b. Proxy a -> Proxy b -> Permutation '[b, a] '[a, b] -> r) -> r
-- doesn't_work_ambiguous f = f Proxy Proxy cpermutation
doesn't_work_ambiguous f = f Proxy Proxy (PS (IS IN) (PS IN PN))
-- show instances
instance Show (Insert x xs ys) where
showsPrec prec x = showsPrec prec (f x) where
f :: forall x xs ys. Insert x xs ys -> Int
f IN = 0
f (IS x) = f x + 1
data SomeInsert -- morally existential newtype
instance Show SomeInsert where
showsPrec prec x = showsPrec prec (unsafeCoerce x :: Insert x xs ys)
instance Show (Permutation xs ys) where
showsPrec prec x = showsPrec prec (unsafeCoerce x :: [SomeInsert])
What I actually want to use it for is something like:
f :: CPermutation xs '[A, B b, C] => F xs -> T
The core point is that I don’t really care about the order of the things in the type-level lists.
Imagine it for example to be a list of effects.
The order of the effects in the type-level list may not have any meaning.
For reasons I won’t dive into, I can’t do the usual thing where you require that A, B b, C
are in the list rather than requiring that it is permutible to that.
I imagine that I can implement something like this with a GHC plugin but I’d preferably avoid that.