Permutation.hs

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wall -Wextra -Werror -Wno-name-shadowing #-}

module Permutation where

import Data.Kind (Constraint, Type)
import Data.Map qualified as Map
import Data.Maybe (fromMaybe)
import Numeric.Natural (Natural)

-- | unary encoding of the natural numbers
type Nat :: Type
data Nat = Zero | Succ Nat

type Sin :: Nat -> Type
data Sin n where
  SZero :: Sin 'Zero
  SSucc :: Sin n -> Sin ('Succ n)

deriving instance Eq (Sin n)

deriving instance Ord (Sin n)

instance KnownNat n => Num (Sin n) where
  fromInteger k = case knownNat @n of
    sn
      | fromSin sn == fromInteger k -> sn
      | otherwise -> error ("expected singular natural " ++ show sn)
  (+) = undefined
  (*) = undefined
  (-) = undefined
  abs = id
  signum = id

type KnownNat :: Nat -> Constraint
class KnownNat n where
  knownNat :: Sin n

instance KnownNat 'Zero where
  knownNat = SZero

instance KnownNat n => KnownNat ('Succ n) where
  knownNat = SSucc knownNat

instance Show (Sin n) where
  showsPrec _ = shows . fromSin

fromSin :: Sin n -> Natural
fromSin = loop 0
  where
    loop :: Natural -> Sin m -> Natural
    loop !n SZero = n
    loop !n (SSucc sn) = loop (n + 1) sn

predSin :: Sin ('Succ n) -> Sin n
predSin (SSucc sn) = sn

-- | all natural numbers less than n
type Fin :: Nat -> Type
data Fin n where
  FZero :: Sin n -> Fin ('Succ n)
  FSucc :: Fin n -> Fin ('Succ n)

deriving instance Eq (Fin n)

deriving instance Ord (Fin n)

instance KnownNat n => Bounded (Fin n) where
  minBound = case knownNat @n of
    SZero -> error "minBound :: Fin 'Zero"
    sn@(SSucc _) -> minFin sn
  maxBound = case knownNat @n of
    SZero -> error "maxBound :: Fin 'Zero"
    sn@(SSucc _) -> maxFin sn

minFin :: Sin ('Succ n) -> Fin ('Succ n)
minFin (SSucc sn) = FZero sn

maxFin :: Sin ('Succ n) -> Fin ('Succ n)
maxFin (SSucc sn) = loop sn
  where
    loop :: Sin m -> Fin ('Succ m)
    loop (SSucc sn) = FSucc (loop sn)
    loop SZero = FZero SZero

instance KnownNat n => Enum (Fin n) where
  toEnum k = toEnum k % knownNat @n

  fromEnum = fromEnum . fst . fromFin

  pred fn = fromMaybe
    do error ("no prior finite natural number: " ++ show fn)
    do predFin fn

  succ fn = fromMaybe
    do error ("no valid successor for finite natural number: " ++ show fn)
    do succFin fn

  enumFrom lo = enumFromTo lo maxBound

  enumFromTo = setup id
    where
      setup :: (Fin m -> r) -> Fin m -> Fin m -> [r]
      setup f (FSucc lo) (FSucc hi) = setup (f . FSucc) lo hi
      setup f lo@(FZero sn) hi = f lo : loop (f . FSucc) sn hi
      setup _ _ (FZero _) = []

      loop :: (Fin m -> r) -> Sin m -> Fin ('Succ m) -> [r]
      loop _ _ (FZero _) = []
      loop _ SZero _ = []
      loop f (SSucc sn) (FSucc fn) = f (FZero sn) : loop (f . FSucc) sn fn

(%) :: Natural -> Sin n -> Fin n
k % sn = fromMaybe
  do error ("invalid finite natural natural number: " ++ show k ++ " % " ++ show sn)
  do toFin k sn

infix 8 %

toFin :: Natural -> Sin n -> Maybe (Fin n)
toFin k sn = loop id sn k
  where
    loop :: (Fin m -> r) -> Sin m -> Natural -> Maybe r
    loop _ SZero _ = Nothing
    loop f (SSucc sn) 0 = Just (f (FZero sn))
    loop f (SSucc sn) n = loop (f . FSucc) sn (n - 1)

fromFin :: Fin n -> (Natural, Sin n)
fromFin (FZero sn) = (0, SSucc sn)
fromFin (FSucc fn) = loop 1 SSucc fn
  where
    loop :: Natural -> (Sin m -> r) -> Fin m -> (Natural, r)
    loop !k f (FSucc fn) = loop (k + 1) (f . SSucc) fn
    loop !k f (FZero sn) = (k, f (SSucc sn))

embedFin :: Fin n -> Fin ('Succ n)
embedFin (FZero sn) = FZero (SSucc sn)
embedFin (FSucc fn) = FSucc (embedFin fn)

narrowFin :: Fin ('Succ n) -> Maybe (Fin n)
narrowFin (FZero SZero) = Nothing
narrowFin (FZero (SSucc sn)) = Just (FZero sn)
narrowFin (FSucc fn) = succFin fn

predFin :: Fin n -> Maybe (Fin n)
predFin (FZero _) = Nothing
predFin (FSucc fn) = Just (embedFin fn)

succFin :: Fin n -> Maybe (Fin n)
succFin = loop id
  where
    loop :: (Fin n -> r) -> Fin n -> Maybe r
    loop f (FSucc fn) = loop (f . FSucc) fn
    loop f (FZero (SSucc sn)) = Just . f . FSucc $ FZero sn
    loop _ (FZero SZero) = Nothing

instance Show (Fin n) where
  showsPrec p fn = showParen
    do p >= 8
    do shows k . showString " % " . shows sn
    where
      (k, sn) = fromFin fn

-- | permutation on n elements
type Perm :: Nat -> Type
data Perm n where
  Trivial :: Perm 'Zero
  -- | given an existing permuation on n elements, insert n+1 at the given
  -- index.
  Insert :: Fin ('Succ n) -> Perm n -> Perm ('Succ n)

infixr 4 `Insert`

deriving instance Eq (Perm n)

deriving instance Ord (Perm n)

deriving instance Show (Perm n)

-- $> identityPerm = 3 % 4 `Insert` 2 % 3 `Insert` 1 % 2 `Insert` 0 % 1 `Insert` Trivial

-- $> getOneLineNotation identityPerm
-- [0 % 4,1 % 4,2 % 4,3 % 4]

-- $> getCycleNotation identityPerm
-- [[0 % 4],[1 % 4],[2 % 4],[3 % 4]]

-- $> mirrorPerm = 0 % 4 `Insert` 0 % 3 `Insert` 0 % 2 `Insert` 0 % 1 `Insert` Trivial

-- $> getOneLineNotation mirrorPerm
-- [3 % 4,2 % 4,1 % 4,0 % 4]

-- $> getCycleNotation mirrorPerm
-- [[0 % 4,3 % 4],[1 % 4,2 % 4]]

-- $> singleCyclePerm = 2 % 4 `Insert` 1 % 3 `Insert` 0 % 2 `Insert` 0 % 1 `Insert` Trivial

-- $> getOneLineNotation singleCyclePerm
-- [1 % 4,2 % 4,3 % 4,0 % 4]

-- $> getCycleNotation singleCyclePerm
-- [[0 % 4,1 % 4,2 % 4,3 % 4]]

getOneLineNotation :: Perm n -> [Fin n]
getOneLineNotation = \case
  Trivial -> []
  Insert fn perm ->
    let (k, sn) = fromFin fn
        (prefix, suffix) = splitAt (fromEnum k) (embedFin <$> getOneLineNotation perm)
     in prefix ++ maxFin sn : suffix

getCycleNotation :: Perm n -> [[Fin n]]
getCycleNotation = cycles . Map.fromList . zip [0 ..] . getOneLineNotation
  where
    cycles m = case Map.minViewWithKey m of
      Nothing -> []
      Just ((k, next), m) -> cycle k id next m
    cycle first xs curr m =
      let ix = fst (fromFin curr)
       in if first == ix
            then (curr : xs []) : cycles m
            else cycle first (xs . (curr :)) (m Map.! ix) (Map.delete ix m)