タイプファミリーインスタンスプルーフは可能ですか？

Question

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

{-# 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次元グリッドを表すデータ型を作成したかったのです。 （Evaluating cellular automata is 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 

アイデアはタイプU num xがグリッド内の特定の点に「集束」であるx Sのnum次元グリッドの種類があるということです。

は、だから私はこのcomonad作りたかった、と私は私が作ることができ、この潜在的に有用な機能があることに気づい：

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) 

我々は今の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 Zはnとタイプシステムにどのように伝えることができますか？そして、キャッチはこれです：dimJoinに同様の型エラーが発生するような型のファミリインスタンスを変更することはできません。あなたが必要なもの

Answer 1

が素敵な命題平等タイプです：

{-# 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上のパターンマッチングによってローカルスコープにその知識を持って来ることができます。

私のplusZero証明には問題の自然の上に誘導が必要ですが、これは実行時には存在しないため、デフォルトでは実行できません。しかし、Natural目撃者を生成するためのtypeclassは簡単です。

特殊なケースの別のオプションは、型定義の引数を逆にして、Zを自動的に取得し、自動的に減らすことです。あなたのタイプをできるだけシンプルにすることができるようにするためには、まず最初に良い一歩ですが、しばしば、より複雑なものには命題の平等が必要です。