(注: このコードは型チェックしただけです (実際には実行しませんでした)。)
アプローチ1
実際、証明を GADT に格納することで証明を操作できます。ScopedTypeVariables
このアプローチを有効にするには、有効にする必要があります。
data Proof n where
NilProof :: Proof Ze
ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)
class PlusOneIsSucc n where proof :: Proof n
instance PlusOneIsSucc Ze where proof = NilProof
instance PlusOneIsSucc n => PlusOneIsSucc (Su n) where
proof = case proof :: Proof n of
NilProof -> ConsProof proof
ConsProof _ -> ConsProof proof
rev :: PlusOneIsSucc n => Vec a n -> Vec a n
rev = go proof where
go :: Proof n -> Vec a n -> Vec a n
go NilProof Nil = Nil
go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil
Proof
実は、上記のタイプの興味深い動機かもしれません。
data Proof n where Proof :: (n + Su Ze) ~ Su n => Proof n
しかし、これはうまくいきませんでした: GHC は、私たちが知っているからといって、(Su n)+1 = Su (Su n)
を知っているとは限らないと正しく不平を言いました。したがって、a の意味を拡張して、自然界までのすべての等式の証明を含める必要がありました。これは、帰納法から強い帰納法に移行するときの強化プロセスと本質的に似ています。n+1 = Su n
rev
Cons
Proof
n
アプローチ 2
少し熟考した後、クラスが少し余分であることがわかりました。このアプローチは、追加の拡張機能 ( であってもScopedTypeVariables
) を必要とせず、 の型に追加の制約を導入しないという点で特に優れていVec
ます。
data Proof n where
NilProof :: Proof Ze
ConsProof :: (n + Su Ze) ~ Su n => Proof n -> Proof (Su n)
proofFor :: Vec a n -> Proof n
proofFor Nil = NilProof
proofFor (Cons x xs) = let rec = proofFor xs in case rec of
NilProof -> ConsProof rec
ConsProof _ -> ConsProof rec
rev :: Vec a n -> Vec a n
rev xs = go (proofFor xs) xs where
go :: Proof n -> Vec a n -> Vec a n
go NilProof Nil = Nil
go (ConsProof p) (Cons x xs) = go p xs `append` Cons x Nil
アプローチ 3
代わりにrev
、ビットの実装を cons に切り替えて、最後の要素をリストの反転された最初のセグメントに配置すると、コードはもう少し単純に見える可能性があります。(このアプローチでは、追加の拡張も必要ありません。)
class Rev n where
initLast :: Vec a (Su n) -> (a, Vec a n)
rev :: Vec a n -> Vec a n
instance Rev Ze where
initLast (Cons x xs) = (x, xs)
rev x = x
instance Rev n => Rev (Su n) where
initLast (Cons x xs) = case initLast xs of
(x', xs') -> (x', Cons x xs')
rev as = case initLast as of
(a, as') -> Cons a (rev as')
アプローチ 4
アプローチ 3 と同様ですが、型クラスが不要であることを確認します。
initLast :: Vec a (Su n) -> (a, Vec a n)
initLast (Cons x xs) = case xs of
Nil -> (x, Nil)
Cons {} -> case initLast xs of
(x', xs') -> (x', Cons x xs')
rev :: Vec a n -> Vec a n
rev Nil = Nil
rev xs@(Cons {}) = case initLast xs of
(x, xs') -> Cons x (rev xs')