Challenge: implement automatic type-level permutation

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.

1 Like

Does it work for you to just use constraints as sets, instead of lists?

{-# language DataKinds, ConstraintKinds, TypeFamilies, QuantifiedConstraints, UndecidableInstances #-}

import Data.Kind

class Wrap (a :: Type)

type family Encode (xs :: [Type]) :: Constraint where
  Encode '[]       = ()
  Encode (x ': xs) = (Wrap x, Encode xs)

class Permutation' c1 c2
instance (c1 => c2, c2 => c1) => Permutation' c1 c2

type Permutation c1 c2 = Dict (Permutation' (Encode c1) (Encode c2))

data Dict c where
  Dict :: c => Dict c

data A
data B

works :: Permutation '[A, B] '[B, A]
works = Dict

stillWorks :: forall a b. Permutation '[b, a] '[a, b]
stillWorks = Dict

alsoWorks :: forall r. (forall a b. Permutation '[b, a] '[a, b] -> r) -> r
alsoWorks f = f Dict

Drop the Helper and IsEq stuff. You need incoherent instances for this, I think, because there are two valid permutations for '[b, a] '[a, b] if a and b are instantiated as the same type. Type families won’t cut it because the apartness check balks at that possibility.

Replacing your CInsert instances with the below should do it.

instance (xs ~ ys) => CInsert x xs (x : ys) where
  cinsert = IN
instance {-# INCOHERENT #-} CInsert x xs ys => CInsert x (y : xs) (y : ys) where
  cinsert = IS cinsert
1 Like

Thanks! Currently no, I depend on the integer indices, but perhaps I can change my code to work with this or perhaps I can even extract the indices from this somehow.


It doesn’t work for this code though:

data F :: [Type] -> Type

data C (a :: Type)

c :: C a
c = undefined

f :: F '[A, C a]
f = undefined

reorder :: CPermutation xs ys => F xs -> F ys
reorder = undefined

doesn't_work_f_flipped :: forall a. F '[C a, A]
doesn't_work_f_flipped = reorder (f @a)
-- doesn't_work_f_flipped = reorder f

Something like this is my main use-case.
You could just specify the variables every time, but it’s not ergonomic.

This is the error:

permutation.hs:76:26: error: [GHC-39999]
    • No instance for ‘CInsert (C a0) xs '[]’
        arising from a use of ‘reorder’
    • In the expression: reorder f
      In an equation for ‘doesn't_work_f_flipped’:
          doesn't_work_f_flipped = reorder f
76 | doesn't_work_f_flipped = reorder f

I believe the issue is that we have CInsert (C a0) (C a : xs) (C a : ys), which reduces to CInsert (C a0) xs ys, but ys is empty, leading to the error.
What is needed I think is a way of optimistically unifying x and y if possible, and if not skipping it.
I think this would cover most of my use cases. Notably, it doesn’t have to be perfect, since you can manually supply the permutation the rest of the time.

I think this is a simplification:

doesn't_work_cinsert_ambiguous :: forall a r. (forall b xs. Insert (C b) xs '[C a, A] -> r) -> r
doesn't_work_cinsert_ambiguous f = f cinsert

I don’t think there’s any way to backtrack unification. In the choice between matching the heads of the two lists or recursing, if the compiler doesn’t have enough information to choose a branch, it can’t pick one and then come back to the other if that failed. The best you can do is convince the compiler to favor one branch if it can’t prove that the other is going to work, but as you’ve noted this means that if one list contains an unknown it will only match up with the same unknown, and not unify with a constant type or rigid type variable.

1 Like

I have a post about exactly this.

1 Like

Thanks! I tried this but it seems the technique fails when comparing one type variable against another type variable unfortunately.

Not sure what you mean, but I’ve been using this trick a lot and it works well for me.

In general, your puzzle sounds quite interesting, I think you might succeed at nerd-sniping somebody if you post all the details of what you actually need, otherwise it’s kinda vague and seemingly relevant ideas may not apply for the actual use case in the end, so this is a bit discouraging.

1 Like

I think this is basically the same as the incoherent instance approach I suggested here—you’ve abstracted out some things but using incoherent instances to choose whether CInsert should match or recurse should have the same limitations whether used directly or encapsulated in a TryUnify constraint.