7

最初に、私はいくつかの典型的なタイプレベルの自然数のものから始めました。

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

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

そこで、n次元グリッドを表すデータ型を作成したいと思いました。（セルオートマトンの評価で見られるものの一般化はcomonadicです。）

data U (n :: Nat) x where
  Point     :: x                           -> U Z     x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

タイプは、グリッド内の特定のポイントに「焦点を合わせた」sの次元グリッドのU num xタイプであるという考え方です。numx

だから私はこれをコモナドにしたかったのですが、私が作ることができるこの潜在的に有用な関数があることに気づきました：

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r
ufold f (Point x) = f x
ufold f (Dimension ls mid rs) =
  Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs)

これで、このコンビネータに関して、m次元グリッドのn次元グリッドを（n + m）次元グリッドに変換する「次元結合」を実装できます。cojoinこれは、グリッドのグリッドを生成する結果を処理するときに便利です。

dimJoin :: U n (U m x) -> U (Plus n m) x
dimJoin = ufold id

ここまでは順調ですね。Functorまた、インスタンスは。で記述できることにも気づきましたufold。

instance Functor (U n) where
  fmap f = ufold (\x -> Point (f x))

ただし、これによりタイプエラーが発生します。

Couldn't match type `n' with `Plus n 'Z'

しかし、コピーパスタを作ると、タイプエラーはなくなります。

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f (Dimension ls mid rs) =
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs)

コピーパスタの味が嫌いなので、これが私の質問です。に等しい型システムをどのように見分けることができPlus n Znますか？dimJoinそして、キャッチはこれです：同様のタイプエラーを生成する原因となるタイプファミリーインスタンスに変更を加えることはできません。

4

1 に答える 1

5

必要なのは、優れた命題等式タイプです。

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

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

data (:=) :: k -> k -> * where
  Refl :: a := a

data Natural (n :: Nat) where
  Zero :: Natural Z
  Suc  :: Natural n -> Natural (S n)

plusZero :: Natural n -> n := (n `Plus` Z)
plusZero Zero = Refl
plusZero (Suc n) | Refl <- plusZero n = Refl

これにより、タイプに関する任意のことを証明し、のパターンマッチングによってその知識をローカルでスコープに取り込むことができますRefl。

厄介なことの1つは、私のplusZero証明には問題の自然に対する誘導が必要なことです。これは、デフォルトでは実行できません（実行時に存在しないため）。ただし、証人を生成するための型クラスはNatural簡単です。

特定の場合の別のオプションは、型定義の引数をplusに反転しZて、左側を取得し、自動的に減少するようにすることです。多くの場合、型をできる限り単純にすることは良い最初のステップですが、それでも、より複雑なものについては命題の平等が必要になることがよくあります。

于 2012-10-19T00:29:08.267 に答える