19

GHC 7.6.1には、データ型の昇格など、型レベルでプログラミングするための新機能が付属しています。そこから型レベルの自然とベクトルを例にとると、算術の基本法則に依存するベクトルに関数を記述できるようにしたいと思います。

残念ながら、私が望む法則は、通常、事例分析と帰納法によって帰納的自然について証明するのは簡単ですが、これをタイプチェッカーに納得させることができるかどうかは疑問です。簡単な例として、以下の素朴な逆関数の型チェックには、次の証明が必要ですn + Su Ze ~ Su n

その証拠を提供できる方法はありますか、それとも私は本当に本格的な依存型の領域にいますか?

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TypeOperators #-}

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

type family (m :: Nat) + (n :: Nat) :: Nat

type instance Ze + n = n
type instance (Su m + n) = Su (m + n)

append :: Vec a m -> Vec a n -> Vec a (m + n)
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev (Cons x xs) = rev xs `append` Cons x Nil
4

1 に答える 1

20

(注: このコードは型チェックしただけです (実際には実行しませんでした)。)

アプローチ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 nrevConsProofn

アプローチ 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')
于 2012-09-16T01:33:05.003 に答える