defunctionalization.hs

{-# Language TypeOperators, GADTs, TypeInType, TypeFamilies #-}
module Help where

import Data.Kind

-- Suppose we have some type families
type family Two  t where Two x = '(x,x)
type family Swap t where Swap '(x,y) = '(y,x)

-- And we want a reusable Map function on types
type family Map (f :: fK dom rng) (xs :: [dom]) :: [rng] where
  Map f '[] = '[]
  Map f (x ': xs) = f $ x ': Map f xs

-- We can defunctionalize our type-families
type Defun = Type -> Type -> Type
data TwoK  :: Defun where Two_ :: TwoK x (x,x)
data SwapK :: Defun where Swap_ :: SwapK (a, b) (b, a)

type family ($) (defun :: fK dom rng) (x :: dom) :: rng
type instance Two_ $ x = Two x
type instance Swap_ $ x = Swap x

-- And we can see it in action here

type Example1 = Map Two_ '[Int, Bool, Char]
type Example2 = Map Swap_ '[ '(Maybe, Bool), '([], Int)]

{-
>>> :kind! Example1
Example1 :: [(*, *)]
= '[ '(Int, Int), '(Bool, Bool), '(Char, Char)]
>>> :kind! Example2
Example2 :: [(*, * -> *)]
= '[ '(Bool, Maybe), '(Int, [])]
-}