Permutation.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Permutation
  ( Permutation(..)
  , refl
  , sym
  , trans
  , here
  , myReverseIsPermutation
  ) where

import Data.Singletons.TH
import Data.Singletons.Prelude.List hiding (Reverse, ReverseSym0, ReverseSym1, sReverse)
import qualified Data.Singletons.Prelude.List as L (Reverse, ReverseSym0, ReverseSym1, sReverse)
import Data.Kind
import Data.Type.Equality (gcastWith)

-- 2つの型レベルリストにおける置換関係
data Permutation :: [k] -> [k] -> Type where
  PermutationNil   :: Permutation '[] '[]
  PermutationSkip  :: Sing a -> Permutation xs ys -> Permutation (a : xs) (a : ys)
  PermutationSwap  :: Sing a -> Sing b -> Permutation (a : b : xs) (b : a : xs)
  PermutationTrans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs

s1 :: Sing 1
s1 = sing
s2 :: Sing 2
s2 = sing
s3 :: Sing 3
s3 = sing
s4 :: Sing 4
s4 = sing

-- おためし
testPermutation :: Permutation [1,2,3,4] [2,4,3,1]
testPermutation =
  PermutationTrans (PermutationSwap s1 s2) $
  PermutationTrans (PermutationSkip s2 $ PermutationSwap s1 s3) $
  PermutationTrans (PermutationSkip s2 $ PermutationSkip s3 $ PermutationSwap s1 s4) $
  PermutationSkip s2 $ PermutationSwap s3 s4

-- 反射律
refl :: Sing xs -> Permutation xs xs
refl  SNil        = PermutationNil
refl (SCons x xs) = PermutationSkip x $ refl xs

-- 対称律
sym :: Permutation xs ys -> Permutation ys xs
sym  PermutationNil          = PermutationNil
sym (PermutationSkip s p)    = PermutationSkip s $ sym p
sym (PermutationSwap a b)    = PermutationSwap b a
sym (PermutationTrans p1 p2) = PermutationTrans (sym p2) (sym p1)

-- 推移律
trans :: Permutation xs ys -> Permutation ys zs -> Permutation xs zs
trans = PermutationTrans

-- 先頭への要素追加と途中への要素追加はPermutation的には同じ
here :: Sing a -> Sing xs -> Sing ys -> Permutation (a : xs :++ ys) (xs :++ (a : ys))
here a  SNil ys        = PermutationSkip a $ refl ys
here a (SCons x xs) ys = PermutationTrans (PermutationSwap a x) (PermutationSkip x $ here a xs ys)

-- []は++の右単位元
nilIsRightIdentityOfAppend :: Sing xs -> (xs :++ '[]) :~: xs
nilIsRightIdentityOfAppend  SNil        = Refl
nilIsRightIdentityOfAppend (SCons _ xs) = gcastWith (nilIsRightIdentityOfAppend xs) Refl

-- singletonsのReverseは置換の一種の筈
reverseIsPermutation :: Sing xs -> Permutation xs (L.Reverse xs)
reverseIsPermutation SNil = PermutationNil
reverseIsPermutation (SCons x xs) = _
{-
[-Wtyped-holes]
    • Found hole:
        _ :: Permutation
               (n0 : n1)
               (Data.Singletons.Prelude.List.Let6989586621679793554Rev
                  (n0 : n1) n1 '[n0])
-}

-- singletonsのReverseの定義がHaskell上での証明に向いてない，
-- (補助関数revがexportされておらず証明時に展開できない)
-- ので独自のreverseを定義する
$(singletonsOnly [d|
 myReverse :: [a] -> [a]
 myReverse l = myReverseAcc l []
 myReverseAcc :: [a] -> [a] -> [a]
 myReverseAcc [] ys = ys
 myReverseAcc (x:xs) ys = myReverseAcc xs (x:ys)
                   |])

-- MyReverseは置換の一種
myReverseIsPermutation :: Sing xs -> Permutation xs (MyReverse xs)
myReverseIsPermutation xs' = gcastWith (nilIsRightIdentityOfAppend xs') (go xs' SNil)
  where
    go :: Sing xs -> Sing ys -> Permutation (xs :++ ys) (MyReverseAcc xs ys)
    go  SNil        ys = refl ys
    go (SCons x xs) ys = PermutationTrans (here x xs ys) (go xs (SCons x ys))